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

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