let G be non-trivial RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for xi being Element of (G . i) holds ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||
let i be Element of dom G; :: thesis: for xi being Element of (G . i) holds ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||
let xi be Element of (G . i); :: thesis: ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||
set j = len G;
reconsider i0 = i as Element of NAT ;
Seg (len G) = dom G by FINSEQ_1:def 3;
then A1: ( 1 <= i0 & i0 <= len G ) by FINSEQ_1:1;
set z = 0. (product G);
B3: (reproj (i,(0. (product G)))) . xi = (0. (product G)) +* (i,xi) by Def5;
ZZ: the carrier of (product G) = product (carr G) by LM001;
then reconsider w = (0. (product G)) +* (i0,xi) as Element of product (carr G) by LM003;
B4: ||.((reproj (i,(0. (product G)))) . xi).|| = |.(normsequence (G,w)).| by B3, PRVECT_2:7;
set q = ||.xi.||;
set q1 = <*||.xi.||*>;
set y = 0* (len G);
C1: len (normsequence (G,w)) = len G by PRVECT_2:def 11;
C2: len (0* (len G)) = len G by CARD_1:def 7;
then C4: (((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0) = Replace ((0* (len G)),i0,||.xi.||) by A1, FINSEQ_7:def 1;
then C3: len ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) = len (0* (len G)) by FINSEQ_7:5;
E2: len (0* (len G)) = len (Replace ((0* (len G)),i0,||.xi.||)) by FINSEQ_7:5;
for k being Nat st 1 <= k & k <= len (normsequence (G,w)) holds
(normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (normsequence (G,w)) implies (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) . k )
assume D0: ( 1 <= k & k <= len (normsequence (G,w)) ) ; :: thesis: (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) . k
then reconsider k1 = k as Element of dom G by C1, FINSEQ_3:25;
Y0: k1 in dom G ;
0. (product G) in the carrier of (product G) ;
then 0. (product G) in product (carr G) by LM001;
then consider g being Function such that
Y1: ( 0. (product G) = g & dom g = dom (carr G) & ( for y being set st y in dom (carr G) holds
g . y in (carr G) . y ) ) by CARD_3:def 5;
Z2: k in dom (0. (product G)) by Y0, Y1, ZE;
F4: k in Seg (len (0* (len G))) by D0, C1, C2, FINSEQ_1:1;
D1: (normsequence (G,w)) . k = the normF of (G . k1) . (w . k1) by PRVECT_2:def 11;

per cases ( k = i0 or k <> i0 ) ;

suppose D2: k = i0 ; :: thesis: (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) . k

then D3: (normsequence (G,w)) . k = ||.xi.|| by D1, Z2, FUNCT_7:31;
(Replace ((0* (len G)),i0,||.xi.||)) /. k = ||.xi.|| by D2, D0, C1, C2, FINSEQ_7:8;
hence (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) . k by D3, C4, D0, C1, C2, E2, FINSEQ_4:15; :: thesis: verum

end;

suppose F1: k <> i0 ; :: thesis: (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) . k

then w . k1 = (0. (product G)) . k1 by FUNCT_7:32;
then F2: (normsequence (G,w)) . k = ||.(0. (G . k1)).|| by D1, ZR1, ZZ;
(Replace ((0* (len G)),i0,||.xi.||)) /. k = (0* (len G)) /. k by F1, D0, C1, C2, FINSEQ_7:10;
then (Replace ((0* (len G)),i0,||.xi.||)) . k = (0* (len G)) /. k by D0, C1, C2, E2, FINSEQ_4:15;
then (Replace ((0* (len G)),i0,||.xi.||)) . k = (0* (len G)) . k by D0, C1, C2, FINSEQ_4:15;
hence (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) . k by F2, C4, C2, F4, FINSEQ_2:57; :: thesis: verum

end;

end;

end;

then A4: normsequence (G,w) = (((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0) by C1, C2, C3, FINSEQ_1:14;
sqrt (Sum (sqr ((0* (len G)) | (i0 -' 1)))) = |.(0* (i0 -' 1)).| by A1, PDIFF_7:2;
then sqrt (Sum (sqr ((0* (len G)) | (i0 -' 1)))) = 0 by EUCLID:7;
then A5: Sum (sqr ((0* (len G)) | (i0 -' 1))) = 0 by RVSUM_1:86, SQUARE_1:24;
sqrt (Sum (sqr ((0* (len G)) /^ i0))) = |.(0* ((len G) -' i0)).| by PDIFF_7:3;
then A6: sqrt (Sum (sqr ((0* (len G)) /^ i0))) = 0 by EUCLID:7;
sqr ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0)) = (sqr (((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>)) ^ (sqr ((0* (len G)) /^ i0)) by TOPREAL7:10
.= ((sqr ((0* (len G)) | (i0 -' 1))) ^ (sqr <*||.xi.||*>)) ^ (sqr ((0* (len G)) /^ i0)) by TOPREAL7:10
.= ((sqr ((0* (len G)) | (i0 -' 1))) ^ <*(||.xi.|| ^2)*>) ^ (sqr ((0* (len G)) /^ i0)) by RVSUM_1:55 ;
then Sum (sqr ((((0* (len G)) | (i0 -' 1)) ^ <*||.xi.||*>) ^ ((0* (len G)) /^ i0))) = (Sum ((sqr ((0* (len G)) | (i0 -' 1))) ^ <*(||.xi.|| ^2)*>)) + (Sum (sqr ((0* (len G)) /^ i0))) by RVSUM_1:75
.= ((Sum (sqr ((0* (len G)) | (i0 -' 1)))) + (||.xi.|| ^2)) + (Sum (sqr ((0* (len G)) /^ i0))) by RVSUM_1:74
.= ||.xi.|| ^2 by A5, A6, RVSUM_1:86, SQUARE_1:24 ;
then ||.((reproj (i,(0. (product G)))) . xi).|| = |.||.xi.||.| by A4, B4, COMPLEX1:72;
hence ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.|| by COMPLEX1:43; :: thesis: verum