A1: ( not C is empty implies ex F being Function of (Ob C),(Mor C) st
for o being Element of Ob C holds F . o = id- o )

assume not C is empty ; :: thesis:
then reconsider A = Mor C, O = Ob C as non empty set ;
defpred S₁[ set , set ] means ex o being Element of Ob C ex a being Element of Mor C st
( o = $1 & a = $2 & a = id- o );
A2: for x being Element of O ex y being Element of A st S₁[x,y]

let x be Element of O; :: thesis:
reconsider o = x as Element of Ob C ;
reconsider y = id- o as Element of A ;
take y ; :: thesis:
thus S₁[x,y] ; :: thesis:

end;

consider F being Function of O,A such that
A3: for x being Element of O holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
reconsider F = F as Function of (Ob C),(Mor C) ;
take F ; :: thesis:
let o be Element of Ob C; :: thesis:
S₁[o,F . o] by A3;
hence F . o = id- o ; :: thesis:

end;

A4: ( C is empty implies ex F being Function of (Ob C),(Mor C) st F = {} )

assume C is empty ; :: thesis:
then ( Mor C = {} & Ob C = {} ) ;
then reconsider F = {} as Function of (Ob C),(Mor C) ;
take F ; :: thesis:
thus F = {} ; :: thesis:

end;

A5: for F1, F2 being Function of (Ob C),(Mor C) st ( for o being Element of Ob C holds F1 . o = id- o ) & ( for o being Element of Ob C holds F2 . o = id- o ) holds
F1 = F2

let x be object ; :: thesis:
assume x in Ob C ; :: thesis:
then reconsider o = x as Element of Ob C ;
thus F1 . x = id- o by A6
.= F2 . x by A7 ; :: thesis:

end;

end;

thus ( ( for b₁ being Function of (Ob C),(Mor C) holds verum ) & ( not C is empty implies ex b₁ being Function of (Ob C),(Mor C) st
for o being Element of Ob C holds b₁ . o = id- o ) & ( C is empty implies ex b₁ being Function of (Ob C),(Mor C) st b₁ = {} ) & ( for b₁, b₂ being Function of (Ob C),(Mor C) holds
( ( not C is empty & ( for o being Element of Ob C holds b₁ . o = id- o ) & ( for o being Element of Ob C holds b₂ . o = id- o ) implies b₁ = b₂ ) & ( C is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) ) ) by A1, A4, A5; :: thesis: