consider m being Function such that
A1: dom m = F₁() and
A2: for p being object st p in F₁() holds
m . p = F₂(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 = F₂(x) by A1, A2, A3, A4;
hence y in NAT ; :: thesis: verum

end;

then reconsider m = m as marking of F₁() by A1, FUNCT_2:67, RELSET_1:4;
take m ; :: thesis: for p being set st p in F₁() holds
m . p = F₂(p)
thus for p being set st p in F₁() holds
m . p = F₂(p) by A2; :: thesis: verum