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