set f = Cart4Id ;
set A = { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } ;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng Cart4Id or q in { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } )
assume q in rng Cart4Id ; :: thesis: q in { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 }
then consider a being Element of NATPLUS such that
A1: Cart4Id . a = q by FUNCT_2:113;
A2: Cart4Id . a = [a,a,a,a] by Def1;
a / a = 1 by XCMPLX_1:60;
then (((a / a) + (a / a)) + (a / a)) + (a / a) = 4 ;
hence q in { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } by A1, A2; :: thesis: verum