set A = { [x,y,z] where x, y, z is positive Nat : (1 + (x ^2)) + (y ^2) = z ^2 } ;
deffunc H₁( Nat) -> set = 2 * $1;
deffunc H₂( Nat) -> Element of omega = 2 * ($1 ^2);
deffunc H₃( Nat) -> Element of omega = (2 * ($1 ^2)) + 1;
deffunc H₄( Nat) -> object = [H₁($1),H₂($1),H₃($1)];
consider f being ManySortedSet of NATPLUS such that
A1: for d being Element of NATPLUS holds f . d = H₄(d) from PBOOLE:sch 5();
A2: dom f = NATPLUS by PARTFUN1:def 2;
A3: rng f c= { [x,y,z] where x, y, z is positive Nat : (1 + (x ^2)) + (y ^2) = z ^2 }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { [x,y,z] where x, y, z is positive Nat : (1 + (x ^2)) + (y ^2) = z ^2 } )
assume y in rng f ; :: thesis: y in { [x,y,z] where x, y, z is positive Nat : (1 + (x ^2)) + (y ^2) = z ^2 }
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 NATPLUS by A4, PARTFUN1:def 2;
A6: (1 + (H₁(k) ^2)) + (H₂(k) ^2) = H₃(k) ^2 ;
H₄(k) = f . k by A1;
hence y in { [x,y,z] where x, y, z is positive Nat : (1 + (x ^2)) + (y ^2) = z ^2 } by A5, A6; :: 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
A7: ( x1 in dom f & x2 in dom f ) and
A8: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NATPLUS by A7, PARTFUN1:def 2;
( H₄(x1) = f . x1 & H₄(x2) = f . x2 ) by A1;
then H₁(x1) = H₁(x2) by A8, XTUPLE_0:3;
hence x1 = x2 ; :: thesis: verum

end;

hence { [x,y,z] where x, y, z is positive Nat : (1 + (x ^2)) + (y ^2) = z ^2 } is infinite by A2, A3, CARD_1:59; :: thesis: verum