now :: thesis: for o1, o2 being Object of C st not C is empty & ex f1 being morphism of C st
( o1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) holds
o1 = o2
let o1, o2 be Object of C; :: thesis: ( not C is empty & ex f1 being morphism of C st
( o1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) implies o1 = o2 )
assume not C is empty ; :: thesis: ( ex f1 being morphism of C st
( o1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) implies o1 = o2 )
assume ex f1 being morphism of C st
( o1 = f1 & f |> f1 & f1 is identity ) ; :: thesis: ( ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) implies o1 = o2 )
then consider f11 being morphism of C such that
A3: ( o1 = f11 & f |> f11 & f11 is identity ) ;
assume ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) ; :: thesis: o1 = o2
then consider f12 being morphism of C such that
A4: ( o2 = f12 & f |> f12 & f12 is identity ) ;
( f (*) f11 = f & f (*) f12 = f ) by A3, A4, Def5;
then A5: f11 |> f12 by A3, A4, Lm3;
f11 = f11 (*) f12 by A5, A4, Def5
.= f12 by A5, A3, Def4 ;
hence o1 = o2 by A3, A4; :: thesis: verum
end;
hence for b1, b2 being Object of C holds
( ( not C is empty & ex f1 being morphism of C st
( b1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( b2 = f1 & f |> f1 & f1 is identity ) implies b1 = b2 ) & ( C is empty & b1 = the Object of C & b2 = the Object of C implies b1 = b2 ) ) ; :: thesis: verum