let f1, f2 be Morphism of a,b; :: thesis: f1 = f2
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1;
thus f1 = f by A2
.= f2 by A2 ; :: thesis: verum