defpred S₁[ set , set ] means ex a' being Element of A ex t being Functor of F . a',G . a' st
( $1 = a' & $2 = t );

A1: now

let a be set ; :: thesis: ( a in A implies ex f' being set st S₁[a,f'] )
assume a in A ; :: thesis: ex f' being set st S₁[a,f']
then reconsider a' = a as Element of A ;
consider f being Functor of F . a',G . a';
reconsider f' = f as set ;
take f' = f'; :: thesis: S₁[a,f']
thus S₁[a,f'] ; :: thesis: verum

end;

consider f being Function such that
A2: ( dom f = A & ( for a being set st a in A holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A1);
f is Function-yielding

proof

let a be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not a in dom f or f . a is set )
assume a in dom f ; :: thesis: f . a is set
then ex a' being Element of A ex t being Functor of F . a',G . a' st
( a = a' & f . a = t ) by A2;
hence f . a is set ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of A by A2, PARTFUN1:def 4, RELAT_1:def 18;
take f ; :: thesis: for a being Element of A holds f . a is Functor of F . a,G . a
let a be Element of A; :: thesis: f . a is Functor of F . a,G . a
ex a' being Element of A ex t being Functor of F . a',G . a' st
( a = a' & f . a = t ) by A2;
hence f . a is Functor of F . a,G . a ; :: thesis: verum