theorem Th91: :: NUMBER08:91

for a, b, a1, a2, a3, b1, b2, b3 being Real st a > 0 & b > 0 & a1 >= 1 & a2 > 0 & a3 >= 0 & b1 > 0 & b2 >= 1 & b3 >= 0 holds
for m, n being Nat st m > n holds
( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . m) `1 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . m) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 )