equal
deleted
inserted
replaced
744 assume "a \<noteq> a1" hence "a = a2" using * by auto |
744 assume "a \<noteq> a1" hence "a = a2" using * by auto |
745 hence "?f False = a" by auto thus ?thesis by blast |
745 hence "?f False = a" by auto thus ?thesis by blast |
746 qed |
746 qed |
747 } |
747 } |
748 ultimately show ?thesis unfolding bij_betw_def inj_on_def |
748 ultimately show ?thesis unfolding bij_betw_def inj_on_def |
749 by (metis image_subsetI order_eq_iff subsetI) |
749 by (metis (no_types) image_subsetI order_eq_iff subsetI) |
750 qed |
750 qed |
751 thus ?thesis using card_of_ordIso by blast |
751 thus ?thesis using card_of_ordIso by blast |
752 qed |
752 qed |
753 |
753 |
754 lemma card_of_Plus_Times_aux: |
754 lemma card_of_Plus_Times_aux: |