set f = exampleSierpinski150 (m,D);
set A = RAT ;
thus rng (exampleSierpinski150 (m,D)) c= [:RAT,RAT:] :: 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 [:RAT,RAT:] )
assume y in rng (exampleSierpinski150 (m,D)) ; :: thesis: y in [:RAT,RAT:]
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 [:RAT,RAT:];
A2: S₁[ 0 ]

proof

reconsider r = (2 * (m ^2)) + 1, s = 2 * m as Rational ;
(exampleSierpinski150 (m,D)) . 0 = In ([(In (r,RAT)),(In (s,RAT))],[:RAT,RAT:]) 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 [:RAT,RAT:] ;
reconsider r = ((fn `1) ^2) + (D * ((fn `2) ^2)), s = (2 * (fn `1)) * (fn `2) as Rational ;
(exampleSierpinski150 (m,D)) . (n + 1) = In ([(In (r,RAT)),(In (s,RAT))],[:RAT,RAT:]) 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 [:RAT,RAT:] by A1; :: thesis: verum

end;