now :: thesis: for y being object st y in rng |.p.| holds
y in NAT

let y be object ; :: thesis: ( y in rng |.p.| implies y in NAT )
assume y in rng |.p.| ; :: thesis: y in NAT
then consider x being object such that
A1: ( x in dom |.p.| & |.p.| . x = y ) by FUNCT_1:def 3;
|.p.| . x = |.(p . x).| by A1, Def1;
hence y in NAT by A1, ORDINAL1:def 12; :: thesis: verum

end;

hence |.p.| is natural-valued by VALUED_0:def 6, TARSKI:def 3; :: thesis: verum