proposition: Lemma image_invimage_image : forall A : part_set E, Equal (image f (invimage f (image f A))) (image f A).
proof: Proof. simpl in |- *. unfold eq_part in |- *. intros A x; split; [ try assumption | idtac ]. simpl in |- *; auto with algebra. intros H'; try assumption. elim H'; intros x0 E0; elim E0; intros H'0 H'1; elim H'0; intros x1 E1; elim E1; intros H'2 H'3; try exact H'2; clear E1 H'0 E0 H'. exists x1; split; [ try assumption | idtac ]; auto with algebra. apply Trans with (Ap f x0); auto with algebra. simpl in |- *; auto with algebra. intros H'; try assumption. elim H'; intros x0 E0; elim E0; intros H'0 H'1; try exact H'0; clear E0 H'. exists x0; split; [ exists x0; split; [ try assumption | idtac ] | idtac ]; auto with algebra. Qed.
imports: Parts2