reconsider F = incl NAT as Function of NAT ,ExtREAL by FUNCT_2:9, NUMBERS:31;
A1: ( rng F is non empty Subset of ExtREAL & dom F = NAT & F is one-to-one & rng F = NAT )

proof

A2: ( dom F = NAT & rng F c= ExtREAL ) 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 A3: 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 A3, 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 A2, FUNCT_1:35; :: thesis: verum

end;

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

end;

take F ; :: thesis: ( F is one-to-one & NAT = rng F & rng F is non empty Subset of ExtREAL )
thus ( F is one-to-one & NAT = rng F & rng F is non empty Subset of ExtREAL ) by A1; :: thesis: verum