theorem Th90: :: NUMBER08:90

for a, b, a1, a2, a3, b1, b2, b3 being Real st a >= 0 & b >= 0 & a1 >= 0 & a2 >= 0 & a3 >= 0 & b1 >= 0 & b2 >= 0 & b3 >= 0 holds
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 )