now :: thesis: for o1, o2 being Object of C st not C is empty & ex f1 being morphism of C st
( o1 = f1 & f1 |> f & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f1 |> f & 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 & f1 |> f & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f1 |> f & f1 is identity ) implies o1 = o2 )
assume not C is empty ; :: thesis: ( ex f1 being morphism of C st
( o1 = f1 & f1 |> f & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f1 |> f & f1 is identity ) implies o1 = o2 )
assume ex f1 being morphism of C st
( o1 = f1 & f1 |> f & f1 is identity ) ; :: thesis: ( ex f1 being morphism of C st
( o2 = f1 & f1 |> f & f1 is identity ) implies o1 = o2 )
then consider f11 being morphism of C such that
A8: ( o1 = f11 & f11 |> f & f11 is identity ) ;
assume ex f1 being morphism of C st
( o2 = f1 & f1 |> f & f1 is identity ) ; :: thesis: o1 = o2
then consider f12 being morphism of C such that
A9: ( o2 = f12 & f12 |> f & f12 is identity ) ;
( f11 (*) f = f & f12 (*) f = f ) by A8, A9, Def4;
then A10: f11 |> f12 by A8, A9, Lm3;
f11 = f11 (*) f12 by A10, A9, Def5
.= f12 by A10, A8, Def4 ;
hence o1 = o2 by A8, A9; :: 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 & f1 |> f & f1 is identity ) & ex f1 being morphism of C st
( b₂ = f1 & f1 |> f & f1 is identity ) implies b₁ = b₂ ) & ( C is empty & b₁ = the Object of C & b₂ = the Object of C implies b₁ = b₂ ) ) ; :: thesis: verum