defpred S₁[ Nat] means ((exampleSierpinski150 (m,D)) . m) `2 > 0 ;
A3: S₁[ 0 ]

proof

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

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
(exampleSierpinski150 (m,D)) . (k + 1) = [(((((exampleSierpinski150 (m,D)) . k) `1) ^2) + (D * ((((exampleSierpinski150 (m,D)) . k) `2) ^2))),((2 * (((exampleSierpinski150 (m,D)) . k) `1)) * (((exampleSierpinski150 (m,D)) . k) `2))] by Def19;
hence ( S₁[k] implies S₁[k + 1] ) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence ((exampleSierpinski150 (m,D)) . n) `2 is positive ; :: thesis: verum