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

proof

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

end;