consider f being ManySortedSet of F₁() such that
A2: for a being object st a in F₁() holds
f . a = F₄(a) from PBOOLE:sch 4();
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 reconsider a = a as Element of F₁() by PARTFUN1:def 2;
f . a = F₄(a) by A2;
hence f . a is set by A1; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of F₁() ;
f is ManySortedFunctor of F₂(),F₃()

proof

let a be Element of F₁(); :: according to INDEX_1:def 7 :: thesis: f . a is Functor of F₂() . a,F₃() . a
f . a = F₄(a) by A2;
hence f . a is Functor of F₂() . a,F₃() . a by A1; :: thesis: verum

end;

then reconsider f = f as ManySortedFunctor of F₂(),F₃() ;
take f ; :: thesis: for a being Element of F₁() holds f . a = F₄(a)
thus for a being Element of F₁() holds f . a = F₄(a) by A2; :: thesis: verum