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

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

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

dom G = Seg n
by FINSEQ_1:def 3;
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;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

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