set f = recSeqCart (a,b,x1,x2,x3,y1,y2,y3);
A1: ( a in NAT & b in NAT ) by ORDINAL1:def 12;
defpred S₁[ Nat] means (recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . a in [:NAT,NAT:];
A2: S₁[ 0 ]

proof

(recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . 0 = [a,b] by Def10;
hence S₁[ 0 ] by A1, ZFMISC_1:87; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then ( ((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `1 in NAT & ((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `2 in NAT ) by MCART_1:10;
then A4: ( ((x1 * (((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `1)) + (x2 * (((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `2))) + x3 in NAT & ((y1 * (((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `1)) + (y2 * (((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `2))) + y3 in NAT ) by ORDINAL1:def 12;
(recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . (n + 1) = [(((x1 * (((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `1)) + (x2 * (((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `2))) + x3),(((y1 * (((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `1)) + (y2 * (((recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . n) `2))) + y3)] by Def10;
hence S₁[n + 1] by A4, ZFMISC_1:87; :: thesis: verum

end;

A5: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
thus rng (recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) c= [:NAT,NAT:] :: according to RELAT_1:def 19 :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) or y in [:NAT,NAT:] )
assume y in rng (recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) ; :: thesis: y in [:NAT,NAT:]
then ex x being object st
( x in dom (recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) & (recSeqCart (a,b,x1,x2,x3,y1,y2,y3)) . x = y ) by FUNCT_1:def 3;
hence y in [:NAT,NAT:] by A5; :: thesis: verum

end;