let n be Nat; :: thesis: for X being RealNormSpace-Sequence st X = n |-> RNS_Real holds
product X = REAL-NS n
let X be RealNormSpace-Sequence; :: thesis: ( X = n |-> RNS_Real implies product X = REAL-NS n )
assume A1: X = n |-> RNS_Real ; :: thesis: product X = REAL-NS n
A2: n is Element of NAT by ORDINAL1:def 12;
A3: X = (Seg n) --> RNS_Real by FINSEQ_2:def 2, A1;
set RN = REAL-NS n;
set PX = product X;
A4: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
A5: len X = n by A1, CARD_1:def 7;
then A6: dom X = Seg n by FINSEQ_1:def 3;
A7: len (carr X) = len X by PRVECT_1:def 11
.= n by A1, CARD_1:def 7 ;
then A8: dom (carr X) = Seg n by FINSEQ_1:def 3;
A9: for i being Nat st i in Seg n holds
(carr X) . i = REAL

proof

let i be Nat; :: thesis: ( i in Seg n implies (carr X) . i = REAL )
assume A10: i in Seg n ; :: thesis: (carr X) . i = REAL
then reconsider i0 = i as Element of dom (carr X) by A7, FINSEQ_1:def 3;
X . i0 = RNS_Real by A1, A10, FINSEQ_2:57;
hence (carr X) . i = the carrier of RNS_Real by A6, A10, PRVECT_1:def 11
.= REAL ;
:: thesis: verum

end;

A11: for x being object holds
( x in product (carr X) iff x in REAL n )

proof

let x be object ; :: thesis: ( x in product (carr X) iff x in REAL n )

hereby :: thesis: ( x in REAL n implies x in product (carr X) )

assume x in product (carr X) ; :: thesis: x in REAL n
then consider g being Function such that
A12: ( x = g & dom g = dom (carr X) & ( for y being object st y in dom (carr X) holds
g . y in (carr X) . y ) ) by CARD_3:def 5;
dom g = Seg n by A7, A12, FINSEQ_1:def 3;
then reconsider g = g as FinSequence by FINSEQ_1:def 2;
for y being object st y in rng g holds
y in REAL

proof

let y be object ; :: thesis: ( y in rng g implies y in REAL )
assume y in rng g ; :: thesis: y in REAL
then consider i being object such that
A13: ( i in dom g & y = g . i ) by FUNCT_1:def 3;
A14: g . i in (carr X) . i by A12, A13;
reconsider i = i as Nat by A13;
thus y in REAL by A8, A9, A12, A13, A14; :: thesis: verum

end;

then rng g c= REAL ;
then reconsider g = g as FinSequence of REAL by FINSEQ_1:def 4;
len g = n by A2, A8, A12, FINSEQ_1:def 3;
then g is Element of n -tuples_on REAL by FINSEQ_2:92;
hence x in REAL n by A12; :: thesis: verum

end;

assume x in REAL n ; :: thesis: x in product (carr X)
then x in { s where s is Element of REAL * : len s = n } by FINSEQ_2:def 4;
then consider z being Element of REAL * such that
A15: ( x = z & len z = n ) ;
reconsider z = z as FinSequence of REAL ;
A16: dom z = Seg n by A15, FINSEQ_1:def 3
.= dom (carr X) by A7, FINSEQ_1:def 3 ;
for y being object st y in dom (carr X) holds
z . y in (carr X) . y

proof

let y be object ; :: thesis: ( y in dom (carr X) implies z . y in (carr X) . y )
assume A17: y in dom (carr X) ; :: thesis: z . y in (carr X) . y
then reconsider i = y as Nat ;
A18: (carr X) . i = REAL by A8, A9, A17;
z . i in rng z by A16, A17, FUNCT_1:3;
hence z . y in (carr X) . y by A18; :: thesis: verum

end;

hence x in product (carr X) by A15, A16, CARD_3:def 5; :: thesis: verum

end;

then A19: product (carr X) = REAL n by TARSKI:2;
A20: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4
.= the carrier of (product X) by A4, A11, TARSKI:2 ;
A21: for j being Element of dom (carr X) holds (0* n) . j = 0. (X . j)

proof

let j be Element of dom (carr X); :: thesis: (0* n) . j = 0. (X . j)
thus (0* n) . j = (n |-> (In (0,REAL))) . j
.= ((Seg n) --> (In (0,REAL))) . j by FINSEQ_2:def 2
.= In (0,REAL) by A8
.= 0. (X . j) by A1, A8, FINSEQ_2:57 ; :: thesis: verum

end;

A22: the ZeroF of (REAL-NS n) = 0. (REAL-NS n)
.= 0* n by REAL_NS1:def 4
.= the ZeroF of (product X) by A4, A19, A21, PRVECT_1:def 14 ;
A23: REAL n = the carrier of (REAL-NS n) by REAL_NS1:def 4
.= the carrier of (product X) by A20 ;
for a, b being Element of REAL n holds the addF of (product X) . (a,b) = a + b

proof

let a, b be Element of REAL n; :: thesis: the addF of (product X) . (a,b) = a + b
reconsider a1 = a, b1 = b as Element of product (carr X) by A11;
reconsider ab = [:(addop X):] . (a1,b1) as Element of REAL n by A11;
a in n -tuples_on REAL ;
then a in { s where s is Element of REAL * : len s = n } by FINSEQ_2:def 4;
then consider az being Element of REAL * such that
A24: ( a = az & len az = n ) ;
reconsider az = az as FinSequence of REAL ;
b in n -tuples_on REAL ;
then b in { s where s is Element of REAL * : len s = n } by FINSEQ_2:def 4;
then consider bz being Element of REAL * such that
A25: ( b = bz & len bz = n ) ;
reconsider bz = bz as FinSequence of REAL ;
ab in n -tuples_on REAL ;
then ab in { s where s is Element of REAL * : len s = n } by FINSEQ_2:def 4;
then consider abz being Element of REAL * such that
A26: ( ab = abz & len abz = n ) ;
reconsider abz = abz as FinSequence of REAL ;
A27: dom abz = Seg n by A26, FINSEQ_1:def 3
.= (Seg n) /\ (Seg n)
.= (dom az) /\ (Seg n) by A24, FINSEQ_1:def 3
.= (dom az) /\ (dom bz) by A25, FINSEQ_1:def 3 ;
for i being object st i in dom abz holds
abz . i = (az . i) + (bz . i)

proof

let i be object ; :: thesis: ( i in dom abz implies abz . i = (az . i) + (bz . i) )
assume i in dom abz ; :: thesis: abz . i = (az . i) + (bz . i)
then reconsider i0 = i as Element of dom (carr X) by A8, A26, FINSEQ_1:def 3;
reconsider ai0 = a . i0 as VECTOR of (X . i0) by A3, A8, XREAL_0:def 1;
reconsider bi0 = b . i0 as VECTOR of (X . i0) by A3, A8, XREAL_0:def 1;
([:(addop X):] . (a1,b1)) . i0 = ai0 + bi0 by Th11
.= (a . i0) + (b . i0) by A3, A8, BINOP_2:def 9 ;
hence abz . i = (az . i) + (bz . i) by A24, A25, A26; :: thesis: verum

end;

hence the addF of (product X) . (a,b) = a + b by A4, A24, A25, A26, A27, VALUED_1:def 1; :: thesis: verum

end;

then Euclid_add n = the addF of (product X) by A23, REAL_NS1:def 1;
then A28: the addF of (REAL-NS n) = the addF of (product X) by REAL_NS1:def 4;
for r being Real
for a being Element of REAL n holds the Mult of (product X) . (r,a) = r * a

proof

let r be Real; :: thesis: for a being Element of REAL n holds the Mult of (product X) . (r,a) = r * a
let a be Element of REAL n; :: thesis: the Mult of (product X) . (r,a) = r * a
A29: r is Element of REAL by XREAL_0:def 1;
reconsider a1 = a as Element of product (carr X) by A11;
reconsider aa1 = a1 as Element of (product X) by A4;
[:(multop X):] . (r,a1) = r * aa1 by A4;
then reconsider ra = [:(multop X):] . (r,a1) as Element of REAL n by A4, A11;
a in n -tuples_on REAL ;
then a in { s where s is Element of REAL * : len s = n } by FINSEQ_2:def 4;
then consider az being Element of REAL * such that
A30: ( a = az & len az = n ) ;
reconsider az = az as FinSequence of REAL ;
ra in n -tuples_on REAL ;
then ra in { s where s is Element of REAL * : len s = n } by FINSEQ_2:def 4;
then consider raz being Element of REAL * such that
A31: ( ra = raz & len raz = n ) ;
reconsider raz = raz as FinSequence of REAL ;
A32: dom raz = Seg n by A31, FINSEQ_1:def 3
.= dom az by A30, FINSEQ_1:def 3 ;
for i being object st i in dom raz holds
raz . i = r * (az . i)

proof

let i be object ; :: thesis: ( i in dom raz implies raz . i = r * (az . i) )
assume i in dom raz ; :: thesis: raz . i = r * (az . i)
then reconsider i0 = i as Element of dom (carr X) by A8, A31, FINSEQ_1:def 3;
reconsider ai0 = a . i0 as VECTOR of (X . i0) by XREAL_0:def 1, A3, A8;
([:(multop X):] . (r,a1)) . i0 = r * ai0 by Th12, A29
.= r * (a . i0) by A3, A8, BINOP_2:def 11 ;
hence raz . i = r * (az . i) by A30, A31; :: thesis: verum

end;

hence the Mult of (product X) . (r,a) = r * a by A4, A30, A31, A32, VALUED_1:def 5; :: thesis: verum

end;

then Euclid_mult n = the Mult of (product X) by A23, REAL_NS1:def 2;
then A33: the Mult of (REAL-NS n) = the Mult of (product X) by REAL_NS1:def 4;
for a being Element of REAL n holds the normF of (product X) . a = |.a.|

proof

let a be Element of REAL n; :: thesis: the normF of (product X) . a = |.a.|
reconsider a1 = a as Element of product (carr X) by A11;
reconsider aa1 = a1 as Element of (product X) by A4;
a in n -tuples_on REAL ;
then a in { s where s is Element of REAL * : len s = n } by FINSEQ_2:def 4;
then consider az being Element of REAL * such that
A34: ( a = az & len az = n ) ;
reconsider az = az as FinSequence of REAL ;
A35: the normF of (product X) . aa1 = ||.aa1.||
.= |.(normsequence (X,a1)).| by PRVECT_2:7 ;
A36: len (normsequence (X,a1)) = len X by PRVECT_2:def 11
.= n by A1, CARD_1:def 7 ;
A37: dom (normsequence (X,a1)) = Seg n by A36, FINSEQ_1:def 3
.= dom a by A34, FINSEQ_1:def 3 ;
reconsider f1 = normsequence (X,a1) as real-valued Function ;
reconsider g1 = a as real-valued Function ;
for i being object st i in dom f1 holds
f1 . i = |.(g1 . i).|

proof

let i be object ; :: thesis: ( i in dom f1 implies f1 . i = |.(g1 . i).| )
assume i in dom f1 ; :: thesis: f1 . i = |.(g1 . i).|
then i in Seg n by A36, FINSEQ_1:def 3;
then reconsider i0 = i as Element of dom X by A5, FINSEQ_1:def 3;
thus f1 . i = the normF of (X . i0) . (a1 . i0) by PRVECT_2:def 11
.= the normF of RNS_Real . (a1 . i0) by A3
.= |.(g1 . i).| by EUCLID:def 2 ; :: thesis: verum

end;

then f1 = |.g1.| by A37, VALUED_1:def 11
.= abs a ;
then |.(normsequence (X,a1)).| = sqrt (Sum (sqr a)) by EUCLID:25
.= |.a.| ;
hence the normF of (product X) . a = |.a.| by A35; :: thesis: verum

end;

then Euclid_norm n = the normF of (product X) by A23, REAL_NS1:def 3;
hence product X = REAL-NS n by A20, A22, A28, A33, REAL_NS1:def 4; :: thesis: verum