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 )

proof

assume not C is empty ; :: thesis: ex F being Function of (Ob C),(Mor C) st
for o being Element of Ob C holds F . o = id- o
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]

proof

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

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: for o being Element of Ob C holds F . o = id- o
let o be Element of Ob C; :: thesis: F . o = id- o
S₁[o,F . o] by A3;
hence F . o = id- o ; :: thesis: verum

end;

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

proof

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

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

proof

let F1, F2 be Function of (Ob C),(Mor C); :: thesis: ( ( for o being Element of Ob C holds F1 . o = id- o ) & ( for o being Element of Ob C holds F2 . o = id- o ) implies F1 = F2 )
assume A6: for o being Element of Ob C holds F1 . o = id- o ; :: thesis: ( ex o being Element of Ob C st not F2 . o = id- o or F1 = F2 )
assume A7: for o being Element of Ob C holds F2 . o = id- o ; :: thesis: F1 = F2
for x being object st x in Ob C holds
F1 . x = F2 . x

proof

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

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum

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: verum