let a, b, a1, a2, a3, b1, b2, b3 be Real; :: thesis: ( a > 0 & b > 0 & a1 >= 1 & a2 > 0 & a3 >= 0 & b1 > 0 & b2 >= 1 & b3 >= 0 implies recSeqCart (a,b,a1,a2,a3,b1,b2,b3) is one-to-one )
assume A1: ( a > 0 & b > 0 & a1 >= 1 & a2 > 0 & a3 >= 0 & b1 > 0 & b2 >= 1 & b3 >= 0 ) ; :: thesis: recSeqCart (a,b,a1,a2,a3,b1,b2,b3) is one-to-one
set f = recSeqCart (a,b,a1,a2,a3,b1,b2,b3);
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) or not x2 in proj1 (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) or not (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . x1 = (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . x2 or x1 = x2 )
assume that
A2: ( x1 in dom (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) & x2 in dom (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) ) and
A3: (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . x1 = (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NAT by A2, PARTFUN1:def 2;

now :: thesis: not x1 <> x2

assume x1 <> x2 ; :: thesis: contradiction
then ( x1 < x2 or x2 < x1 ) by XXREAL_0:1;
then ( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . x1) `1 < ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . x2) `1 or ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . x2) `1 < ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . x1) `1 ) by A1, Th91;
hence contradiction by A3; :: thesis: verum

end;

hence x1 = x2 ; :: thesis: verum