let m1, m2 be Morphism of a,a; :: thesis: ( ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m1 (*) f = f ) ) ) & ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m2 (*) f = f ) ) ) implies m1 = m2 )
assume that
A1: for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m1 (*) f = f ) ) and
A2: for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m2 (*) f = f ) ) ; :: thesis: m1 = m2
A3: Hom (a,a) <> {} ;
hence m1 = m1 (*) m2 by A2
.= m2 by A3, A1 ;
:: thesis: verum