let C be non empty category; :: thesis: for f being morphism of C holds
( f is identity iff ex o being Object of (Alter C) st f = id o )
let f be morphism of C; :: thesis: ( f is identity iff ex o being Object of (Alter C) st f = id o )
set A = Alter C;
reconsider a = f as morphism of (alter (Alter C)) ;
hereby :: thesis: ( ex o being Object of (Alter C) st f = id o implies f is identity )
assume f is identity ; :: thesis: ex o being Object of (Alter C) st f = id o
then a is identity by Th25;
then consider o being Object of (Alter C) such that
A1: a = id o by Th42;
take o = o; :: thesis: f = id o
thus f = id o by A1; :: thesis: verum
end;
given o being Object of (Alter C) such that A2: f = id o ; :: thesis: f is identity
a is identity by A2, Th42;
hence f is identity by Th25; :: thesis: verum