defpred S1[ object , object ] means ex f being Function st
( $2 = f & dom f = F2() . $1 & ( for y being Element of F2() . $1 holds f . y = F3($1,y) ) );
A1: for x being object st x in F1() holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in F1() implies ex y being object st S1[x,y] )
assume A2: x in F1() ; :: thesis: ex y being object st S1[x,y]
then reconsider s = x as Element of F1() ;
deffunc H2( object ) -> set = F3(x,$1);
consider f being Function such that
A3: ( dom f = F2() . x & ( for y being object st y in F2() . x holds
f . y = H2(y) ) ) from FUNCT_1:sch 3();
 take f ; :: thesis: S1[x,f]
take f ; :: thesis: ( f = f & dom f = F2() . x & ( for y being Element of F2() . x holds f . y = F3(x,y) ) )
thus ( f = f & dom f = F2() . x & ( for y being Element of F2() . x holds f . y = F3(x,y) ) ) by A2, A3; :: thesis: verum
end;
consider g being Function such that
A4: ( dom g = F1() & ( for x being object st x in F1() holds
S1[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 S1[x,g . x] by A4;
hence g . x is set ; :: thesis: verum
end;
then reconsider g = g as ManySortedFunction of F1() by A4, RELAT_1:def 18, PARTFUN1:def 2;
take g ; :: thesis: for x being set st x in F1() holds
( dom (g . x) = F2() . x & ( for y being Element of F2() . x holds (g . x) . y = F3(x,y) ) )
let x be set ; :: thesis: ( x in F1() implies ( dom (g . x) = F2() . x & ( for y being Element of F2() . x holds (g . x) . y = F3(x,y) ) ) )
assume x in F1() ; :: thesis: ( dom (g . x) = F2() . x & ( for y being Element of F2() . x holds (g . x) . y = F3(x,y) ) )
then ( S1[x,g . x] & F2() . x <> {} ) by A4;
hence ( dom (g . x) = F2() . x & ( for y being Element of F2() . x holds (g . x) . y = F3(x,y) ) ) ; :: thesis: verum