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

y in NAT

hence
|.p.| is natural-valued
by VALUED_0:def 6, TARSKI:def 3; :: thesis: verumy 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;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