consider x being Point of X, y being Point of Y such that
P1: z = [x,y] by PRVECT_3:18;
thus z `2 is Point of Y by P1; :: thesis: verum