let C be non empty with_identities CategoryStr ; :: thesis: for f being morphism of C holds
( f is identity iff f is Object of C )
let f be morphism of C; :: thesis: ( f is identity iff f is Object of C )

hereby :: thesis: ( f is Object of C implies f is identity )

assume f is identity ; :: thesis: f is Object of C
then f in { u where u is morphism of C : ( u is identity & u in Mor C ) } ;
hence f is Object of C ; :: thesis: verum

end;

assume f is Object of C ; :: thesis: f is identity
then f in { u where u is morphism of C : ( u is identity & u in Mor C ) } ;
then consider u being morphism of C such that
A1: ( f = u & u is identity & u in Mor C ) ;
thus f is identity by A1; :: thesis: verum