let G be RealNormSpace-Sequence; :: thesis: ( product G is reflexive & product G is discerning & product G is RealNormSpace-like )

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;

reconsider n = len G as Element of NAT ;

thus product G is reflexive :: thesis: ( product G is discerning & product G is RealNormSpace-like )_{1} being object holds

( ||.(b_{1} * x).|| = |.b_{1}.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

let a be Real; :: thesis: ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

reconsider z = x as Element of product (carr G) by A1;

reconsider xx = x, yy = y as Element of product (carr G) by A1;

reconsider ax = a * x as Element of product (carr G) by A1;

A7: ( ||.y.|| = |.(normsequence (G,yy)).| & |.((normsequence (G,xx)) + (normsequence (G,yy))).| <= |.(normsequence (G,xx)).| + |.(normsequence (G,yy)).| ) by Th7, EUCLID:12;

A8: len (normsequence (G,ax)) = n by CARD_1:def 7;

then A9: dom (normsequence (G,ax)) = Seg n by FINSEQ_1:def 3;

A10: for i being Nat st i in dom (normsequence (G,ax)) holds

(normsequence (G,ax)) . i = (|.a.| * (normsequence (G,z))) . i

then |.(normsequence (G,ax)).| = |.(|.a.| * (normsequence (G,z))).| by A8, A10, FINSEQ_2:9;

then A11: |.(normsequence (G,ax)).| = |.|.a.|.| * |.(normsequence (G,z)).| by EUCLID:11;

reconsider z = x + y as Element of product (carr G) by A1;

A12: 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 )

then len (normsequence (G,z)) = len ((normsequence (G,xx)) + (normsequence (G,yy))) by CARD_1:def 7;

then A17: |.(normsequence (G,z)).| <= |.((normsequence (G,xx)) + (normsequence (G,yy))).| by A16, A12, Th2;

( ||.(x + y).|| = |.(normsequence (G,z)).| & ||.x.|| = |.(normsequence (G,xx)).| ) by Th7;

hence ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by A11, A17, A7, Th7, XXREAL_0:2; :: thesis: verum

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;

reconsider n = len G as Element of NAT ;

thus product G is reflexive :: thesis: ( product G is discerning & product G is RealNormSpace-like )

proof

thus
product G is discerning
:: thesis: product G is RealNormSpace-like
reconsider z = 0. (product G) as Element of product (carr G) by A1;

A3: for i being Element of dom (carr G) holds (normsequence (G,z)) . i = 0

(sqr (normsequence (G,z))) . i = 0

hence ||.(0. (product G)).|| = 0 by Th7; :: according to NORMSP_0:def 6 :: thesis: verum

end;A3: for i being Element of dom (carr G) holds (normsequence (G,z)) . i = 0

proof

for i being Element of NAT st i in dom (sqr (normsequence (G,z))) holds
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:29;

(carr G) . i0 = the carrier of (G . i0) by Def4;

then reconsider zi0 = z . i0 as Element of (G . i0) by CARD_3:9;

z . i = 0. (G . i) by A1, Def7;

then ||.zi0.|| = 0 ;

hence (normsequence (G,z)) . i = 0 by Def11; :: thesis: verum

end;reconsider i0 = i as Element of dom G by A2, FINSEQ_3:29;

(carr G) . i0 = the carrier of (G . i0) by Def4;

then reconsider zi0 = z . i0 as Element of (G . i0) by CARD_3:9;

z . i = 0. (G . i) by A1, Def7;

then ||.zi0.|| = 0 ;

hence (normsequence (G,z)) . i = 0 by Def11; :: thesis: verum

(sqr (normsequence (G,z))) . i = 0

proof

then
|.(normsequence (G,z)).| = 0
by Th3, SQUARE_1:17;
let i be Element of NAT ; :: thesis: ( i in dom (sqr (normsequence (G,z))) implies (sqr (normsequence (G,z))) . i = 0 )

assume A4: i in dom (sqr (normsequence (G,z))) ; :: thesis: (sqr (normsequence (G,z))) . i = 0

len (normsequence (G,z)) = len G by Def11;

then A5: dom (normsequence (G,z)) = dom G by FINSEQ_3:29;

dom (carr G) = dom G by A2, FINSEQ_3:29;

then dom (sqr (normsequence (G,z))) = dom (carr G) by A5, VALUED_1:11;

then ((normsequence (G,z)) . i) ^2 = 0 ^2 by A3, A4;

hence (sqr (normsequence (G,z))) . i = 0 by VALUED_1:11; :: thesis: verum

end;assume A4: i in dom (sqr (normsequence (G,z))) ; :: thesis: (sqr (normsequence (G,z))) . i = 0

len (normsequence (G,z)) = len G by Def11;

then A5: dom (normsequence (G,z)) = dom G by FINSEQ_3:29;

dom (carr G) = dom G by A2, FINSEQ_3:29;

then dom (sqr (normsequence (G,z))) = dom (carr G) by A5, VALUED_1:11;

then ((normsequence (G,z)) . i) ^2 = 0 ^2 by A3, A4;

hence (sqr (normsequence (G,z))) . i = 0 by VALUED_1:11; :: thesis: verum

hence ||.(0. (product G)).|| = 0 by Th7; :: according to NORMSP_0:def 6 :: thesis: verum

proof

let x, y be Point of (product G); :: according to NORMSP_1:def 1 :: thesis: for b
let x be Point of (product G); :: according to NORMSP_0:def 5 :: thesis: ( not ||.x.|| = 0 or x = 0. (product G) )

reconsider z = x as Element of product (carr G) by A1;

assume A6: ||.x.|| = 0 ; :: thesis: x = 0. (product G)

end;reconsider z = x as Element of product (carr G) by A1;

assume A6: ||.x.|| = 0 ; :: thesis: x = 0. (product G)

now :: thesis: for i being Element of dom (carr G) holds z . i = the ZeroF of (G . i)

hence
x = 0. (product G)
by A1, Def7; :: thesis: verumlet i be Element of dom (carr G); :: thesis: z . i = the ZeroF of (G . i)

reconsider i0 = i as Element of dom G by A2, FINSEQ_3:29;

(carr G) . i0 = the carrier of (G . i0) by Def4;

then reconsider zzi0 = z . i0 as Element of (G . i0) by CARD_3:9;

||.x.|| = |.(normsequence (G,z)).| by Th7;

then normsequence (G,z) = 0* n by A6, EUCLID:8;

then (normsequence (G,z)) . i = 0 ;

then ||.zzi0.|| = 0 by Def11;

then z . i = 0. (G . i) by NORMSP_0:def 5;

hence z . i = the ZeroF of (G . i) ; :: thesis: verum

end;reconsider i0 = i as Element of dom G by A2, FINSEQ_3:29;

(carr G) . i0 = the carrier of (G . i0) by Def4;

then reconsider zzi0 = z . i0 as Element of (G . i0) by CARD_3:9;

||.x.|| = |.(normsequence (G,z)).| by Th7;

then normsequence (G,z) = 0* n by A6, EUCLID:8;

then (normsequence (G,z)) . i = 0 ;

then ||.zzi0.|| = 0 by Def11;

then z . i = 0. (G . i) by NORMSP_0:def 5;

hence z . i = the ZeroF of (G . i) ; :: thesis: verum

( ||.(b

let a be Real; :: thesis: ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

reconsider z = x as Element of product (carr G) by A1;

reconsider xx = x, yy = y as Element of product (carr G) by A1;

reconsider ax = a * x as Element of product (carr G) by A1;

A7: ( ||.y.|| = |.(normsequence (G,yy)).| & |.((normsequence (G,xx)) + (normsequence (G,yy))).| <= |.(normsequence (G,xx)).| + |.(normsequence (G,yy)).| ) by Th7, EUCLID:12;

A8: len (normsequence (G,ax)) = n by CARD_1:def 7;

then A9: dom (normsequence (G,ax)) = Seg n by FINSEQ_1:def 3;

A10: for i being Nat st i in dom (normsequence (G,ax)) holds

(normsequence (G,ax)) . i = (|.a.| * (normsequence (G,z))) . i

proof

len (|.a.| * (normsequence (G,z))) = n
by CARD_1:def 7;
let i be Nat; :: thesis: ( i in dom (normsequence (G,ax)) implies (normsequence (G,ax)) . i = (|.a.| * (normsequence (G,z))) . i )

assume i in dom (normsequence (G,ax)) ; :: thesis: (normsequence (G,ax)) . i = (|.a.| * (normsequence (G,z))) . i

then reconsider i0 = i as Element of dom G by A9, FINSEQ_1:def 3;

reconsider i1 = i0 as Element of dom (carr G) by A2, FINSEQ_3:29;

( (carr G) . i0 = the carrier of (G . i0) & dom (carr G) = dom G ) by A2, Def4, FINSEQ_3:29;

then reconsider axi0 = ax . i0, zi0 = z . i0 as Element of (G . i0) by CARD_3:9;

reconsider aa = a as Element of REAL by XREAL_0:def 1;

([:(multop G):] . (aa,z)) . i1 = ((multop G) . i1) . (a,zi0) by Def2;

then axi0 = a * zi0 by A1, Def8;

then ||.axi0.|| = |.a.| * ||.zi0.|| by NORMSP_1:def 1;

then ||.axi0.|| = |.a.| * ((normsequence (G,z)) . i0) by Def11;

then ||.axi0.|| = (|.a.| * (normsequence (G,z))) . i0 by RVSUM_1:44;

hence (normsequence (G,ax)) . i = (|.a.| * (normsequence (G,z))) . i by Def11; :: thesis: verum

end;assume i in dom (normsequence (G,ax)) ; :: thesis: (normsequence (G,ax)) . i = (|.a.| * (normsequence (G,z))) . i

then reconsider i0 = i as Element of dom G by A9, FINSEQ_1:def 3;

reconsider i1 = i0 as Element of dom (carr G) by A2, FINSEQ_3:29;

( (carr G) . i0 = the carrier of (G . i0) & dom (carr G) = dom G ) by A2, Def4, FINSEQ_3:29;

then reconsider axi0 = ax . i0, zi0 = z . i0 as Element of (G . i0) by CARD_3:9;

reconsider aa = a as Element of REAL by XREAL_0:def 1;

([:(multop G):] . (aa,z)) . i1 = ((multop G) . i1) . (a,zi0) by Def2;

then axi0 = a * zi0 by A1, Def8;

then ||.axi0.|| = |.a.| * ||.zi0.|| by NORMSP_1:def 1;

then ||.axi0.|| = |.a.| * ((normsequence (G,z)) . i0) by Def11;

then ||.axi0.|| = (|.a.| * (normsequence (G,z))) . i0 by RVSUM_1:44;

hence (normsequence (G,ax)) . i = (|.a.| * (normsequence (G,z))) . i by Def11; :: thesis: verum

then |.(normsequence (G,ax)).| = |.(|.a.| * (normsequence (G,z))).| by A8, A10, FINSEQ_2:9;

then A11: |.(normsequence (G,ax)).| = |.|.a.|.| * |.(normsequence (G,z)).| by EUCLID:11;

reconsider z = x + y as Element of product (carr G) by A1;

A12: 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

A16:
len (normsequence (G,z)) = n
by Def11;
A13:
dom xx = dom (carr G)
by CARD_3:9;

A14: ( Seg n = dom G & dom (carr G) = dom G ) by A2, FINSEQ_1:def 3, FINSEQ_3:29;

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 A15: i in Seg n ; :: thesis: ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i )

i in dom z by A15, A14, CARD_3:9;

hence ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i ) by A1, A15, A14, A13, Th8, Th9; :: thesis: verum

end;A14: ( Seg n = dom G & dom (carr G) = dom G ) by A2, FINSEQ_1:def 3, FINSEQ_3:29;

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 A15: i in Seg n ; :: thesis: ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i )

i in dom z by A15, A14, CARD_3:9;

hence ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i ) by A1, A15, A14, A13, Th8, Th9; :: thesis: verum

then len (normsequence (G,z)) = len ((normsequence (G,xx)) + (normsequence (G,yy))) by CARD_1:def 7;

then A17: |.(normsequence (G,z)).| <= |.((normsequence (G,xx)) + (normsequence (G,yy))).| by A16, A12, Th2;

( ||.(x + y).|| = |.(normsequence (G,z)).| & ||.x.|| = |.(normsequence (G,xx)).| ) by Th7;

hence ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by A11, A17, A7, Th7, XXREAL_0:2; :: thesis: verum