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