theorem Th92: :: NUMBER08:92

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
recSeqCart (a,b,a1,a2,a3,b1,b2,b3) is one-to-one