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