deffunc H₁( Complex, Complex) -> set = ($1 * ($1 + 1)) - ((4 * $2) * ($2 + 1));
set A = { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } ;
deffunc H₂( Nat) -> set = (((3 |^ $1) - (3 to_power (1 - $1))) - 2) / 4;
deffunc H₃( Nat) -> set = (((3 |^ $1) + (3 to_power (1 - $1))) - 4) / 8;
deffunc H₄( Nat) -> object = [H₂($1),H₃($1)];
set D = NAT \ {0,1};
reconsider D = NAT \ {0,1} as infinite natural-membered set ;
consider f being ManySortedSet of D such that
A1: for d being Element of D holds f . d = H₄(d) from PBOOLE:sch 5();
A2: dom f = D by PARTFUN1:def 2;
A3: rng f c= { [x,y] where x, y is positive Rational : H₁(x,y) = 0 }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } )
assume y in rng f ; :: thesis: y in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 }
then consider k being object such that
A4: k in dom f and
A5: f . k = y by FUNCT_1:def 3;
reconsider k = k as Element of D by A4, PARTFUN1:def 2;
A6: not k in {0,1} by XBOOLE_0:def 5;

A7: now :: thesis: not k <= 1

assume k <= 1 ; :: thesis: contradiction
then not not k = 0 & ... & not k = 1 ;
hence contradiction by A6, TARSKI:def 2; :: thesis: verum

end;

H₂(k) * (H₂(k) + 1) = (4 * H₃(k)) * (H₃(k) + 1) by Th102;
then A8: H₁(H₂(k),H₃(k)) = 0 ;
A9: ((3 |^ k) - (3 to_power (1 - k))) - 2 > 0 by A7, Th100;
((3 |^ k) + (3 to_power (1 - k))) - 4 > 0 by A7, Th101;
then H₄(k) in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } by A8, A9;
hence y in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } by A1, A5; :: thesis: verum

end;

A10: f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A11: ( x1 in dom f & x2 in dom f ) and
A12: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of D by A11, PARTFUN1:def 2;
( f . x1 = H₄(x1) & f . x2 = H₄(x2) ) by A1;
then A13: H₂(x1) = H₂(x2) by A12, XTUPLE_0:1;

now :: thesis: not x1 <> x2

assume x1 <> x2 ; :: thesis: contradiction
then ( x1 < x2 or x1 > x2 ) by XXREAL_0:1;
hence contradiction by A13, Th103; :: thesis: verum

end;

hence x1 = x2 ; :: thesis: verum

end;

defpred S₁[ Complex, Complex] means $1 * ($1 + 1) = (4 * $2) * ($2 + 1);
set B = { [x,y] where x, y is positive Rational : S₁[x,y] } ;
{ [x,y] where x, y is positive Rational : H₁(x,y) = 0 } = { [x,y] where x, y is positive Rational : S₁[x,y] }

proof

thus { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } c= { [x,y] where x, y is positive Rational : S₁[x,y] } :: according to XBOOLE_0:def 10 :: thesis: { [x,y] where x, y is positive Rational : S₁[x,y] } c= { [x,y] where x, y is positive Rational : H₁(x,y) = 0 }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } or a in { [x,y] where x, y is positive Rational : S₁[x,y] } )
assume a in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } ; :: thesis: a in { [x,y] where x, y is positive Rational : S₁[x,y] }
then ex x, y being positive Rational st
( a = [x,y] & H₁(x,y) = 0 ) ;
hence a in { [x,y] where x, y is positive Rational : S₁[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 Rational : S₁[x,y] } or a in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } )
assume a in { [x,y] where x, y is positive Rational : S₁[x,y] } ; :: thesis: a in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 }
then consider x, y being positive Rational such that
A14: a = [x,y] and
A15: S₁[x,y] ;
H₁(x,y) = 0 by A15;
hence a in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } by A14; :: thesis: verum

end;

hence { [x,y] where x, y is positive Rational : x * (x + 1) = (4 * y) * (y + 1) } is infinite by A2, A3, A10, CARD_1:59; :: thesis: verum