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