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

proof

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

end;

consider f being ManySortedSet of F₁() such that
A3: for o being object st o in F₁() holds
S₁[o,f . o] from PBOOLE:sch 3(A1);
f is Function-yielding

proof

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

end;

then reconsider f = f as ManySortedFunction of F₁() ;
take f ; :: thesis: for o being Element of F₁() holds
( dom (f . o) = F₂(o) & ( for x being Element of F₂(o) holds (f . o) . x = F₃(o,x) ) )
let o be Element of F₁(); :: thesis: ( dom (f . o) = F₂(o) & ( for x being Element of F₂(o) holds (f . o) . x = F₃(o,x) ) )
A4: S₁[o,f . o] by A3;
hence dom (f . o) = F₂(o) ; :: thesis: for x being Element of F₂(o) holds (f . o) . x = F₃(o,x)
let x be Element of F₂(o); :: thesis: (f . o) . x = F₃(o,x)
thus (f . o) . x = F₃(o,x) by A4; :: thesis: verum