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 Element of NAT st i in Seg n holds
0 <= (sqr (normsequence G,y)) . i

proof

let i be Element of 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:65;
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:65;
||.xi.|| = (normsequence G,y) . i by A2, Def11;
then sqrt ((sqr (normsequence G,y)) . i) = (normsequence G,y) . i by A3, NORMSP_1:8, SQUARE_1:89;
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:94; :: thesis: verum