A2:
for x being set st x in F2() holds
F4(x) in F3()
by A1;
consider f being Function of F2(),F3() such that
A3:
for x being set st x in F2() holds
f . x = F4(x)
from FUNCT_2:sch 2(A2);
take
f
; :: thesis: for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z)
thus
for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z)
by A3; :: thesis: verum