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
||.z.|| <= ||.x.|| + ||.y.||
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
||.z.|| <= ||.x.|| + ||.y.||
let y be Point of Y; :: thesis: for z being Point of [:X,Y:] st z = [x,y] holds
||.z.|| <= ||.x.|| + ||.y.||
let z be Point of [:X,Y:]; :: thesis: ( z = [x,y] implies ||.z.|| <= ||.x.|| + ||.y.|| )
assume z = [x,y] ; :: thesis: ||.z.|| <= ||.x.|| + ||.y.||
then A1: ||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2)) by NDIFF_8:1;
( |.||.x.||.| = ||.x.|| & |.||.y.||.| = ||.y.|| ) by COMPLEX1:43, NORMSP_1:4;
hence ||.z.|| <= ||.x.|| + ||.y.|| by A1, COMPLEX1:78; :: thesis: verum