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 b₁, b₂ being Object of C holds
( ( not C is empty & ex f1 being morphism of C st
( b₁ = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( b₂ = f1 & f |> f1 & f1 is identity ) implies b₁ = b₂ ) & ( C is empty & b₁ = the Object of C & b₂ = the Object of C implies b₁ = b₂ ) ) ; :: thesis: verum