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

begin

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 set 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 set 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 set 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 set 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:65;

Lm2: for G, F being non empty addLoopStr ex ADGF being Function of [:[: the carrier of G, the carrier of F:],[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for g1, g2 being Point of G
for f1, f2 being Point of F holds ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]

proof end;

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 b₁ 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 b₁ . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] by Lm2;
uniqueness
for b₁, b₂ 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 b₁ . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) & ( for g1, g2 being Point of G
for f1, f2 being Point of F holds b₂ . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) holds
b₁ = b₂

proof end;

end;

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

Lm3: for G, F being non empty RLSStruct ex MLTGF being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Element of REAL
for g being Point of G
for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)]

proof end;

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 Element of REAL
for g being Point of G
for f being Point of F holds it . (r,[g,f]) = [(r * g),(r * f)];
existence
ex b₁ being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for r being Element of REAL
for g being Point of G
for f being Point of F holds b₁ . (r,[g,f]) = [(r * g),(r * f)] by Lm3;
uniqueness
for b₁, b₂ being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st ( for r being Element of REAL
for g being Point of G
for f being Point of F holds b₁ . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Element of REAL
for g being Point of G
for f being Point of F holds b₂ . (r,[g,f]) = [(r * g),(r * f)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines prod_MLT PRVECT_3:def 2 :
for G, F being non empty RLSStruct
for b₃ being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] holds
( b₃ = prod_MLT (G,F) iff for r being Element of REAL
for g being Point of G
for f being Point of F holds b₃ . (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)) #);

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)) #);

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 number st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) )

proof end;

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;

begin

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 Element of REAL holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )

proof end;

Lm4: 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 non empty 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 number st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )

proof end;

begin

Lm5: for G, F being non empty NORMSTR ex NORMGF 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.||*> & NORMGF . (g,f) = |.v.| )

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 b₁ 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.||*> & b₁ . (g,f) = |.v.| ) by Lm5;
uniqueness
for b₁, b₂ 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.||*> & b₁ . (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.||*> & b₂ . (g,f) = |.v.| ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines prod_NORM PRVECT_3:def 6 :
for G, F being non empty NORMSTR
for b₃ being Function of [: the carrier of G, the carrier of F:],REAL holds
( b₃ = 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.||*> & b₃ . (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)) #);

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 Element of 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;

Lm6: for F1, F2 being FinSequence of REAL holds sqr (F1 ^ F2) = (sqr F1) ^ (sqr F2)
by TOPREAL7:11;

theorem Th17: :: PRVECT_3:17

for X, Y being non empty 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 number 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 number 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty 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;