let G be RealNormSpace-Sequence; :: thesis: for x, y being Point of (product G)
for Z, x0 being Element of product (carr G)
for X being set st Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) holds
||.y.|| <= ||.x.||
let x, y be Point of (product G); :: thesis: for Z, x0 being Element of product (carr G)
for X being set st Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) holds
||.y.|| <= ||.x.||
let Z, x0 be Element of product (carr G); :: thesis: for X being set st Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) holds
||.y.|| <= ||.x.||
let X be set ; :: thesis: ( Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) implies ||.y.|| <= ||.x.|| )
assume A1: ( Z = 0. (product G) & x0 = x & y = Z +* (x0 | X) ) ; :: thesis: ||.y.|| <= ||.x.||
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 )

proof

let k be Element of NAT ; :: thesis: ( k in Seg (len Ny) implies ( 0 <= Ny . k & Ny . k <= Nx . k ) )
assume A5: k in Seg (len Ny) ; :: thesis: ( 0 <= Ny . k & Ny . k <= Nx . k )
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: Ny . k <= Nx . k
A9: Nx . k = ||.xk.|| by PRVECT_2:def 11;

per cases ( k1 in X or not k1 in X ) ;

suppose k1 in X ; :: thesis: Ny . k <= Nx . k

then A10: k1 in dom (x0 | X) by A6, RELAT_1:57;
then y0 . k1 = (x0 | X) . k1 by A1, FUNCT_4:13;
then y0 . k1 = x0 . k1 by A10, FUNCT_1:47;
hence Ny . k <= Nx . k by A7, PRVECT_2:def 11; :: thesis: verum

end;

suppose not k1 in X ; :: thesis: Ny . k <= Nx . k

then not k1 in dom (x0 | X) ;
then y0 . k1 = Z . k1 by A1, FUNCT_4:11;
then y0 . k1 = 0. (G . k1) by A1, Th14;
hence Ny . k <= Nx . k by A8, A9; :: thesis: verum

end;

end;

end;

hence ||.y.|| <= ||.x.|| by A2, A3, A4, PRVECT_2:2; :: thesis: verum