deffunc H1( Nat, Nat) -> set = ((($1 - 1) ^2) + (($1 + 1) ^2)) - (($2 ^2) + 1);
set A = { [x,y] where x, y is positive Nat : H1(x,y) = 0 } ;
A1: H1(2,3) = 0 ;
then [2,3] 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( Nat, Nat) -> Element of omega = ((3 * $1) + (2 * $2)) + 0;
deffunc H3( Nat, Nat) -> Element of omega = ((4 * $1) + (3 * $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 (2,3,3,2,0,4,3,0);
A2: dom (recSeqCart (2,3,3,2,0,4,3,0)) = NAT by PARTFUN1:def 2;
defpred S2[ Nat] means (recSeqCart (2,3,3,2,0,4,3,0)) . $1 in A;
(recSeqCart (2,3,3,2,0,4,3,0)) . 0 = [2,3] 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 (2,3,3,2,0,4,3,0)) . a = [x,y] & H1(x,y) = 0 ) ;
set m = ((recSeqCart (2,3,3,2,0,4,3,0)) . a) `1 ;
set n = ((recSeqCart (2,3,3,2,0,4,3,0)) . a) `2 ;
reconsider m = ((recSeqCart (2,3,3,2,0,4,3,0)) . a) `1 , n = ((recSeqCart (2,3,3,2,0,4,3,0)) . a) `2 as Nat by A5;
A6: (recSeqCart (2,3,3,2,0,4,3,0)) . (a + 1) = [H2(m,n),H3(m,n)] by Def10;
A7: ( m > 0 & n > 0 ) by Th89;
H1(H2(m,n),H3(m,n)) = 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 (2,3,3,2,0,4,3,0)) c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (recSeqCart (2,3,3,2,0,4,3,0)) or y in A )
assume y in rng (recSeqCart (2,3,3,2,0,4,3,0)) ; :: thesis: y in A
then ex k being object st
( k in dom (recSeqCart (2,3,3,2,0,4,3,0)) & (recSeqCart (2,3,3,2,0,4,3,0)) . k = y ) by FUNCT_1:def 3;
hence y in A by A8; :: thesis: verum
end;
A10: recSeqCart (2,3,3,2,0,4,3,0) is one-to-one by Th92;
defpred S3[ Nat, Nat] means (($1 - 1) ^2) + (($1 + 1) ^2) = ($2 ^2) + 1;
set B = { [x,y] where x, y is positive Nat : S3[x,y] } ;
A = { [x,y] where x, y is positive Nat : S3[x,y] }
proof
thus A c= { [x,y] where x, y is positive Nat : S3[x,y] } :: according to XBOOLE_0:def 10 :: thesis: { [x,y] where x, y is positive Nat : S3[x,y] } c= A
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in { [x,y] where x, y is positive Nat : S3[x,y] } )
assume a in A ; :: thesis: a in { [x,y] where x, y is positive Nat : S3[x,y] }
then ex x, y being positive Nat st
( a = [x,y] & H1(x,y) = 0 ) ;
hence a in { [x,y] where x, y is positive Nat : S3[x,y] } ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is positive Nat : S3[x,y] } or a in A )
assume a in { [x,y] where x, y is positive Nat : S3[x,y] } ; :: thesis: a in A
then consider x, y being positive Nat such that
A11: a = [x,y] and
A12: S3[x,y] ;
 H1(x,y) = 0 by A12;
hence a in A by A11; :: thesis: verum
end;
hence { [x,y] where x, y is positive Nat : ((x - 1) ^2) + ((x + 1) ^2) = (y ^2) + 1 } is infinite by A2, A9, A10, CARD_1:59; :: thesis: verum