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

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

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

then
rng (absreal | INT) c= NAT
by TARSKI:def 3;
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;

end;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 ) )

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

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