theorem Th89: :: NUMBER08:89

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