reconsider x = x, y = y, z = z as Element of REAL by XREAL_0:def 1;
<*x,y,z*> is Element of REAL 3 by FINSEQ_2:104;
hence <*x,y,z*> is Element of REAL 3 ; :: thesis: verum