defpred S₁[ object , object ] means ex f being Function st
( $2 = f & dom f = F₂() . $1 & ( for y being Element of F₂() . $1 holds f . y = F₃($1,y) ) );
A1: for x being object st x in F₁() holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in F₁() implies ex y being object st S₁[x,y] )
assume A2: x in F₁() ; :: thesis: ex y being object st S₁[x,y]
then reconsider s = x as Element of F₁() ;
deffunc H₂( object ) -> set = F₃(x,$1);
consider f being Function such that
A3: ( dom f = F₂() . x & ( for y being object st y in F₂() . x holds
f . y = H₂(y) ) ) from FUNCT_1:sch 3();
take f ; :: thesis: S₁[x,f]
take f ; :: thesis: ( f = f & dom f = F₂() . x & ( for y being Element of F₂() . x holds f . y = F₃(x,y) ) )
thus ( f = f & dom f = F₂() . x & ( for y being Element of F₂() . x holds f . y = F₃(x,y) ) ) by A2, A3; :: thesis: verum

end;

consider g being Function such that
A4: ( dom g = F₁() & ( for x being object st x in F₁() holds
S₁[x,g . x] ) ) from CLASSES1:sch 1(A1);
g is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 g or g . x is set )
assume x in dom g ; :: thesis: g . x is set
then S₁[x,g . x] by A4;
hence g . x is set ; :: thesis: verum

end;

then reconsider g = g as ManySortedFunction of F₁() by A4, RELAT_1:def 18, PARTFUN1:def 2;
take g ; :: thesis: for x being set st x in F₁() holds
( dom (g . x) = F₂() . x & ( for y being Element of F₂() . x holds (g . x) . y = F₃(x,y) ) )
let x be set ; :: thesis: ( x in F₁() implies ( dom (g . x) = F₂() . x & ( for y being Element of F₂() . x holds (g . x) . y = F₃(x,y) ) ) )
assume x in F₁() ; :: thesis: ( dom (g . x) = F₂() . x & ( for y being Element of F₂() . x holds (g . x) . y = F₃(x,y) ) )
then ( S₁[x,g . x] & F₂() . x <> {} ) by A4;
hence ( dom (g . x) = F₂() . x & ( for y being Element of F₂() . x holds (g . x) . y = F₃(x,y) ) ) ; :: thesis: verum