let X, Y be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: for z being Point of [:X,Y:] st z = [x,y] holds
( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )
let z be Point of [:X,Y:]; :: thesis: ( z = [x,y] implies ( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| ) )
assume z = [x,y] ; :: thesis: ( ||.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; :: thesis: ||.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; :: thesis: verum