let X, Y be RealNormSpace-Sequence; :: thesis: ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st
( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
reconsider X0 = X, Y0 = Y as RealLinearSpace-Sequence ;
set PX = product X;
set PY = product Y;
set PX0 = product X0;
set PY0 = product Y0;
reconsider CX = carr X, CY = carr Y as non-empty non empty FinSequence ;
reconsider CX0 = carr X0, CY0 = carr Y0 as non-empty non empty FinSequence ;
A1: ( product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) & product Y = NORMSTR(# (product (carr Y)),(zeros Y),[:(addop Y):],[:(multop Y):],(productnorm Y) #) ) by PRVECT_2:6;
A2: for g1, g2 being Point of (product X)
for f1, f2 being Point of (product Y) holds (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]

proof

let g1, g2 be Point of (product X); :: thesis: for f1, f2 being Point of (product Y) holds (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
let f1, f2 be Point of (product Y); :: thesis: (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
reconsider g10 = g1, g20 = g2 as Point of (product X0) by A1;
reconsider f10 = f1, f20 = f2 as Point of (product Y0) by A1;
( g10 + g20 = g1 + g2 & f10 + f20 = f1 + f2 ) by A1;
hence (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] by Def1; :: thesis: verum

end;

A3: for r being Real
for g being Point of (product X)
for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]

proof

let r be Real; :: thesis: for g being Point of (product X)
for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
let g be Point of (product X); :: thesis: for f being Point of (product Y) holds (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
let f be Point of (product Y); :: thesis: (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)]
reconsider g0 = g as Point of (product X0) by A1;
reconsider f0 = f as Point of (product Y0) by A1;
( r * g0 = r * g & r * f0 = r * f ) by A1;
hence (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)] by Def2; :: thesis: verum

end;

A4: ( len (carr (X ^ Y)) = len (X ^ Y) & len (carr (X0 ^ Y0)) = len (X0 ^ Y0) & len CX = len X & len CY = len Y & len CX0 = len X0 & len CY0 = len Y0 ) by PRVECT_1:def 11;
consider I0 being Function of [:(product X0),(product Y0):],(product (X0 ^ Y0)) such that
A5: ( I0 is one-to-one & I0 is onto & ( for x being Point of (product X0)
for y being Point of (product Y0) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I0 . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X0),(product Y0):] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:(product X0),(product Y0):]
for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product (X0 ^ Y0)) = I0 . (0. [:(product X0),(product Y0):]) ) by Th13;
A6: product (X ^ Y) = NORMSTR(# (product (carr (X ^ Y))),(zeros (X ^ Y)),[:(addop (X ^ Y)):],[:(multop (X ^ Y)):],(productnorm (X ^ Y)) #) by PRVECT_2:6;
then reconsider I = I0 as Function of [:(product X),(product Y):],(product (X ^ Y)) by A1;
take I ; :: thesis: ( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
thus ( I is one-to-one & I is onto ) by A5, A6; :: thesis: ( ( for x being Point of (product X)
for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
thus for x being Point of (product X)
for y being Point of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) by A1, A5; :: thesis: ( ( for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )
A7: for x, y being FinSequence st x in the carrier of (product X) & y in the carrier of (product Y) holds
I . (x,y) = x ^ y

proof

let x, y be FinSequence; :: thesis: ( x in the carrier of (product X) & y in the carrier of (product Y) implies I . (x,y) = x ^ y )
assume ( x in the carrier of (product X) & y in the carrier of (product Y) ) ; :: thesis: I . (x,y) = x ^ y
then ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) by A1, A5;
hence I . (x,y) = x ^ y ; :: thesis: verum

end;

thus for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) :: thesis: ( ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )

proof

let v, w be Point of [:(product X),(product Y):]; :: thesis: I . (v + w) = (I . v) + (I . w)
reconsider v0 = v, w0 = w as Point of [:(product X0),(product Y0):] by A1;
v + w = v0 + w0 by A2, A1, Def1;
then I . (v + w) = (I0 . v0) + (I0 . w0) by A5;
hence I . (v + w) = (I . v) + (I . w) by A6; :: thesis: verum

end;

thus for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v) :: thesis: ( I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ) )

proof

let v be Point of [:(product X),(product Y):]; :: thesis: for r being Element of REAL holds I . (r * v) = r * (I . v)
let r be Element of REAL ; :: thesis: I . (r * v) = r * (I . v)
reconsider v0 = v as Point of [:(product X0),(product Y0):] by A1;
r * v = r * v0 by A3, A1, Def2;
then I . (r * v) = r * (I0 . v0) by A5;
hence I . (r * v) = r * (I . v) by A6; :: thesis: verum

end;

thus 0. (product (X ^ Y)) = I . (0. [:(product X),(product Y):]) by A1, A5, A6; :: thesis: for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.||
for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.||

proof

let v be Point of [:(product X),(product Y):]; :: thesis: ||.(I . v).|| = ||.v.||
consider x1 being Point of (product X), y1 being Point of (product Y) such that
A8: v = [x1,y1] by Lm1;
consider v1 being Element of REAL 2 such that
A9: ( v1 = <*||.x1.||,||.y1.||*> & (prod_NORM ((product X),(product Y))) . (x1,y1) = |.v1.| ) by Def6;
reconsider Ix1 = x1, Iy1 = y1 as FinSequence by A1, Lm2;
A10: ( dom Ix1 = dom (carr X) & dom Iy1 = dom (carr Y) ) by A1, CARD_3:9;
A11: I . v = I . (x1,y1) by A8
.= Ix1 ^ Iy1 by A7 ;
reconsider Iv = I . v as Element of product (carr (X ^ Y)) by A6;
reconsider Ix = x1 as Element of product (carr X) by A1;
reconsider Iy = y1 as Element of product (carr Y) by A1;
A12: ||.(I . v).|| = |.(normsequence ((X ^ Y),Iv)).| by A6, PRVECT_2:def 12
.= sqrt (Sum (sqr (normsequence ((X ^ Y),Iv)))) ;
A13: ( len (normsequence ((X ^ Y),Iv)) = len (X ^ Y) & len (normsequence (X,Ix)) = len X & len (normsequence (Y,Iy)) = len Y ) by PRVECT_2:def 11;
reconsider x12 = ||.x1.|| ^2 , y12 = ||.y1.|| ^2 as Real ;
A14: |.v1.| = sqrt (Sum <*x12,y12*>) by A9, TOPREAL6:11
.= sqrt ((||.x1.|| ^2) + (||.y1.|| ^2)) by RVSUM_1:77 ;
A15: ( 0 <= Sum (sqr (normsequence (X,Ix))) & 0 <= Sum (sqr (normsequence (Y,Iy))) ) by RVSUM_1:86;
( ||.x1.|| ^2 = |.(normsequence (X,Ix)).| ^2 & ||.y1.|| ^2 = |.(normsequence (Y,Iy)).| ^2 ) by A1, PRVECT_2:def 12;
then A16: ( ||.x1.|| ^2 = Sum (sqr (normsequence (X,Ix))) & ||.y1.|| ^2 = Sum (sqr (normsequence (Y,Iy))) ) by A15, SQUARE_1:def 2;
len (normsequence ((X ^ Y),Iv)) = (len (normsequence (X,Ix))) + (len (normsequence (Y,Iy))) by A13, FINSEQ_1:22
.= len ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) by FINSEQ_1:22 ;
then A17: dom (normsequence ((X ^ Y),Iv)) = dom ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) by FINSEQ_3:29;
for k being Nat st k in dom (normsequence ((X ^ Y),Iv)) holds
(normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k

proof

let k be Nat; :: thesis: ( k in dom (normsequence ((X ^ Y),Iv)) implies (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k )
assume k in dom (normsequence ((X ^ Y),Iv)) ; :: thesis: (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k
then A18: k in Seg (len (normsequence ((X ^ Y),Iv))) by FINSEQ_1:def 3;
then A19: k in dom (X ^ Y) by A13, FINSEQ_1:def 3;
reconsider k1 = k as Element of dom (X ^ Y) by A18, A13, FINSEQ_1:def 3;
A20: (normsequence ((X ^ Y),Iv)) . k = the normF of ((X ^ Y) . k1) . (Iv . k1) by PRVECT_2:def 11;
A21: ( dom Ix1 = Seg (len (carr X)) & dom Iy1 = Seg (len (carr Y)) ) by A10, FINSEQ_1:def 3;
then A22: ( dom Ix1 = dom X & dom Iy1 = dom Y ) by A4, FINSEQ_1:def 3;

per cases ( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) ) by A19, FINSEQ_1:25;

suppose A23: k in dom X ; :: thesis: (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k

len X = len (normsequence (X,Ix)) by PRVECT_2:def 11;
then A24: k in dom (normsequence (X,Ix)) by A23, FINSEQ_3:29;
reconsider k2 = k1 as Element of dom X by A23;
A25: Iv . k = Ix1 . k by A23, A22, A11, FINSEQ_1:def 7;
thus (normsequence ((X ^ Y),Iv)) . k = the normF of (X . k2) . (Iv . k2) by A20, FINSEQ_1:def 7
.= (normsequence (X,Ix)) . k2 by A25, PRVECT_2:def 11
.= ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k by A24, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom Y & k = (len X) + n ) ; :: thesis: (normsequence ((X ^ Y),Iv)) . k = ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k

then consider n being Nat such that
A26: ( n in dom Y & k = (len X) + n ) ;
len Y = len (normsequence (Y,Iy)) by PRVECT_2:def 11;
then A27: n in dom (normsequence (Y,Iy)) by A26, FINSEQ_3:29;
reconsider n1 = n as Element of dom Y by A26;
len Ix1 = len X by A21, A4, FINSEQ_1:def 3;
then A28: Iv . k = Iy1 . n by A11, A26, A22, FINSEQ_1:def 7;
thus (normsequence ((X ^ Y),Iv)) . k = the normF of (Y . n1) . (Iv . k1) by A20, A26, FINSEQ_1:def 7
.= (normsequence (Y,Iy)) . n1 by A28, PRVECT_2:def 11
.= ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k by A27, A26, A13, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

then normsequence ((X ^ Y),Iv) = (normsequence (X,Ix)) ^ (normsequence (Y,Iy)) by A17, FINSEQ_1:13;
then sqr (normsequence ((X ^ Y),Iv)) = (sqr (normsequence (X,Ix))) ^ (sqr (normsequence (Y,Iy))) by Lm3;
hence ||.(I . v).|| = ||.v.|| by A14, A12, A16, A9, A8, RVSUM_1:75; :: thesis: verum

end;

hence for v being Point of [:(product X),(product Y):] holds ||.(I . v).|| = ||.v.|| ; :: thesis: verum