proposition: Lemma surjective_comp : forall (A B : Setoid) (f f' : MAP A B), surjective f -> Equal f f' -> surjective f'.
proof: Proof. unfold surjective in |- *. intros A B f f' H' H'0 y; try assumption. elim (H' y); intros x E; try exact E. exists x; try assumption. apply Trans with (Ap f x); auto with algebra. Qed.