thus ( not C is empty implies ex o being Object of C ex f1 being morphism of C st
( o = f1 & f1 |> f & f1 is identity ) ) :: thesis: ( C is empty implies ex b₁ being Object of C st b₁ = the Object of C )

proof

assume A6: not C is empty ; :: thesis: ex o being Object of C ex f1 being morphism of C st
( o = f1 & f1 |> f & f1 is identity )
then consider f1 being morphism of C such that
A7: ( f1 |> f & f1 is identity ) by Lm2;
reconsider o = f1 as Object of C by A7, A6, Th22;
take o ; :: thesis: ex f1 being morphism of C st
( o = f1 & f1 |> f & f1 is identity )
take f1 ; :: thesis: ( o = f1 & f1 |> f & f1 is identity )
thus ( o = f1 & f1 |> f & f1 is identity ) by A7; :: thesis: verum

end;

assume C is empty ; :: thesis: ex b₁ being Object of C st b₁ = the Object of C
take the Object of C ; :: thesis: the Object of C = the Object of C
thus the Object of C = the Object of C ; :: thesis: verum