set f = exampleSierpinski150 (m,D);
set A = REAL ;
thus rng (exampleSierpinski150 (m,D)) c= [:REAL,REAL:] :: according to RELAT_1:def 19 :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (exampleSierpinski150 (m,D)) or y in [:REAL,REAL:] )
assume y in rng (exampleSierpinski150 (m,D)) ; :: thesis: y in [:REAL,REAL:]
then consider n being Element of NAT such that
A1: (exampleSierpinski150 (m,D)) . n = y by FUNCT_2:113;
defpred S₁[ Nat] means (exampleSierpinski150 (m,D)) . m in [:REAL,REAL:];
A2: S₁[ 0 ]

proof

(exampleSierpinski150 (m,D)) . 0 = In ([(In (((2 * (m ^2)) + 1),REAL)),(In ((2 * m),REAL))],[:REAL,REAL:]) by Def19;
hence S₁[ 0 ] ; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then reconsider fn = (exampleSierpinski150 (m,D)) . n as Element of [:REAL,REAL:] ;
(exampleSierpinski150 (m,D)) . (n + 1) = In ([(In ((((fn `1) ^2) + (D * ((fn `2) ^2))),REAL)),(In (((2 * (fn `1)) * (fn `2)),REAL))],[:REAL,REAL:]) by Def19;
hence S₁[n + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence y in [:REAL,REAL:] by A1; :: thesis: verum

end;