defpred S₁[ object , object ] means for C being Category st C = F . $1 holds
$2 = the carrier' of C;

A9: now :: thesis: for x being object st x in dom F holds
ex y being object st S₁[x,y]

let x be object ; :: thesis: ( x in dom F implies ex y being object st S₁[x,y] )
assume x in dom F ; :: thesis: ex y being object st S₁[x,y]
then reconsider C = F . x as Category by Def1;
reconsider y = the carrier' of C as object ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A10: ( dom f = dom F & ( for x being object st x in dom F holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A9);
f is non-empty

proof

let x be object ; :: according to FUNCT_1:def 9 :: thesis: ( not x in proj1 f or not f . x is empty )
assume A11: x in dom f ; :: thesis: not f . x is empty
then reconsider C = F . x as Category by A10, Def1;
f . x = the carrier' of C by A10, A11;
hence not f . x is empty ; :: thesis: verum

end;

hence ex b₁ being non-empty Function st
( dom b₁ = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b₁ . x = the carrier' of C ) ) by A10; :: thesis: verum