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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { [x,y,z,t] where x, y, z, t is Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 1 } )
assume y in rng f ; :: thesis: y in { [x,y,z,t] where x, y, z, t is Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 1 }
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 GreaterOrEqualsNumbers 2 by A4, PARTFUN1:def 2;
set q = (k ^2) - 1;
A6: H₁(k) / H₂(k) = ((- 1) * (k ^2)) / (((k ^2) - 1) * (k ^2))
.= (- 1) / ((k ^2) - 1) by XCMPLX_1:91 ;
A7: H₃(k) / H₄(k) = (((k ^2) - 1) ^2) / ((- k) * ((k ^2) - 1))
.= ((k ^2) - 1) / (- k) by XCMPLX_1:91
.= - (((k ^2) - 1) / k) by XCMPLX_1:188 ;
A8: H₄(k) / H₁(k) = (k * ((k ^2) - 1)) / (k ^2) by XCMPLX_1:191
.= ((k ^2) - 1) / k by XCMPLX_1:91 ;
((k ^2) / ((k ^2) - 1)) - (1 / ((k ^2) - 1)) = ((k ^2) - 1) / ((k ^2) - 1)
.= 1 by XCMPLX_1:60 ;
then (((H₁(k) / H₂(k)) + (H₂(k) / H₃(k))) + (H₃(k) / H₄(k))) + (H₄(k) / H₁(k)) = 1 by A6, A7, A8, XCMPLX_1:91;
then H₅(k) in { [x,y,z,t] where x, y, z, t is Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 1 } ;
hence y in { [x,y,z,t] where x, y, z, t is Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 1 } 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
A9: ( x1 in dom f & x2 in dom f ) and
A10: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of GreaterOrEqualsNumbers 2 by A9, PARTFUN1:def 2;
( f . x1 = H₅(x1) & f . x2 = H₅(x2) ) by A1;
then H₁(x1) = H₁(x2) by A10, XTUPLE_0:5;
then ( x1 = x2 or x1 = - x2 ) by SQUARE_1:40;
hence x1 = x2 ; :: thesis: verum

end;

hence { [x,y,z,t] where x, y, z, t is Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 1 } is infinite by A2, A3, CARD_1:59; :: thesis: verum