let X, Y be RealNormSpace; :: 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:18; :: thesis: verum

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:18; :: thesis: verum