dom absreal = REAL by FUNCT_2:def 1;
then A1: dom (absreal | INT ) = the carrier of INT.Ring by NUMBERS:15, RELAT_1:91;
for y being set st y in rng (absreal | INT ) holds
y in NAT

proof

let y be set ; :: thesis: ( y in rng (absreal | INT ) implies y in NAT )
assume y in rng (absreal | INT ) ; :: thesis: y in NAT
then consider x being set such that
A2: [x,y] in absreal | INT by RELAT_1:def 5;
A3: (absreal | INT ) . x = y by A2, FUNCT_1:8;
A4: x in dom (absreal | INT ) by A2, RELAT_1:def 4;
then reconsider x = x as Integer by A1;
A5: (absreal | INT ) . x = absreal . x by A1, A4, FUNCT_1:72;

now

per cases ( 0 <= x or not 0 <= x ) ;

case A6: 0 <= x ; :: thesis: (absreal | INT ) . x is Element of NAT

(absreal | INT ) . x = abs x by A5, EUCLID:def 2
.= x by A6, ABSVALUE:def 1 ;
hence (absreal | INT ) . x is Element of NAT by A6, INT_1:16; :: thesis: verum

end;

case A7: not 0 <= x ; :: thesis: (absreal | INT ) . x is Element of NAT

A8: (absreal | INT ) . x = abs x by A5, EUCLID:def 2
.= - x by A7, ABSVALUE:def 1 ;
- 0 <= - x by A7;
hence (absreal | INT ) . x is Element of NAT by A8, INT_1:16; :: thesis: verum

end;

end;

end;

hence y in NAT by A3; :: thesis: verum

end;

then rng (absreal | INT ) c= NAT by TARSKI:def 3;
then reconsider f = absreal | INT as Function of the carrier of INT.Ring ,NAT by A1, FUNCT_2:def 1, RELSET_1:11;
take f ; :: thesis: for a being Element of INT.Ring holds f . a = absreal . a
thus for a being Element of INT.Ring holds f . a = absreal . a by FUNCT_1:72; :: thesis: verum