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

A1: now :: thesis: for a being object st a in A holds
ex f being object st S₁[a,f]

let a be object ; :: thesis: ( a in A implies ex f being object st S₁[a,f] )
assume a in A ; :: thesis: ex f being object st S₁[a,f]
then reconsider a9 = a as Element of A ;
set f = the Functor of F . a9,G . a9;
reconsider f = the Functor of F . a9,G . a9 as object ;
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 object st a in A holds
S₁[a,f . a] ) ) from CLASSES1:sch 1(A1);
f is Function-yielding

proof

let a be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not a in proj1 f or f . a is set )
assume a in dom f ; :: thesis: f . a is set
then ex a9 being Element of A ex t being Functor of F . a9,G . a9 st
( a = a9 & 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 2, 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 a9 being Element of A ex t being Functor of F . a9,G . a9 st
( a = a9 & f . a = t ) by A2;
hence f . a is Functor of F . a,G . a ; :: thesis: verum