set h = abs f;

A1: dom (abs f) = dom f by Def36;

rng (abs f) c= N_PFuncs (DOMS Y)

A1: dom (abs f) = dom f by Def36;

rng (abs f) c= N_PFuncs (DOMS Y)

proof

hence
abs f is PartFunc of X,(N_PFuncs (DOMS Y))
by A1, RELSET_1:4; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (abs f) or y in N_PFuncs (DOMS Y) )

assume y in rng (abs f) ; :: thesis: y in N_PFuncs (DOMS Y)

then consider x being object such that

A2: x in dom (abs f) and

A3: (abs f) . x = y by FUNCT_1:def 3;

reconsider y = y as Function by A3;

A4: (abs f) . x = abs (f . x) by A2, Def36;

A5: rng y c= NAT by A3, A4, ORDINAL1:def 12;

f . x in Y by A1, A2, PARTFUN1:4;

then dom (f . x) in { (dom m) where m is Element of Y : verum } ;

then A6: dom (f . x) c= DOMS Y by ZFMISC_1:74;

dom y = dom (f . x) by A3, A4, VALUED_1:def 11;

then y is PartFunc of (DOMS Y),NAT by A6, A5, RELSET_1:4;

hence y in N_PFuncs (DOMS Y) by Def18; :: thesis: verum

end;assume y in rng (abs f) ; :: thesis: y in N_PFuncs (DOMS Y)

then consider x being object such that

A2: x in dom (abs f) and

A3: (abs f) . x = y by FUNCT_1:def 3;

reconsider y = y as Function by A3;

A4: (abs f) . x = abs (f . x) by A2, Def36;

A5: rng y c= NAT by A3, A4, ORDINAL1:def 12;

f . x in Y by A1, A2, PARTFUN1:4;

then dom (f . x) in { (dom m) where m is Element of Y : verum } ;

then A6: dom (f . x) c= DOMS Y by ZFMISC_1:74;

dom y = dom (f . x) by A3, A4, VALUED_1:def 11;

then y is PartFunc of (DOMS Y),NAT by A6, A5, RELSET_1:4;

hence y in N_PFuncs (DOMS Y) by Def18; :: thesis: verum