:: Cartesian Products of Family of Real Linear Spaces
:: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama
::
:: Received August 17, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users


theorem :: PRVECT_3:1
for D, E, F, G being non empty set ex I being Function of [:[:D,E:],[:F,G:]:],[:[:D,F:],[:E,G:]:] st
( I is one-to-one & I is onto & ( for d, e, f, g being set st d in D & e in E & f in F & g in G holds
I . ([d,e],[f,g]) = [[d,f],[e,g]] ) )
proof end;

theorem Th2: :: PRVECT_3:2
for X being non empty set
for D being Function st dom D = {1} & D . 1 = X holds
ex I being Function of X,(product D) st
( I is one-to-one & I is onto & ( for x being object st x in X holds
I . x = <*x*> ) )
proof end;

theorem Th3: :: PRVECT_3:3
for X, Y being non empty set
for D being Function st dom D = {1,2} & D . 1 = X & D . 2 = Y holds
ex I being Function of [:X,Y:],(product D) st
( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
proof end;

theorem Th4: :: PRVECT_3:4
for X being non empty set ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being object st x in X holds
I . x = <*x*> ) )
proof end;

registration
let X, Y be non-empty non empty FinSequence;
cluster X ^ Y -> non-empty ;
correctness
coherence
X ^ Y is non-empty ;
proof end;
end;

theorem Th5: :: PRVECT_3:5
for X, Y being non empty set ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
proof end;

theorem Th6: :: PRVECT_3:6
for X, Y being non-empty non empty FinSequence ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st
( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product X & y in product Y holds
I . (x,y) = x ^ y ) )
proof end;

Lm1: for G, F being non empty 1-sorted
for x being set st x in [: the carrier of G, the carrier of F:] holds
ex x1 being Point of G ex x2 being Point of F st x = [x1,x2]
by SUBSET_1:43;

definition
let G, F be non empty addLoopStr ;
func prod_ADD (G,F) -> BinOp of [: the carrier of G, the carrier of F:] means :Def1: :: PRVECT_3:def 1
 for g1, g2 being Point of G
for f1, f2 being Point of F holds it . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)];
existence
ex b1 being BinOp of [: the carrier of G, the carrier of F:] st
for g1, g2 being Point of G
for f1, f2 being Point of F holds b1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
proof end;
uniqueness
for b1, b2 being BinOp of [: the carrier of G, the carrier of F:] st ( for g1, g2 being Point of G
for f1, f2 being Point of F holds b1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) & ( for g1, g2 being Point of G
for f1, f2 being Point of F holds b2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines prod_ADD PRVECT_3:def 1 :
for G, F being non empty addLoopStr
for b3 being BinOp of [: the carrier of G, the carrier of F:] holds
( b3 = prod_ADD (G,F) iff for g1, g2 being Point of G
for f1, f2 being Point of F holds b3 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] );

definition
let G, F be non empty RLSStruct ;
func prod_MLT (G,F) -> Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] means :Def2: :: PRVECT_3:def 2
 for r being Real
for g being Point of G
for f being Point of F holds it . (r,[g,f]) = [(r * g),(r * f)];
existence
ex b1 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Real
for g being Point of G
for f being Point of F holds b1 . (r,[g,f]) = [(r * g),(r * f)]
proof end;
uniqueness
for b1, b2 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st ( for r being Real
for g being Point of G
for f being Point of F holds b1 . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Real
for g being Point of G
for f being Point of F holds b2 . (r,[g,f]) = [(r * g),(r * f)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines prod_MLT PRVECT_3:def 2 :
for G, F being non empty RLSStruct
for b3 being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] holds
( b3 = prod_MLT (G,F) iff for r being Real
for g being Point of G
for f being Point of F holds b3 . (r,[g,f]) = [(r * g),(r * f)] );

definition
let G, F be non empty addLoopStr ;
func prod_ZERO (G,F) -> Element of [: the carrier of G, the carrier of F:] equals :: PRVECT_3:def 3
[(0. G),(0. F)];
correctness
coherence
[(0. G),(0. F)] is Element of [: the carrier of G, the carrier of F:];
;
end;

:: deftheorem defines prod_ZERO PRVECT_3:def 3 :
for G, F being non empty addLoopStr holds prod_ZERO (G,F) = [(0. G),(0. F)];

definition
let G, F be non empty addLoopStr ;
func [:G,F:] -> non empty strict addLoopStr equals :: PRVECT_3:def 4
 addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #);
correctness
coherence
addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #) is non empty strict addLoopStr ;
;
end;

:: deftheorem defines [: PRVECT_3:def 4 :
for G, F being non empty addLoopStr holds [:G,F:] = addLoopStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)) #);

definition
let G, F be non empty addLoopStr ;
let g be Element of G;
let f be Element of F;
:: original: [
redefine func [g,f] -> Element of [:G,F:];
coherence
[g,f] is Element of [:G,F:]
proof end;
end;

registration
let G, F be non empty Abelian addLoopStr ;
cluster [:G,F:] -> non empty strict Abelian ;
correctness
coherence
[:G,F:] is Abelian ;
proof end;
end;

registration
let G, F be non empty add-associative addLoopStr ;
cluster [:G,F:] -> non empty strict add-associative ;
correctness
coherence
[:G,F:] is add-associative ;
proof end;
end;

registration
let G, F be non empty right_zeroed addLoopStr ;
cluster [:G,F:] -> non empty strict right_zeroed ;
correctness
coherence
[:G,F:] is right_zeroed ;
proof end;
end;

registration
let G, F be non empty right_complementable addLoopStr ;
cluster [:G,F:] -> non empty strict right_complementable ;
correctness
coherence
[:G,F:] is right_complementable ;
proof end;
end;

theorem :: PRVECT_3:7
for G, F being non empty addLoopStr holds
( ( for x being set holds
( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]
for x1, y1 being Point of G
for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] ) by Lm1, Def1;

theorem :: PRVECT_3:8
for G, F being non empty right_complementable add-associative right_zeroed addLoopStr
for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
proof end;

registration
let G, F be non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr ;
cluster [:G,F:] -> non empty strict right_complementable Abelian add-associative right_zeroed ;
correctness
coherence
( [:G,F:] is strict & [:G,F:] is Abelian & [:G,F:] is add-associative & [:G,F:] is right_zeroed & [:G,F:] is right_complementable );
;
end;

definition
let G, F be non empty RLSStruct ;
func [:G,F:] -> non empty strict RLSStruct equals :: PRVECT_3:def 5
 RLSStruct(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)) #);
correctness
coherence
RLSStruct(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)) #) is non empty strict RLSStruct ;
;
end;

:: deftheorem defines [: PRVECT_3:def 5 :
for G, F being non empty RLSStruct holds [:G,F:] = RLSStruct(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)) #);

definition
let G, F be non empty RLSStruct ;
let g be Element of G;
let f be Element of F;
:: original: [
redefine func [g,f] -> Element of [:G,F:];
coherence
[g,f] is Element of [:G,F:]
proof end;
end;

registration
let G, F be non empty Abelian RLSStruct ;
cluster [:G,F:] -> non empty strict Abelian ;
correctness
coherence
[:G,F:] is Abelian ;
proof end;
end;

registration
let G, F be non empty add-associative RLSStruct ;
cluster [:G,F:] -> non empty strict add-associative ;
correctness
coherence
[:G,F:] is add-associative ;
proof end;
end;

registration
let G, F be non empty right_zeroed RLSStruct ;
cluster [:G,F:] -> non empty strict right_zeroed ;
correctness
coherence
[:G,F:] is right_zeroed ;
proof end;
end;

registration
let G, F be non empty right_complementable RLSStruct ;
cluster [:G,F:] -> non empty right_complementable strict ;
correctness
coherence
[:G,F:] is right_complementable ;
proof end;
end;

theorem Th9: :: PRVECT_3:9
for G, F being non empty RLSStruct holds
( ( for x being set holds
( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]
for x1, y1 being Point of G
for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being Real st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) ) by Def2, Def1, Lm1;

theorem :: PRVECT_3:10
for G, F being non empty right_complementable add-associative right_zeroed RLSStruct
for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
proof end;

registration
let G, F be non empty vector-distributive RLSStruct ;
cluster [:G,F:] -> non empty strict vector-distributive ;
correctness
coherence
[:G,F:] is vector-distributive ;
proof end;
end;

registration
let G, F be non empty scalar-distributive RLSStruct ;
cluster [:G,F:] -> non empty strict scalar-distributive ;
correctness
coherence
[:G,F:] is scalar-distributive ;
proof end;
end;

registration
let G, F be non empty scalar-associative RLSStruct ;
cluster [:G,F:] -> non empty strict scalar-associative ;
correctness
coherence
[:G,F:] is scalar-associative ;
proof end;
end;

registration
let G, F be non empty scalar-unital RLSStruct ;
cluster [:G,F:] -> non empty strict scalar-unital ;
correctness
coherence
[:G,F:] is scalar-unital ;
proof end;
end;

registration
let G be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;
cluster <*G*> -> RealLinearSpace-yielding ;
correctness
coherence
<*G*> is RealLinearSpace-yielding ;
proof end;
end;

registration
let G, F be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;
cluster <*G,F*> -> RealLinearSpace-yielding ;
correctness
coherence
<*G,F*> is RealLinearSpace-yielding ;
proof end;
end;

theorem Th11: :: PRVECT_3:11
for X being RealLinearSpace ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. X) = 0. (product <*X*>) )
proof end;

registration
let G, F be non empty RealLinearSpace-yielding FinSequence;
cluster G ^ F -> RealLinearSpace-yielding ;
correctness
coherence
G ^ F is RealLinearSpace-yielding ;
proof end;
end;

theorem Th12: :: PRVECT_3:12
for X, Y being RealLinearSpace ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )
proof end;

Lm2: for X being non-empty non empty FinSequence
for x being set st x in product X holds
x is FinSequence
proof end;

theorem Th13: :: PRVECT_3:13
for X, Y being RealLinearSpace-Sequence 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)) )
proof end;

theorem :: PRVECT_3:14
for G, F being RealLinearSpace holds
( ( for x being set holds
( x is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st x = <*x1,x2*> ) ) & ( for x, y being Point of (product <*G,F*>)
for x1, y1 being Point of G
for x2, y2 being Point of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*> ) & 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F
for a being Real st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )
proof end;

definition
let G, F be non empty NORMSTR ;
func prod_NORM (G,F) -> Function of [: the carrier of G, the carrier of F:],REAL means :Def6: :: PRVECT_3:def 6
 for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & it . (g,f) = |.v.| );
existence
ex b1 being Function of [: the carrier of G, the carrier of F:],REAL st
for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & b1 . (g,f) = |.v.| )
proof end;
uniqueness
for b1, b2 being Function of [: the carrier of G, the carrier of F:],REAL st ( for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & b1 . (g,f) = |.v.| ) ) & ( for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & b2 . (g,f) = |.v.| ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines prod_NORM PRVECT_3:def 6 :
for G, F being non empty NORMSTR
for b3 being Function of [: the carrier of G, the carrier of F:],REAL holds
( b3 = prod_NORM (G,F) iff for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & b3 . (g,f) = |.v.| ) );

definition
let G, F be non empty NORMSTR ;
func [:G,F:] -> non empty strict NORMSTR equals :: PRVECT_3:def 7
 NORMSTR(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)),(prod_NORM (G,F)) #);
correctness
coherence
NORMSTR(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)),(prod_NORM (G,F)) #) is non empty strict NORMSTR ;
;
end;

:: deftheorem defines [: PRVECT_3:def 7 :
for G, F being non empty NORMSTR holds [:G,F:] = NORMSTR(# [: the carrier of G, the carrier of F:],(prod_ZERO (G,F)),(prod_ADD (G,F)),(prod_MLT (G,F)),(prod_NORM (G,F)) #);

definition
let G, F be non empty NORMSTR ;
let g be Element of G;
let f be Element of F;
:: original: [
redefine func [g,f] -> Element of [:G,F:];
coherence
[g,f] is Element of [:G,F:]
proof end;
end;

registration
let G, F be RealNormSpace;
cluster [:G,F:] -> non empty discerning reflexive strict RealNormSpace-like ;
correctness
coherence
( [:G,F:] is reflexive & [:G,F:] is discerning & [:G,F:] is RealNormSpace-like );
proof end;
end;

registration
let G, F be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;
cluster [:G,F:] -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ;
correctness
coherence
( [:G,F:] is strict & [:G,F:] is reflexive & [:G,F:] is discerning & [:G,F:] is RealNormSpace-like & [:G,F:] is scalar-distributive & [:G,F:] is vector-distributive & [:G,F:] is scalar-associative & [:G,F:] is scalar-unital & [:G,F:] is Abelian & [:G,F:] is add-associative & [:G,F:] is right_zeroed & [:G,F:] is right_complementable );
proof end;
end;

registration
let G be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;
cluster <*G*> -> RealNormSpace-yielding ;
correctness
coherence
<*G*> is RealNormSpace-yielding ;
proof end;
end;

registration
let G, F be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;
cluster <*G,F*> -> RealNormSpace-yielding ;
correctness
coherence
<*G,F*> is RealNormSpace-yielding ;
proof end;
end;

theorem Th15: :: PRVECT_3:15
for X, Y being RealNormSpace ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
proof end;

theorem Th16: :: PRVECT_3:16
for X being RealNormSpace ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) & ( for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of X
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) )
proof end;

registration
let G, F be non empty RealNormSpace-yielding FinSequence;
cluster G ^ F -> non empty RealNormSpace-yielding ;
correctness
coherence
( not G ^ F is empty & G ^ F is RealNormSpace-yielding );
proof end;
end;

Lm3: for F1, F2 being FinSequence of REAL holds sqr (F1 ^ F2) = (sqr F1) ^ (sqr F2)
by RVSUM_1:144;

theorem Th17: :: PRVECT_3:17
for X, Y being RealNormSpace-Sequence 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.|| ) )
proof end;

theorem Th18: :: PRVECT_3:18
for G, F being RealNormSpace holds
( ( for x being set holds
( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]
for x1, y1 being Point of G
for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being Real st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )
proof end;

theorem Th19: :: PRVECT_3:19
for G, F being RealNormSpace holds
( ( for x being set holds
( x is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st x = <*x1,x2*> ) ) & ( for x, y being Point of (product <*G,F*>)
for x1, y1 being Point of G
for x2, y2 being Point of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*> ) & 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F
for a being Real st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) & ( for x being Point of (product <*G,F*>)
for x1 being Point of G
for x2 being Point of F st x = <*x1,x2*> holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )
proof end;

registration
let X, Y be complete RealNormSpace;
cluster [:X,Y:] -> non empty strict complete ;
coherence
[:X,Y:] is complete
proof end;
end;

theorem :: PRVECT_3:20
for X, Y being RealNormSpace-Sequence ex I being Function of (product <*(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 <*(product X),(product Y)*>) holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of (product <*(product X),(product Y)*>)
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) & ( for v being Point of (product <*(product X),(product Y)*>) holds ||.(I . v).|| = ||.v.|| ) )
proof end;

theorem Th21: :: PRVECT_3:21
for X, Y being RealLinearSpace ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] )
proof end;

theorem :: PRVECT_3:22
for X being RealLinearSpace-Sequence
for Y being RealLinearSpace ex I being Function of [:(product X),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 Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) )
proof end;

theorem Th23: :: PRVECT_3:23
for X, Y being RealNormSpace ex I being Function of [:X,Y:],[:X,(product <*Y*>):] st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
proof end;

theorem :: PRVECT_3:24
for X being RealNormSpace-Sequence
for Y being RealNormSpace ex I being Function of [:(product X),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 Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(I . v).|| = ||.v.|| ) )
proof end;