rng (SMoebius X) c= REAL

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (SMoebius X) or y in REAL )
assume y in rng (SMoebius X) ; :: thesis: y in REAL
then consider i being object such that
A1: i in dom (SMoebius X) and
A2: (SMoebius X) . i = y by FUNCT_1:def 3;
dom (SMoebius X) = NAT by PARTFUN1:def 2;
then reconsider i = i as Nat by A1;

per cases ( i in support (SMoebius X) or not i in support (SMoebius X) ) ;

suppose i in support (SMoebius X) ; :: thesis: y in REAL

then y = Moebius i by A2, Def5;
hence y in REAL by XREAL_0:def 1; :: thesis: verum

end;

suppose not i in support (SMoebius X) ; :: thesis: y in REAL

then (SMoebius X) . i = In (0,REAL) by PRE_POLY:def 7;
hence y in REAL by A2; :: thesis: verum

end;

end;

end;

hence SMoebius X is real-valued by VALUED_0:def 3; :: thesis: verum