A8: ( not C is empty implies ex F being Function of (Mor C),(Ob C) st
for f being Element of Mor C holds F . f = cod f )

proof

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

proof

let x be Element of A; :: thesis: ex y being Element of O st S₁[x,y]
reconsider f = x as Element of Mor C ;
reconsider y = cod f as Element of O ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider F being Function of A,O such that
A10: for x being Element of A holds S₁[x,F . x] from FUNCT_2:sch 3(A9);
reconsider F = F as Function of (Mor C),(Ob C) ;
take F ; :: thesis: for f being Element of Mor C holds F . f = cod f
let f be Element of Mor C; :: thesis: F . f = cod f
S₁[f,F . f] by A10;
hence F . f = cod f ; :: thesis: verum

end;

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

proof

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

end;

A12: for F1, F2 being Function of (Mor C),(Ob C) st ( for f being Element of Mor C holds F1 . f = cod f ) & ( for f being Element of Mor C holds F2 . f = cod f ) holds
F1 = F2

proof

let F1, F2 be Function of (Mor C),(Ob C); :: thesis: ( ( for f being Element of Mor C holds F1 . f = cod f ) & ( for f being Element of Mor C holds F2 . f = cod f ) implies F1 = F2 )
assume A13: for f being Element of Mor C holds F1 . f = cod f ; :: thesis: ( ex f being Element of Mor C st not F2 . f = cod f or F1 = F2 )
assume A14: for f being Element of Mor C holds F2 . f = cod f ; :: thesis: F1 = F2
for x being object st x in Mor C holds
F1 . x = F2 . x

proof

let x be object ; :: thesis: ( x in Mor C implies F1 . x = F2 . x )
assume x in Mor C ; :: thesis: F1 . x = F2 . x
then reconsider f = x as Element of Mor C ;
thus F1 . x = cod f by A13
.= F2 . x by A14 ; :: thesis: verum

end;

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

end;

thus ( ( for b₁ being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b₁ being Function of (Mor C),(Ob C) st
for f being Element of Mor C holds b₁ . f = cod f ) & ( C is empty implies ex b₁ being Function of (Mor C),(Ob C) st b₁ = {} ) & ( for b₁, b₂ being Function of (Mor C),(Ob C) holds
( ( not C is empty & ( for f being Element of Mor C holds b₁ . f = cod f ) & ( for f being Element of Mor C holds b₂ . f = cod f ) implies b₁ = b₂ ) & ( C is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) ) ) by A8, A11, A12; :: thesis: verum