set AP = { <*x,y,z*> where x, y, z is Real : x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP } ;
reconsider x = 1 as Nat ;
reconsider y = (5 * x) + 2 as Nat ;
reconsider z = (7 * x) + 3 as Nat ;
x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP ;
then <*1,((5 * 1) + 2),((7 * 1) + 3)*> in { <*x,y,z*> where x, y, z is Real : x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP } ;
then reconsider AP = { <*x,y,z*> where x, y, z is Real : x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP } as non empty set ;
defpred S₁[ Element of REAL , Element of AP] means $2 = <*$1,((5 * $1) + 2),((7 * $1) + 3)*>;
AA: for x being Element of REAL ex y being Element of AP st S₁[x,y]

proof

let x be Element of REAL ; :: thesis: ex y being Element of AP st S₁[x,y]
set y = (5 * x) + 2;
set z = (7 * x) + 3;
x * (x + 1),((5 * x) + 2) * (((5 * x) + 2) + 1),((7 * x) + 3) * (((7 * x) + 3) + 1) form_an_AP ;
then <*x,((5 * x) + 2),((7 * x) + 3)*> in AP ;
then reconsider yy = <*x,((5 * x) + 2),((7 * x) + 3)*> as Element of AP ;
take yy ; :: thesis: S₁[x,yy]
thus S₁[x,yy] ; :: thesis: verum

end;

consider f being Function of REAL,AP such that
A0: for x being Element of REAL holds S₁[x,f . x] from FUNCT_2:sch 3(AA);
A1: dom f is infinite by FUNCT_2:def 1;
for x1, x2 being object st x1 in REAL & x2 in REAL & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in REAL & x2 in REAL & f . x1 = f . x2 implies x1 = x2 )
assume B0: ( x1 in REAL & x2 in REAL & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider xx1 = x1, xx2 = x2 as Element of REAL ;
f . xx1 = <*xx1,((5 * xx1) + 2),((7 * xx1) + 3)*> by A0;
then <*xx1,((5 * xx1) + 2),((7 * xx1) + 3)*> = <*xx2,((5 * xx2) + 2),((7 * xx2) + 3)*> by A0, B0;
hence x1 = x2 by FINSEQ_1:78; :: thesis: verum

end;

then A2: f is one-to-one by FUNCT_2:19;
rng f c= AP by RELAT_1:def 19;
hence { <*x,y,z*> where x, y, z is Real : x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP } is infinite by A1, A2, CARD_1:59; :: thesis: verum