let a, b, a1, a2, a3, b1, b2, b3 be Real; :: thesis: ( a >= 0 & b >= 0 & a1 >= 0 & a2 >= 0 & a3 >= 0 & b1 >= 0 & b2 >= 0 & b3 >= 0 implies for n being Nat holds
( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 >= 0 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 >= 0 ) )
assume that
A1: ( a >= 0 & b >= 0 ) and
A2: ( a1 >= 0 & a2 >= 0 & a3 >= 0 & b1 >= 0 & b2 >= 0 & b3 >= 0 ) ; :: thesis: for n being Nat holds
( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 >= 0 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 >= 0 )
set f = recSeqCart (a,b,a1,a2,a3,b1,b2,b3);
defpred S₁[ Nat] means ( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . $1) `1 >= 0 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . $1) `2 >= 0 );
A3: S₁[ 0 ]

proof

(recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . 0 = [a,b] by Def10;
hence S₁[ 0 ] by A1; :: 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] )
(recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1) = [(((a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (a2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + a3),(((b1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + b3)] by Def10;
hence ( S₁[k] implies S₁[k + 1] ) by A2; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence for n being Nat holds
( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 >= 0 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 >= 0 ) ; :: thesis: verum