let G be RealNormSpace-Sequence; :: thesis: product G is RealNormSpace-like
let x, y be Point of (product G); :: according to NORMSP_1:def 2 :: thesis: for b₁ being Element of REAL holds
( ( not ||.x.|| = 0 or x = 0. (product G) ) & ( not x = 0. (product G) or ||.x.|| = 0 ) & ||.(b₁ * x).|| = (abs b₁) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; :: thesis: ( ( not ||.x.|| = 0 or x = 0. (product G) ) & ( not x = 0. (product G) or ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider n = len G as Element of NAT ;
A1: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;
A2: len G = len (carr G) by Def4;
A3: ( ||.x.|| = 0 implies x = 0. (product G) )

proof

assume A4: ||.x.|| = 0 ; :: thesis: x = 0. (product G)
reconsider z = x as Element of product (carr G) by A1;

now

let i be Element of dom (carr G); :: thesis: z . i = the ZeroF of (G . i)
||.x.|| = |.(normsequence G,z).| by Th7;
then A5: normsequence G,z = 0* n by A4, EUCLID:11;
dom (carr G) = Seg (len (carr G)) by FINSEQ_1:def 3;
then dom (carr G) = Seg (len G) by Def4;
then A6: (normsequence G,z) . i = 0 by A5, FUNCOP_1:13;
reconsider i0 = i as Element of dom G by A2, FINSEQ_3:31;
(carr G) . i0 = the carrier of (G . i0) by Def4;
then reconsider zzi0 = z . i0 as Element of (G . i0) by CARD_3:18;
||.zzi0.|| = 0 by A6, Def11;
then z . i = 0. (G . i) by NORMSP_1:def 2;
hence z . i = the ZeroF of (G . i) ; :: thesis: verum

end;

hence x = 0. (product G) by A1, Def7; :: thesis: verum

end;

A7: ( x = 0. (product G) implies ||.x.|| = 0 )

proof

assume A8: x = 0. (product G) ; :: thesis: ||.x.|| = 0
reconsider z = x as Element of product (carr G) by A1;
A9: for i being Element of dom (carr G) holds (normsequence G,z) . i = 0

proof

let i be Element of dom (carr G); :: thesis: (normsequence G,z) . i = 0
reconsider i0 = i as Element of dom G by A2, FINSEQ_3:31;
(carr G) . i0 = the carrier of (G . i0) by Def4;
then reconsider zi0 = z . i0 as Element of (G . i0) by CARD_3:18;
z . i = 0. (G . i) by A1, A8, Def7;
then ||.zi0.|| = 0 ;
hence (normsequence G,z) . i = 0 by Def11; :: thesis: verum

end;

for i being Element of NAT st i in dom (sqr (normsequence G,z)) holds
(sqr (normsequence G,z)) . i = 0

proof

let i be Element of NAT ; :: thesis: ( i in dom (sqr (normsequence G,z)) implies (sqr (normsequence G,z)) . i = 0 )
assume A10: i in dom (sqr (normsequence G,z)) ; :: thesis: (sqr (normsequence G,z)) . i = 0
len (normsequence G,z) = len G by Def11;
then A11: dom (normsequence G,z) = dom G by FINSEQ_3:31;
dom (carr G) = dom G by A2, FINSEQ_3:31;
then dom (sqr (normsequence G,z)) = dom (carr G) by A11, VALUED_1:11;
then ((normsequence G,z) . i) ^2 = 0 ^2 by A9, A10;
hence (sqr (normsequence G,z)) . i = 0 by VALUED_1:11; :: thesis: verum

end;

then |.(normsequence G,z).| = 0 by Th3, SQUARE_1:82;
hence ||.x.|| = 0 by Th7; :: thesis: verum

end;

reconsider z = x as Element of product (carr G) by A1;
reconsider ax = a * x as Element of product (carr G) by A1;
A12: ( len (normsequence G,ax) = n & len ((abs a) * (normsequence G,z)) = n ) by FINSEQ_1:def 18;
then X: dom (normsequence G,ax) = Seg n by FINSEQ_1:def 3;
for i being Nat st i in dom (normsequence G,ax) holds
(normsequence G,ax) . i = ((abs a) * (normsequence G,z)) . i

proof

let i be Nat; :: thesis: ( i in dom (normsequence G,ax) implies (normsequence G,ax) . i = ((abs a) * (normsequence G,z)) . i )
assume i in dom (normsequence G,ax) ; :: thesis: (normsequence G,ax) . i = ((abs a) * (normsequence G,z)) . i
then reconsider i0 = i as Element of dom G by X, FINSEQ_1:def 3;
( (carr G) . i0 = the carrier of (G . i0) & dom (carr G) = dom G ) by A2, Def4, FINSEQ_3:31;
then reconsider axi0 = ax . i0, zi0 = z . i0 as Element of (G . i0) by CARD_3:18;
reconsider i1 = i0 as Element of dom (carr G) by A2, FINSEQ_3:31;
([:(multop G):] . a,z) . i1 = ((multop G) . i1) . a,zi0 by Def2;
then axi0 = a * zi0 by A1, Def8;
then ||.axi0.|| = (abs a) * ||.zi0.|| by NORMSP_1:def 2;
then ||.axi0.|| = (abs a) * ((normsequence G,z) . i0) by Def11;
then ||.axi0.|| = ((abs a) * (normsequence G,z)) . i0 by RVSUM_1:66;
hence (normsequence G,ax) . i = ((abs a) * (normsequence G,z)) . i by Def11; :: thesis: verum

end;

then |.(normsequence G,ax).| = |.((abs a) * (normsequence G,z)).| by A12, FINSEQ_2:10;
then A13: |.(normsequence G,ax).| = (abs (abs a)) * |.(normsequence G,z).| by EUCLID:14;
reconsider z = x + y as Element of product (carr G) by A1;
reconsider xx = x, yy = y as Element of product (carr G) by A1;
A14: ( ||.(x + y).|| = |.(normsequence G,z).| & ||.x.|| = |.(normsequence G,xx).| & ||.y.|| = |.(normsequence G,yy).| ) by Th7;
A15: len (normsequence G,z) = n by Def11;
then A16: len (normsequence G,z) = len ((normsequence G,xx) + (normsequence G,yy)) by FINSEQ_1:def 18;
for i being Element of NAT st i in Seg n holds
( 0 <= (normsequence G,z) . i & (normsequence G,z) . i <= ((normsequence G,xx) + (normsequence G,yy)) . i )

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( 0 <= (normsequence G,z) . i & (normsequence G,z) . i <= ((normsequence G,xx) + (normsequence G,yy)) . i ) )
assume A17: i in Seg n ; :: thesis: ( 0 <= (normsequence G,z) . i & (normsequence G,z) . i <= ((normsequence G,xx) + (normsequence G,yy)) . i )
A18: Seg n = dom G by FINSEQ_1:def 3;
A19: dom (carr G) = dom G by A2, FINSEQ_3:31;
then A20: i in dom z by A17, A18, CARD_3:18;
dom xx = dom (carr G) by CARD_3:18;
hence ( 0 <= (normsequence G,z) . i & (normsequence G,z) . i <= ((normsequence G,xx) + (normsequence G,yy)) . i ) by A1, A17, A18, A19, A20, Th8, Th9; :: thesis: verum

end;

then A21: |.(normsequence G,z).| <= |.((normsequence G,xx) + (normsequence G,yy)).| by A15, A16, Th2;
|.((normsequence G,xx) + (normsequence G,yy)).| <= |.(normsequence G,xx).| + |.(normsequence G,yy).| by EUCLID:15;
hence ( ( not ||.x.|| = 0 or x = 0. (product G) ) & ( not x = 0. (product G) or ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by A3, A7, A13, A14, A21, Th7, XXREAL_0:2; :: thesis: verum