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 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 ) )
assume that
A1: ( a > 0 & b > 0 ) and
A2: ( a1 >= 1 & a2 > 0 & a3 >= 0 ) and
A3: ( b1 > 0 & b2 >= 1 & b3 >= 0 ) ; :: thesis: 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 )
set f = recSeqCart (a,b,a1,a2,a3,b1,b2,b3);
let m, n be Nat; :: thesis: ( m > n implies ( ((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 ) )
assume A4: m > n ; :: thesis: ( ((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 )
defpred S₁[ Nat] means ( $1 > n implies ( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . $1) `1 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . $1) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 ) );
A5: S₁[ 0 ] ;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A7: S₁[k] and
A8: k + 1 > n ; :: thesis: ( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `1 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 )
A9: (recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1) = [(((a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (a2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + a3),(((b1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + b3)] by Def10;
((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1 >= 0 by A1, A2, A3, Th90;
then A10: 1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1) <= a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1) by A2, XREAL_1:64;
((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2 > 0 by A1, A2, A3, Th89;
then B11: (a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + 0 < (a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (a2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2)) by A2, XREAL_1:6;
((a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (a2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + 0 <= ((a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (a2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + a3 by A2, XREAL_1:6;
then A11: (a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + 0 < ((a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (a2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + a3 by B11, XXREAL_0:2;
((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2 >= 0 by A1, A2, A3, Th90;
then A12: 1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2) <= b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2) by A3, XREAL_1:64;
((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1 > 0 by A1, A2, A3, Th89;
then B13: (b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2)) + 0 < (b1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2)) by A3, XREAL_1:6;
((b1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + 0 <= ((b1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + b3 by A3, XREAL_1:6;
then A13: (b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2)) + 0 < ((b1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1)) + (b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2))) + b3 by B13, XXREAL_0:2;
k >= n by A8, NAT_1:13;

per cases then ( k > n or k = n ) by XXREAL_0:1;

suppose A14: k > n ; :: thesis: ( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `1 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 )

then ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 < a1 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `1) by A7, A10, XXREAL_0:2;
hence ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `1 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 by A9, A11, XXREAL_0:2; :: thesis: ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2
((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 < b2 * (((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . k) `2) by A7, A12, A14, XXREAL_0:2;
hence ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 by A9, A13, XXREAL_0:2; :: thesis: verum

end;

suppose k = n ; :: thesis: ( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `1 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 )

hence ( ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `1 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `1 & ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . (k + 1)) `2 > ((recSeqCart (a,b,a1,a2,a3,b1,b2,b3)) . n) `2 ) by A9, A10, A11, A12, A13, XXREAL_0:2; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
hence ( ((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 ) by A4; :: thesis: verum