let G be RealNormSpace-Sequence; :: thesis:
let x, y be Point of (product G); :: thesis:
let Z, x0 be Element of product (carr G); :: thesis:
let X be set ; :: thesis:
assume A1: ( Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) ) ; :: thesis:
reconsider y0 = y as Element of product (carr G) by Th10;
A2: ||.y.|| = (productnorm G) . y by PRVECT_2:def 13
.= |.(normsequence (G,y0)).| by PRVECT_2:def 12 ;
A3: ||.x.|| = (productnorm G) . x by PRVECT_2:def 13
.= |.(normsequence (G,x0)).| by A1, PRVECT_2:def 12 ;
reconsider Ny = normsequence (G,y0) as len G -element FinSequence of REAL ;
reconsider Nx = normsequence (G,x0) as len G -element FinSequence of REAL ;
A4: ( len Nx = len G & len Ny = len G ) by CARD_1:def 7;
for k being Element of NAT st k in Seg (len Ny) holds
( 0 <= Ny . k & Ny . k <= Nx . k )

let k be Element of NAT ; :: thesis:
assume A5: k in Seg (len Ny) ; :: thesis:
then reconsider k1 = k as Element of dom G by CARD_1:def 7, FINSEQ_1:def 3;
x0 is Element of the carrier of (product G) by Th10;
then reconsider xx = x0 as len G -element FinSequence ;
dom xx = Seg (len G) by FINSEQ_1:89;
then A6: k in dom x0 by A5, CARD_1:def 7;
reconsider yk = y0 . k1, xk = x0 . k1 as Element of the carrier of (G . k1) ;
A7: Nx . k = the normF of (G . k1) . (x0 . k1) by PRVECT_2:def 11;
A8: Ny . k = ||.yk.|| by PRVECT_2:def 11;
hence 0 <= Ny . k ; :: thesis:
A9: Nx . k = ||.xk.|| by PRVECT_2:def 11;

end;

end;