let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of (product G)
for y being Element of product (carr G)
for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <= ||.x.||
let i be Element of dom G; :: thesis: for x being Point of (product G)
for y being Element of product (carr G)
for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <= ||.x.||
let x be Point of (product G); :: thesis: for y being Element of product (carr G)
for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <= ||.x.||
let y be Element of product (carr G); :: thesis: for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <= ||.x.||
let xi be Point of (G . i); :: thesis: ( y = x & xi = y . i implies ||.xi.|| <= ||.x.|| )
reconsider n = len G as Element of NAT ;
assume that
A1: y = x and
A2: xi = y . i ; :: thesis: ||.xi.|| <= ||.x.||
A3: ((normsequence (G,y)) . i) ^2 = (sqr (normsequence (G,y))) . i by VALUED_1:11;
A4: for i being Nat st i in Seg n holds
0 <= (sqr (normsequence (G,y))) . i

proof

let i be Nat; :: thesis: ( i in Seg n implies 0 <= (sqr (normsequence (G,y))) . i )
assume i in Seg n ; :: thesis: 0 <= (sqr (normsequence (G,y))) . i
((normsequence (G,y)) . i) ^2 >= 0 by XREAL_1:63;
hence 0 <= (sqr (normsequence (G,y))) . i by VALUED_1:11; :: thesis: verum

end;

dom G = Seg n by FINSEQ_1:def 3;
then A5: ( 0 <= ((normsequence (G,y)) . i) ^2 & (sqr (normsequence (G,y))) . i <= Sum (sqr (normsequence (G,y))) ) by A4, REAL_NS1:7, XREAL_1:63;
||.xi.|| = (normsequence (G,y)) . i by A2, Def11;
then sqrt ((sqr (normsequence (G,y))) . i) = (normsequence (G,y)) . i by A3, NORMSP_1:4, SQUARE_1:22;
then A6: ||.xi.|| = sqrt ((sqr (normsequence (G,y))) . i) by A2, Def11;
||.x.|| = |.(normsequence (G,y)).| by A1, Th7;
hence ||.xi.|| <= ||.x.|| by A3, A5, A6, SQUARE_1:26; :: thesis: verum