deffunc H1( Complex, Complex) -> set = (((3 * ($1 ^2)) + (3 * $1)) - ($2 ^2)) + 1;
set A = { [x,y] where x, y is positive Nat : H1(x,y) = 0 } ;
A1: H1(7,13) = 0 ;
then [7,13] 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 = ((7 * $1) + (4 * $2)) + 3;
deffunc H3( Real, Real) -> set = ((12 * $1) + (7 * $2)) + 6;
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 (7,13,7,4,3,12,7,6);
A2: dom (recSeqCart (7,13,7,4,3,12,7,6)) = NAT by PARTFUN1:def 2;
defpred S2[ Nat] means (recSeqCart (7,13,7,4,3,12,7,6)) . $1 in A;
(recSeqCart (7,13,7,4,3,12,7,6)) . 0 = [7,13] by NUMBER08:def 10;
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 (7,13,7,4,3,12,7,6)) . a = [x,y] & H1(x,y) = 0 ) ;
set m = ((recSeqCart (7,13,7,4,3,12,7,6)) . a) `1 ;
set n = ((recSeqCart (7,13,7,4,3,12,7,6)) . a) `2 ;
A6: (recSeqCart (7,13,7,4,3,12,7,6)) . (a + 1) = [H2(((recSeqCart (7,13,7,4,3,12,7,6)) . a) `1 ,((recSeqCart (7,13,7,4,3,12,7,6)) . a) `2 ),H3(((recSeqCart (7,13,7,4,3,12,7,6)) . a) `1 ,((recSeqCart (7,13,7,4,3,12,7,6)) . a) `2 )] by NUMBER08:def 10;
H1(H2(((recSeqCart (7,13,7,4,3,12,7,6)) . a) `1 ,((recSeqCart (7,13,7,4,3,12,7,6)) . a) `2 ),H3(((recSeqCart (7,13,7,4,3,12,7,6)) . a) `1 ,((recSeqCart (7,13,7,4,3,12,7,6)) . a) `2 )) = 0 by A5;
hence S2[a + 1] by A6; :: thesis: verum
end;
A7: for a being Nat holds S2[a] from NAT_1:sch 2(A3, A4);
 A8: rng (recSeqCart (7,13,7,4,3,12,7,6)) c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (recSeqCart (7,13,7,4,3,12,7,6)) or y in A )
assume y in rng (recSeqCart (7,13,7,4,3,12,7,6)) ; :: thesis: y in A
then ex k being object st
( k in dom (recSeqCart (7,13,7,4,3,12,7,6)) & (recSeqCart (7,13,7,4,3,12,7,6)) . k = y ) by FUNCT_1:def 3;
hence y in A by A7; :: thesis: verum
end;
recSeqCart (7,13,7,4,3,12,7,6) is one-to-one by NUMBER08:92;
hence { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } is infinite by A2, A8, CARD_1:59; :: thesis: verum