let X, Y be RealNormSpace; for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )
let x be Point of X; for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )
let y be Point of Y; for z being Point of [:X,Y:] st z = [x,y] holds
( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )
let z be Point of [:X,Y:]; ( z = [x,y] implies ( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| ) )
assume
z = [x,y]
; ( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )
then A2:
||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))
by LMNR0;
0 + (||.x.|| ^2) <= (||.x.|| ^2) + (||.y.|| ^2)
by XREAL_1:6;
then
sqrt (||.x.|| ^2) <= sqrt ((||.x.|| ^2) + (||.y.|| ^2))
by SQUARE_1:26;
hence
||.x.|| <= ||.z.||
by A2, SQUARE_1:22; ||.y.|| <= ||.z.||
0 + (||.y.|| ^2) <= (||.x.|| ^2) + (||.y.|| ^2)
by XREAL_1:6;
then
sqrt (||.y.|| ^2) <= sqrt ((||.x.|| ^2) + (||.y.|| ^2))
by SQUARE_1:26;
hence
||.y.|| <= ||.z.||
by A2, SQUARE_1:22; verum