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

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