:: Cartesian Products of Family of Real Linear Spaces :: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama :: :: Received August 17, 2010 :: Copyright (c) 2010-2012 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]] ) ) proofend; 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*> ) ) proofend; 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*> ) ) proofend; 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*> ) ) proofend; registration let X, Y be non empty non-empty FinSequence; clusterX ^ Y -> non-empty ; correctness coherence X ^ Y is non-empty ; proofend; 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*> ) ) proofend; 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 ) ) proofend; 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)] proofend; 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 proofend; 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 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 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 Element of REAL for g being Point of G for f being Point of F holds b1 . (r,[g,f]) = [(r * g),(r * f)] proofend; 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 Element of 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 Element of 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 proofend; 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 Element of 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)) #); registration let G, F be non empty Abelian addLoopStr ; cluster[:G,F:] -> non empty strict Abelian ; correctness coherence [:G,F:] is Abelian ; proofend; 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 ; proofend; 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 ; proofend; 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 ; proofend; 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)] proofend; 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 ; proofend; 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 ; proofend; 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 ; proofend; 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 ; proofend; 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)] ) ) proofend; 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)] proofend; 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 ; proofend; 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 ; proofend; 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 ; proofend; 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 ; proofend; 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 ; proofend; 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 ; proofend; 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*>) ) proofend; registration let G, F be non empty RealLinearSpace-yielding FinSequence; clusterG ^ F -> RealLinearSpace-yielding ; correctness coherence G ^ F is RealLinearSpace-yielding ; proofend; 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*>) ) proofend; Lm2: for X being non empty non-empty FinSequence for x being set st x in product X holds x is FinSequence proofend; 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)) ) proofend; 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)*> ) ) proofend; begin 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.| ) proofend; 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 proofend; 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)) #); 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 ); proofend; 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 ); proofend; 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 ; proofend; 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 ; proofend; 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.|| ) ) proofend; 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.|| ) ) proofend; registration let G, F be non empty RealNormSpace-yielding FinSequence; clusterG ^ F -> non empty RealNormSpace-yielding ; correctness coherence ( not G ^ F is empty & G ^ F is RealNormSpace-yielding ); proofend; 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.|| ) ) proofend; 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.| ) ) ) proofend; 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.| ) ) ) proofend; registration let X, Y be complete RealNormSpace; cluster[:X,Y:] -> non empty strict complete ; coherence [:X,Y:] is complete proofend; 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.|| ) ) proofend; 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*>):] ) proofend; 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*>)) ) proofend; 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.|| ) ) proofend; 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.|| ) ) proofend;