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

A1: 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
A2: ( dom f = dom F & ( for x being object st x in dom F holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
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 A3: x in dom f ; :: thesis: not f . x is empty
then reconsider C = F . x as Category by A2, Def1;
f . x = the carrier of C by A2, A3;
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 A2; :: thesis: verum