let X, Y be RealLinearSpace; :: thesis: for x being Point of X
for y being Point of Y holds [x,y] is Point of [:X,Y:]
let x be Point of X; :: thesis: for y being Point of Y holds [x,y] is Point of [:X,Y:]
let y be Point of Y; :: thesis: [x,y] is Point of [:X,Y:]
[x,y] is set by TARSKI:1;
hence [x,y] is Point of [:X,Y:] by PRVECT_3:9; :: thesis: verum