let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of ()
for y being Element of product (carr G)
for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <=

let i be Element of dom G; :: thesis: for x being Point of ()
for y being Element of product (carr G)
for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <=

let x be Point of (); :: thesis: for y being Element of product (carr G)
for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <=

let y be Element of product (carr G); :: thesis: for xi being Point of (G . i) st y = x & xi = y . i holds
||.xi.|| <=

let xi be Point of (G . i); :: thesis: ( y = x & xi = y . i implies ||.xi.|| <= )
reconsider n = len G as Element of NAT ;
assume that
A1: y = x and
A2: xi = y . i ; :: thesis:
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 ;
||.xi.|| = (normsequence (G,y)) . i by ;
then sqrt ((sqr (normsequence (G,y))) . i) = (normsequence (G,y)) . i by ;
then A6: ||.xi.|| = sqrt ((sqr (normsequence (G,y))) . i) by ;
||.x.|| = |.(normsequence (G,y)).| by ;
hence ||.xi.|| <= by ; :: thesis: verum