consider m being Function such that

A1: dom m = F_{1}()
and

A2: for p being object st p in F_{1}() holds

m . p = F_{2}(p)
from FUNCT_1:sch 3();

rng m c= NAT_{1}() by A1, FUNCT_2:67, RELSET_1:4;

take m ; :: thesis: for p being set st p in F_{1}() holds

m . p = F_{2}(p)

thus for p being set st p in F_{1}() holds

m . p = F_{2}(p)
by A2; :: thesis: verum

A1: dom m = F

A2: for p being object st p in F

m . p = F

rng m c= NAT

proof

then reconsider m = m as marking of F
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_{2}(x)
by A1, A2, A3, A4;

hence y in NAT ; :: thesis: verum

end;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

hence y in NAT ; :: thesis: verum

take m ; :: thesis: for p being set st p in F

m . p = F

thus for p being set st p in F

m . p = F