deffunc H1( Complex, Complex) -> set = ((3 * ($1 ^2)) - (7 * ($2 ^2))) + 1;
set A = { [x,y] where x, y is positive Nat : H1(x,y) = 0 } ;
A1: H1(3,2) = 0 ;
then [3,2] in { [x,y] where x, y is positive Nat : H1(x,y) = 0 } ;
then reconsider A = { [x,y] where x, y is positive Nat : H1(x,y) = 0 } as non empty set ;
deffunc H2( Real, Real) -> set = ((55 * $1) + (84 * $2)) + 0;
deffunc H3( Real, Real) -> set = ((36 * $1) + (55 * $2)) + 0;
defpred S1[ object , Element of [:NAT,NAT:], Element of [:NAT,NAT:]] means $3 = [H2($2 `1 ,$2 `2 ),H3($2 `1 ,$2 `2 )];
set f = recSeqCart (3,2,55,84,0,36,55,0);
A2: dom (recSeqCart (3,2,55,84,0,36,55,0)) = NAT by PARTFUN1:def 2;
defpred S2[ Nat] means (recSeqCart (3,2,55,84,0,36,55,0)) . $1 in A;
(recSeqCart (3,2,55,84,0,36,55,0)) . 0 = [3,2] by Def10;
then A3: S2[ 0 ] by A1;
A4: for a being Nat st S2[a] holds
S2[a + 1]
proof
let a be Nat; :: thesis: ( S2[a] implies S2[a + 1] )
assume S2[a] ; :: thesis: S2[a + 1]
then consider x, y being positive Nat such that
A5: ( (recSeqCart (3,2,55,84,0,36,55,0)) . a = [x,y] & H1(x,y) = 0 ) ;
set m = ((recSeqCart (3,2,55,84,0,36,55,0)) . a) `1 ;
set n = ((recSeqCart (3,2,55,84,0,36,55,0)) . a) `2 ;
A6: (recSeqCart (3,2,55,84,0,36,55,0)) . (a + 1) = [H2(((recSeqCart (3,2,55,84,0,36,55,0)) . a) `1 ,((recSeqCart (3,2,55,84,0,36,55,0)) . a) `2 ),H3(((recSeqCart (3,2,55,84,0,36,55,0)) . a) `1 ,((recSeqCart (3,2,55,84,0,36,55,0)) . a) `2 )] by Def10;
A7: ( ((recSeqCart (3,2,55,84,0,36,55,0)) . a) `1 > 0 & ((recSeqCart (3,2,55,84,0,36,55,0)) . a) `2 > 0 ) by Th89;
H1(H2(((recSeqCart (3,2,55,84,0,36,55,0)) . a) `1 ,((recSeqCart (3,2,55,84,0,36,55,0)) . a) `2 ),H3(((recSeqCart (3,2,55,84,0,36,55,0)) . a) `1 ,((recSeqCart (3,2,55,84,0,36,55,0)) . a) `2 )) = 0 by A5;
hence S2[a + 1] by A6, A7; :: thesis: verum
end;
A8: for a being Nat holds S2[a] from NAT_1:sch 2(A3, A4);
 A9: rng (recSeqCart (3,2,55,84,0,36,55,0)) c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (recSeqCart (3,2,55,84,0,36,55,0)) or y in A )
assume y in rng (recSeqCart (3,2,55,84,0,36,55,0)) ; :: thesis: y in A
then ex k being object st
( k in dom (recSeqCart (3,2,55,84,0,36,55,0)) & (recSeqCart (3,2,55,84,0,36,55,0)) . k = y ) by FUNCT_1:def 3;
hence y in A by A8; :: thesis: verum
end;
recSeqCart (3,2,55,84,0,36,55,0) is one-to-one by Th92;
hence { [x,y] where x, y is positive Nat : ((3 * (x ^2)) - (7 * (y ^2))) + 1 = 0 } is infinite by A2, A9, CARD_1:59; :: thesis: verum