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

A9: now :: thesis:

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

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:
assume A11: x in dom f ; :: thesis:
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:

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: