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