let X, Y be non empty 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 non empty 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 ;
P4X1: ( 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;
V4: 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 P4X1;
reconsider f10 = f1, f20 = f2 as Point of (product Y0) by P4X1;
( g10 + g20 = g1 + g2 & f10 + f20 = f1 + f2 ) by P4X1;
hence (prod_ADD ((product X0),(product Y0))) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] by defADD; :: thesis: verum

end;

P0: for r being Element of 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 Element of 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 P4X1;
reconsider f0 = f as Point of (product Y0) by P4X1;
( r * g0 = r * g & r * f0 = r * f ) by P4X1;
hence (prod_MLT ((product X0),(product Y0))) . (r,[g,f]) = [(r * g),(r * f)] by defMLT; :: thesis: verum

end;

SX0: ( 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_2:def 4;
consider I0 being Function of [:(product X0),(product Y0):],(product (X0 ^ Y0)) such that
P1: ( 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 ThHOM01A;
XX: 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 P4X1;
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 P1, XX; :: 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 P4X1, P1; :: 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.|| ) )
Z1C: 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 P4X1, P1;
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 P4X1;
v + w = v0 + w0 by V4, P4X1, defADD;
then I . (v + w) = (I0 . v0) + (I0 . w0) by P1;
hence I . (v + w) = (I . v) + (I . w) by XX; :: 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 P4X1;
r * v = r * v0 by P0, P4X1, defMLT;
then I . (r * v) = r * (I0 . v0) by P1;
hence I . (r * v) = r * (I . v) by XX; :: thesis: verum

end;

thus 0. (product (X ^ Y)) = I . (0. [:(product X),(product Y):]) by P4X1, P1, XX; :: 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
PPP1: v = [x1,y1] by LM01;
consider v1 being Element of REAL 2 such that
PPP2: ( v1 = <*||.x1.||,||.y1.||*> & (prod_NORM ((product X),(product Y))) . (x1,y1) = |.v1.| ) by defNORM;
reconsider Ix1 = x1, Iy1 = y1 as FinSequence by P4X1, LMPROD1;
XX1: ( dom Ix1 = dom (carr X) & dom Iy1 = dom (carr Y) ) by P4X1, CARD_3:18;
P55: I . v = I . (x1,y1) by PPP1
.= Ix1 ^ Iy1 by Z1C ;
reconsider Iv = I . v as Element of product (carr (X ^ Y)) by XX;
reconsider Ix = x1 as Element of product (carr X) by P4X1;
reconsider Iy = y1 as Element of product (carr Y) by P4X1;
P61: ||.(I . v).|| = |.(normsequence ((X ^ Y),Iv)).| by XX, PRVECT_2:def 12
.= sqrt (Sum (sqr (normsequence ((X ^ Y),Iv)))) ;
P62: ( 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;
U1: |.v1.| = sqrt (Sum <*(||.x1.|| ^2),(||.y1.|| ^2)*>) by PPP2, TOPREAL6:16
.= sqrt ((||.x1.|| ^2) + (||.y1.|| ^2)) by RVSUM_1:107 ;
U20: ( 0 <= Sum (sqr (normsequence (X,Ix))) & 0 <= Sum (sqr (normsequence (Y,Iy))) ) by RVSUM_1:116;
( ||.x1.|| ^2 = |.(normsequence (X,Ix)).| ^2 & ||.y1.|| ^2 = |.(normsequence (Y,Iy)).| ^2 ) by P4X1, PRVECT_2:def 12;
then U2: ( ||.x1.|| ^2 = Sum (sqr (normsequence (X,Ix))) & ||.y1.|| ^2 = Sum (sqr (normsequence (Y,Iy))) ) by U20, SQUARE_1:def 4;
len (normsequence ((X ^ Y),Iv)) = (len (normsequence (X,Ix))) + (len (normsequence (Y,Iy))) by P62, FINSEQ_1:35
.= len ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) by FINSEQ_1:35 ;
then U4: dom (normsequence ((X ^ Y),Iv)) = dom ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) by FINSEQ_3:31;
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 R1: k in Seg (len (normsequence ((X ^ Y),Iv))) by FINSEQ_1:def 3;
then R2: k in dom (X ^ Y) by P62, FINSEQ_1:def 3;
reconsider k1 = k as Element of dom (X ^ Y) by R1, P62, FINSEQ_1:def 3;
A9: (normsequence ((X ^ Y),Iv)) . k = the normF of ((X ^ Y) . k1) . (Iv . k1) by PRVECT_2:def 11;
AB0: ( dom Ix1 = Seg (len (carr X)) & dom Iy1 = Seg (len (carr Y)) ) by XX1, FINSEQ_1:def 3;
then AA1: ( dom Ix1 = dom X & dom Iy1 = dom Y ) by SX0, 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 R2, FINSEQ_1:38;

suppose A80: 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 A81: k in dom (normsequence (X,Ix)) by A80, FINSEQ_3:31;
reconsider k2 = k1 as Element of dom X by A80;
AA2: Iv . k = Ix1 . k by A80, AA1, P55, FINSEQ_1:def 7;
thus (normsequence ((X ^ Y),Iv)) . k = the normF of (X . k2) . (Iv . k2) by A9, FINSEQ_1:def 7
.= (normsequence (X,Ix)) . k2 by AA2, PRVECT_2:def 11
.= ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k by A81, 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
A90: ( n in dom Y & k = (len X) + n ) ;
len Y = len (normsequence (Y,Iy)) by PRVECT_2:def 11;
then A81: n in dom (normsequence (Y,Iy)) by A90, FINSEQ_3:31;
reconsider n1 = n as Element of dom Y by A90;
len Ix1 = len X by AB0, SX0, FINSEQ_1:def 3;
then AA2: Iv . k = Iy1 . n by P55, A90, AA1, FINSEQ_1:def 7;
thus (normsequence ((X ^ Y),Iv)) . k = the normF of (Y . n1) . (Iv . k1) by A9, A90, FINSEQ_1:def 7
.= (normsequence (Y,Iy)) . n1 by AA2, PRVECT_2:def 11
.= ((normsequence (X,Ix)) ^ (normsequence (Y,Iy))) . k by A81, A90, P62, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

then normsequence ((X ^ Y),Iv) = (normsequence (X,Ix)) ^ (normsequence (Y,Iy)) by U4, FINSEQ_1:17;
then sqr (normsequence ((X ^ Y),Iv)) = (sqr (normsequence (X,Ix))) ^ (sqr (normsequence (Y,Iy))) by RVSQR1;
hence ||.(I . v).|| = ||.v.|| by U1, P61, U2, PPP2, PPP1, RVSUM_1:105; :: thesis: verum

end;

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