reconsider F = incl NAT as Function of NAT,ExtREAL by FUNCT_2:9, NUMBERS:31;
take F ; :: thesis: ( F is one-to-one & NAT = rng F & rng F is non empty Subset of ExtREAL )
A1: dom F = NAT by FUNCT_2:def 1;
for y being set holds
( y in NAT iff ex x being set st
( x in dom F & y = F . x ) )

proof

let y be set ; :: thesis: ( y in NAT iff ex x being set st
( x in dom F & y = F . x ) )
( y in NAT implies ex x being set st
( x in dom F & y = F . x ) )

proof

assume A2: y in NAT ; :: thesis: ex x being set st
( x in dom F & y = F . x )
take y ; :: thesis: ( y in dom F & y = F . y )
thus ( y in dom F & y = F . y ) by A2, FUNCT_1:35, FUNCT_2:def 1; :: thesis: verum

end;

hence ( y in NAT iff ex x being set st
( x in dom F & y = F . x ) ) by A1, FUNCT_1:35; :: thesis: verum

end;

hence ( F is one-to-one & NAT = rng F & rng F is non empty Subset of ExtREAL ) by FUNCT_1:def 5; :: thesis: verum