consider f being ManySortedSet of F2() such that
A2: for i being object st i in F2() holds
f . i = F5(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 F2() by PARTFUN1:def 2;
then F5(i) is Function by A1;
hence f . i is set by A2, A3; :: thesis: verum
end;
then reconsider f = f as ManySortedFunction of F2() ;
f is ManySortedFunction of F3(),F4()
proof
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in F2() or f . i is Element of bool [:(F3() . i),(F4() . i):] )
assume A4: i in F2() ; :: thesis: f . i is Element of bool [:(F3() . i),(F4() . i):]
then F5(i) is Function of (F3() . i),(F4() . i) by A1;
hence f . i is Element of bool [:(F3() . i),(F4() . i):] by A2, A4; :: thesis: verum
end;
then reconsider f = f as ManySortedFunction of F3(),F4() ;
take f ; :: thesis: for i being Element of F1() st i in F2() holds
f . i = F5(i)
thus for i being Element of F1() st i in F2() holds
f . i = F5(i) by A2; :: thesis: verum