consider f being ManySortedSet of F_{2}() such that

A2: for i being object st i in F_{2}() holds

f . i = F_{5}(i)
from PBOOLE:sch 4();

f is Function-yielding_{2}() ;

f is ManySortedFunction of F_{3}(),F_{4}()
_{3}(),F_{4}() ;

take f ; :: thesis: for i being Element of F_{1}() st i in F_{2}() holds

f . i = F_{5}(i)

thus for i being Element of F_{1}() st i in F_{2}() holds

f . i = F_{5}(i)
by A2; :: thesis: verum

A2: for i being object st i in F

f . i = F

f is Function-yielding

proof

then reconsider f = f as ManySortedFunction of F
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_{2}()
by PARTFUN1:def 2;

then F_{5}(i) is Function
by A1;

hence f . i is set by A2, A3; :: thesis: verum

end;assume i in dom f ; :: thesis: f . i is set

then A3: i in F

then F

hence f . i is set by A2, A3; :: thesis: verum

f is ManySortedFunction of F

proof

then reconsider f = f as ManySortedFunction of F
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in F_{2}() or f . i is Element of bool [:(F_{3}() . i),(F_{4}() . i):] )

assume A4: i in F_{2}()
; :: thesis: f . i is Element of bool [:(F_{3}() . i),(F_{4}() . i):]

then F_{5}(i) is Function of (F_{3}() . i),(F_{4}() . i)
by A1;

hence f . i is Element of bool [:(F_{3}() . i),(F_{4}() . i):]
by A2, A4; :: thesis: verum

end;assume A4: i in F

then F

hence f . i is Element of bool [:(F

take f ; :: thesis: for i being Element of F

f . i = F

thus for i being Element of F

f . i = F