let E, F be RealNormSpace; :: thesis: for z being Point of [:E,F:]
for x being Point of E
for y being Point of F st z = [x,y] holds
||.z.|| <= ||.x.|| + ||.y.||
let z be Point of [:E,F:]; :: thesis: for x being Point of E
for y being Point of F st z = [x,y] holds
||.z.|| <= ||.x.|| + ||.y.||
let x be Point of E; :: thesis: for y being Point of F st z = [x,y] holds
||.z.|| <= ||.x.|| + ||.y.||
let y be Point of F; :: thesis: ( z = [x,y] implies ||.z.|| <= ||.x.|| + ||.y.|| )
assume z = [x,y] ; :: thesis: ||.z.|| <= ||.x.|| + ||.y.||
then A2: ||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2)) by NDIFF_8:1;
((||.x.|| ^2) + (||.y.|| ^2)) + 0 <= ((||.x.|| ^2) + (||.y.|| ^2)) + ((2 * ||.x.||) * ||.y.||) by XREAL_1:7;
then sqrt ((||.x.|| ^2) + (||.y.|| ^2)) <= sqrt ((||.x.|| + ||.y.||) ^2) by SQUARE_1:26;
hence ||.z.|| <= ||.x.|| + ||.y.|| by A2, SQUARE_1:22; :: thesis: verum