deffunc H₁( Rational, Rational) -> set = ((2 * ($1 |^ 3)) + ($1 * $2)) - 7;
set A = { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } ;
deffunc H₂( Nat) -> set = 7 / $1;
deffunc H₃( Nat) -> set = $1 - (98 / ($1 ^2));
deffunc H₄( Nat) -> object = [H₂($1),H₃($1)];
set D = NAT \ {0,1,2,3,4};
reconsider D = NAT \ {0,1,2,3,4} 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,2,3,4} by XBOOLE_0:def 5;
then A7: k <> 0 by ENUMSET1:def 3;
then A8: H₁(H₂(k),H₃(k)) = 0 by Th96;

now :: thesis: not H₃(k) <= 0

assume A9: H₃(k) <= 0 ; :: thesis: contradiction
(k - (98 / (k ^2))) * (k ^2) = (k * (k ^2)) - ((98 / (k ^2)) * (k ^2))
.= ((k * k) * k) - 98 by A7, XCMPLX_1:87 ;
then (((k * k) * k) - 98) + 98 <= 0 + 98 by A9, XREAL_1:6;
then k |^ 3 <= 98 by POLYEQ_5:2;
then k <= 4 by Th97;
then not not k = 0 & ... & not k = 4 ;
hence contradiction by A6, ENUMSET1:def 3; :: thesis: verum

end;

then H₄(k) in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } by A7, A8;
hence y in { [x,y] where x, y is positive Rational : H₁(x,y) = 0 } by A1, A5; :: thesis: verum

end;

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
A10: ( x1 in dom f & x2 in dom f ) and
A11: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of D by A10, PARTFUN1:def 2;
( f . x1 = H₄(x1) & f . x2 = H₄(x2) ) by A1;
then H₂(x1) = H₂(x2) by A11, XTUPLE_0:1;
hence x1 = x2 by XCMPLX_1:201; :: thesis: verum

end;

hence { [x,y] where x, y is positive Rational : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } is infinite by A2, A3, CARD_1:59; :: thesis: verum