let G be 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);
A3: the carrier of (product G) = product (carr G) by Th10;
then reconsider w = (0. (product G)) +* (i0,xi) as Element of product (carr G) by Th11;
A4: ||.((reproj (i,(0. (product G)))) . xi).|| = |.(normsequence (G,w)).| by Def4, PRVECT_2:7;
reconsider q = ||.xi.|| as Element of REAL ;
set q1 = <*q*>;
set y = 0* (len G);
A5: len (normsequence (G,w)) = len G by PRVECT_2:def 11;
A6: len (0* (len G)) = len G by CARD_1:def 7;
then A7: (((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0) = Replace ((0* (len G)),i0,q) by A1, FINSEQ_7:def 1;
then A8: len ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) = len (0* (len G)) by FINSEQ_7:5;
A9: len (0* (len G)) = len (Replace ((0* (len G)),i0,q)) 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)) ^ <*q*>) ^ ((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)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k )
assume A10: ( 1 <= k & k <= len (normsequence (G,w)) ) ; :: thesis: (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k
then reconsider k1 = k as Element of dom G by A5, FINSEQ_3:25;
A11: k1 in dom G ;
0. (product G) in the carrier of (product G) ;
then 0. (product G) in product (carr G) by Th10;
then consider g being Function such that
A12: ( 0. (product G) = g & dom g = dom (carr G) & ( for y being object st y in dom (carr G) holds
g . y in (carr G) . y ) ) by CARD_3:def 5;
A13: k in dom (0. (product G)) by A11, A12, Lm1;
A14: (normsequence (G,w)) . k = the normF of (G . k1) . (w . k1) by PRVECT_2:def 11;

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

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

then A16: (normsequence (G,w)) . k = ||.xi.|| by A14, A13, FUNCT_7:31;
(Replace ((0* (len G)),i0,q)) /. k = q by A15, A10, A5, A6, FINSEQ_7:8;
hence (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k by A16, A7, A10, A5, A6, A9, FINSEQ_4:15; :: thesis: verum

end;

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

then w . k1 = (0. (product G)) . k1 by FUNCT_7:32;
then A18: (normsequence (G,w)) . k = ||.(0. (G . k1)).|| by A14, Th14, A3;
(Replace ((0* (len G)),i0,q)) /. k = (0* (len G)) /. k by A17, A10, A5, A6, FINSEQ_7:10;
then (Replace ((0* (len G)),i0,q)) . k = (0* (len G)) /. k by A10, A5, A6, A9, FINSEQ_4:15;
then (Replace ((0* (len G)),i0,q)) . k = (0* (len G)) . k by A10, A5, A6, FINSEQ_4:15;
hence (normsequence (G,w)) . k = ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) . k by A18, A6, A1, FINSEQ_7:def 1; :: thesis: verum

end;

end;

end;

then A19: normsequence (G,w) = (((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0) by A6, A8, PRVECT_2:def 11;
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 A20: 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 A21: sqrt (Sum (sqr ((0* (len G)) /^ i0))) = 0 by EUCLID:7;
reconsider q2 = q ^2 as Element of REAL by XREAL_0:def 1;
sqr ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0)) = (sqr (((0* (len G)) | (i0 -' 1)) ^ <*q*>)) ^ (sqr ((0* (len G)) /^ i0)) by RVSUM_1:144
.= ((sqr ((0* (len G)) | (i0 -' 1))) ^ (sqr <*q*>)) ^ (sqr ((0* (len G)) /^ i0)) by RVSUM_1:144
.= ((sqr ((0* (len G)) | (i0 -' 1))) ^ <*(q ^2)*>) ^ (sqr ((0* (len G)) /^ i0)) by RVSUM_1:55 ;
then Sum (sqr ((((0* (len G)) | (i0 -' 1)) ^ <*q*>) ^ ((0* (len G)) /^ i0))) = (Sum ((sqr ((0* (len G)) | (i0 -' 1))) ^ <*q2*>)) + (Sum (sqr ((0* (len G)) /^ i0))) by RVSUM_1:75
.= ((Sum (sqr ((0* (len G)) | (i0 -' 1)))) + (q ^2)) + (Sum (sqr ((0* (len G)) /^ i0))) by RVSUM_1:74
.= q ^2 by A20, A21, RVSUM_1:86, SQUARE_1:24 ;
then ||.((reproj (i,(0. (product G)))) . xi).|| = |.q.| by A19, A4, COMPLEX1:72;
hence ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.|| by COMPLEX1:43; :: thesis: verum