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

proof

let y be object ; :: thesis: ( y in rng (absreal | INT) implies y in NAT )
assume y in rng (absreal | INT) ; :: thesis: y in NAT
then consider x being object such that
A2: [x,y] in absreal | INT by XTUPLE_0:def 13;
A3: (absreal | INT) . x = y by A2, FUNCT_1:1;
A4: x in dom (absreal | INT) by A2, XTUPLE_0:def 12;
then reconsider x = x as Integer by A1;
A5: (absreal | INT) . x = absreal . x by A1, A4, FUNCT_1:49;

now :: thesis: ( ( 0 <= x & (absreal | INT) . x is Element of NAT ) or ( not 0 <= x & (absreal | INT) . x is Element of NAT ) )

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

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

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

end;

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

(absreal | INT) . x = |.x.| by A5, EUCLID:def 2
.= - x by A7, ABSVALUE:def 1 ;
hence (absreal | INT) . x is Element of NAT by A7, INT_1:3; :: 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 INT.Ring,NAT by A1, FUNCT_2:def 1, RELSET_1:4;
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:49; :: thesis: verum