let X, Y be RealNormSpace; for x being Point of X
for y being Point of Y holds
( ||.x.|| <= ||.[x,y].|| & ||.y.|| <= ||.[x,y].|| )
let x be Point of X; for y being Point of Y holds
( ||.x.|| <= ||.[x,y].|| & ||.y.|| <= ||.[x,y].|| )
let y be Point of Y; ( ||.x.|| <= ||.[x,y].|| & ||.y.|| <= ||.[x,y].|| )
consider w being Element of REAL 2 such that
A1:
( w = <*||.x.||,||.y.||*> & ||.[x,y].|| = |.w.| )
by PRVECT_3:18;
(proj (1,2)) . w =
w . 1
by PDIFF_1:def 1
.=
||.x.||
by A1, FINSEQ_1:44
;
then
|.||.x.||.| <= |.w.|
by PDIFF_8:5;
hence
||.x.|| <= ||.[x,y].||
by A1, ABSVALUE:def 1; ||.y.|| <= ||.[x,y].||
(proj (2,2)) . w =
w . 2
by PDIFF_1:def 1
.=
||.y.||
by A1, FINSEQ_1:44
;
then
|.||.y.||.| <= |.w.|
by PDIFF_8:5;
hence
||.y.|| <= ||.[x,y].||
by A1, ABSVALUE:def 1; verum