consider f being ManySortedSet of F₂() such that
A2: for i being object st i in F₂() holds
f . i = F₅(i) from PBOOLE:sch 4();
f is Function-yielding

proof

let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in proj1 f or f . i is set )
assume i in dom f ; :: thesis: f . i is set
then A3: i in F₂() by PARTFUN1:def 2;
then F₅(i) is Function by A1;
hence f . i is set by A2, A3; :: thesis: verum

end;

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

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in F₂() or f . i is Element of bool [:(F₃() . i),(F₄() . i):] )
assume A4: i in F₂() ; :: thesis: f . i is Element of bool [:(F₃() . i),(F₄() . i):]
then F₅(i) is Function of (F₃() . i),(F₄() . i) by A1;
hence f . i is Element of bool [:(F₃() . i),(F₄() . i):] by A2, A4; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of F₃(),F₄() ;
take f ; :: thesis: for i being Element of F₁() st i in F₂() holds
f . i = F₅(i)
thus for i being Element of F₁() st i in F₂() holds
f . i = F₅(i) by A2; :: thesis: verum