consider m being Function such that
A1: dom m = F1() and
A2: for p being object st p in F1() holds
m . p = F2(p) from FUNCT_1:sch 3();
 rng m c= NAT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng m or y in NAT )
assume y in rng m ; :: thesis: y in NAT
then consider x being object such that
A3: x in dom m and
A4: y = m . x by FUNCT_1:def 3;
y = F2(x) by A1, A2, A3, A4;
hence y in NAT ; :: thesis: verum
end;
then reconsider m = m as marking of F1() by A1, FUNCT_2:67, RELSET_1:4;
take m ; :: thesis: for p being set st p in F1() holds
m . p = F2(p)
thus for p being set st p in F1() holds
m . p = F2(p) by A2; :: thesis: verum