:: PRVECT_3 semantic presentation 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 let D, E, F, G be non empty set ; ::_thesis: 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]] ) ) defpred S1[ set , set , set ] means ex d, e, f, g being set st ( d in D & e in E & f in F & g in G & $1 = [d,e] & $2 = [f,g] & $3 = [[d,f],[e,g]] ); A1: for x, y being set st x in [:D,E:] & y in [:F,G:] holds ex z being set st ( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) proof let x, y be set ; ::_thesis: ( x in [:D,E:] & y in [:F,G:] implies ex z being set st ( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) ) assume A2: ( x in [:D,E:] & y in [:F,G:] ) ; ::_thesis: ex z being set st ( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) consider d, e being set such that A3: ( d in D & e in E & x = [d,e] ) by A2, ZFMISC_1:def_2; consider f, g being set such that A4: ( f in F & g in G & y = [f,g] ) by A2, ZFMISC_1:def_2; ( [d,f] in [:D,F:] & [e,g] in [:E,G:] ) by A3, A4, ZFMISC_1:87; then [[d,f],[e,g]] in [:[:D,F:],[:E,G:]:] by ZFMISC_1:87; hence ex z being set st ( z in [:[:D,F:],[:E,G:]:] & S1[x,y,z] ) by A3, A4; ::_thesis: verum end; consider I being Function of [:[:D,E:],[:F,G:]:],[:[:D,F:],[:E,G:]:] such that A5: for x, y being set st x in [:D,E:] & y in [:F,G:] holds S1[x,y,I . (x,y)] from BINOP_1:sch_1(A1); A6: 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 let d, e, f, g be set ; ::_thesis: ( d in D & e in E & f in F & g in G implies I . ([d,e],[f,g]) = [[d,f],[e,g]] ) assume A7: ( d in D & e in E & f in F & g in G ) ; ::_thesis: I . ([d,e],[f,g]) = [[d,f],[e,g]] A8: ( [d,e] in [:D,E:] & [f,g] in [:F,G:] ) by A7, ZFMISC_1:87; consider d1, e1, f1, g1 being set such that A9: ( d1 in D & e1 in E & f1 in F & g1 in G & [d,e] = [d1,e1] & [f,g] = [f1,g1] & I . ([d,e],[f,g]) = [[d1,f1],[e1,g1]] ) by A8, A5; ( d1 = d & e1 = e & f1 = f & g1 = g ) by A9, XTUPLE_0:1; hence I . ([d,e],[f,g]) = [[d,f],[e,g]] by A9; ::_thesis: verum end; A10: I is one-to-one proof now__::_thesis:_for_z1,_z2_being_set_st_z1_in_[:[:D,E:],[:F,G:]:]_&_z2_in_[:[:D,E:],[:F,G:]:]_&_I_._z1_=_I_._z2_holds_ z1_=_z2 let z1, z2 be set ; ::_thesis: ( z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 implies z1 = z2 ) assume A11: ( z1 in [:[:D,E:],[:F,G:]:] & z2 in [:[:D,E:],[:F,G:]:] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2 consider de1, fg1 being set such that A12: ( de1 in [:D,E:] & fg1 in [:F,G:] & z1 = [de1,fg1] ) by A11, ZFMISC_1:def_2; consider d1, e1 being set such that A13: ( d1 in D & e1 in E & de1 = [d1,e1] ) by A12, ZFMISC_1:def_2; consider f1, g1 being set such that A14: ( f1 in F & g1 in G & fg1 = [f1,g1] ) by A12, ZFMISC_1:def_2; consider de2, fg2 being set such that A15: ( de2 in [:D,E:] & fg2 in [:F,G:] & z2 = [de2,fg2] ) by A11, ZFMISC_1:def_2; consider d2, e2 being set such that A16: ( d2 in D & e2 in E & de2 = [d2,e2] ) by A15, ZFMISC_1:def_2; consider f2, g2 being set such that A17: ( f2 in F & g2 in G & fg2 = [f2,g2] ) by A15, ZFMISC_1:def_2; [[d1,f1],[e1,g1]] = I . ([d1,e1],[f1,g1]) by A6, A13, A14 .= I . ([d2,e2],[f2,g2]) by A11, A12, A13, A14, A15, A16, A17 .= [[d2,f2],[e2,g2]] by A6, A16, A17 ; then ( [d1,f1] = [d2,f2] & [e1,g1] = [e2,g2] ) by XTUPLE_0:1; then ( d1 = d2 & f1 = f2 & e1 = e2 & g1 = g2 ) by XTUPLE_0:1; hence z1 = z2 by A12, A13, A14, A15, A16, A17; ::_thesis: verum end; hence I is one-to-one by FUNCT_2:19; ::_thesis: verum end; I is onto proof now__::_thesis:_for_w_being_set_st_w_in_[:[:D,F:],[:E,G:]:]_holds_ w_in_rng_I let w be set ; ::_thesis: ( w in [:[:D,F:],[:E,G:]:] implies w in rng I ) assume A18: w in [:[:D,F:],[:E,G:]:] ; ::_thesis: w in rng I consider df, eg being set such that A19: ( df in [:D,F:] & eg in [:E,G:] & w = [df,eg] ) by A18, ZFMISC_1:def_2; consider d, f being set such that A20: ( d in D & f in F & df = [d,f] ) by A19, ZFMISC_1:def_2; consider e, g being set such that A21: ( e in E & g in G & eg = [e,g] ) by A19, ZFMISC_1:def_2; A22: ( [d,e] in [:D,E:] & [f,g] in [:F,G:] ) by A20, A21, ZFMISC_1:87; reconsider z = [[d,e],[f,g]] as Element of [:[:D,E:],[:F,G:]:] by A22, ZFMISC_1:87; w = I . ([d,e],[f,g]) by A6, A19, A20, A21; then w = I . z ; hence w in rng I by FUNCT_2:112; ::_thesis: verum end; then [:[:D,F:],[:E,G:]:] c= rng I by TARSKI:def_3; then [:[:D,F:],[:E,G:]:] = rng I by XBOOLE_0:def_10; hence I is onto by FUNCT_2:def_3; ::_thesis: verum end; hence 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]] ) ) by A6, A10; ::_thesis: verum 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 let X be non empty set ; ::_thesis: 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*> ) ) let D be Function; ::_thesis: ( dom D = {1} & D . 1 = X implies 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*> ) ) ) assume A1: ( dom D = {1} & D . 1 = X ) ; ::_thesis: 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*> ) ) defpred S1[ set , set ] means $2 = <*$1*>; A2: for x being set st x in X holds ex z being set st ( z in product D & S1[x,z] ) proof let x be set ; ::_thesis: ( x in X implies ex z being set st ( z in product D & S1[x,z] ) ) assume A3: x in X ; ::_thesis: ex z being set st ( z in product D & S1[x,z] ) A4: dom <*x*> = Seg (len <*x*>) by FINSEQ_1:def_3 .= {1} by FINSEQ_1:2, FINSEQ_1:40 ; now__::_thesis:_for_i_being_set_st_i_in_dom_<*x*>_holds_ <*x*>_._i_in_D_._i let i be set ; ::_thesis: ( i in dom <*x*> implies <*x*> . i in D . i ) assume i in dom <*x*> ; ::_thesis: <*x*> . i in D . i then i = 1 by A4, TARSKI:def_1; hence <*x*> . i in D . i by A1, A3, FINSEQ_1:40; ::_thesis: verum end; then <*x*> in product D by A4, A1, CARD_3:9; hence ex z being set st ( z in product D & S1[x,z] ) ; ::_thesis: verum end; consider I being Function of X,(product D) such that A5: for x being set st x in X holds S1[x,I . x] from FUNCT_2:sch_1(A2); now__::_thesis:_not_{}_in_rng_D assume {} in rng D ; ::_thesis: contradiction then ex x being set st ( x in dom D & D . x = {} ) by FUNCT_1:def_3; hence contradiction by A1, TARSKI:def_1; ::_thesis: verum end; then A6: product D <> {} by CARD_3:26; now__::_thesis:_for_z1,_z2_being_set_st_z1_in_X_&_z2_in_X_&_I_._z1_=_I_._z2_holds_ z1_=_z2 let z1, z2 be set ; ::_thesis: ( z1 in X & z2 in X & I . z1 = I . z2 implies z1 = z2 ) assume A7: ( z1 in X & z2 in X & I . z1 = I . z2 ) ; ::_thesis: z1 = z2 <*z1*> = I . z1 by A5, A7 .= <*z2*> by A5, A7 ; hence z1 = z2 by FINSEQ_1:76; ::_thesis: verum end; then A8: I is one-to-one by A6, FUNCT_2:19; now__::_thesis:_for_w_being_set_st_w_in_product_D_holds_ w_in_rng_I let w be set ; ::_thesis: ( w in product D implies w in rng I ) assume w in product D ; ::_thesis: w in rng I then consider g being Function such that A9: ( w = g & dom g = dom D & ( for i being set st i in dom D holds g . i in D . i ) ) by CARD_3:def_5; reconsider g = g as FinSequence by A1, A9, FINSEQ_1:2, FINSEQ_1:def_2; set x = g . 1; A10: len g = 1 by A1, A9, FINSEQ_1:2, FINSEQ_1:def_3; 1 in dom D by A1, TARSKI:def_1; then A11: ( g . 1 in X & w = <*(g . 1)*> ) by A9, A10, A1, FINSEQ_1:40; then w = I . (g . 1) by A5; hence w in rng I by A11, A6, FUNCT_2:112; ::_thesis: verum end; then product D c= rng I by TARSKI:def_3; then product D = rng I by XBOOLE_0:def_10; then I is onto by FUNCT_2:def_3; hence 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*> ) ) by A5, A8; ::_thesis: verum 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 let X, Y be non empty set ; ::_thesis: 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*> ) ) let D be Function; ::_thesis: ( dom D = {1,2} & D . 1 = X & D . 2 = Y implies 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*> ) ) ) assume A1: ( dom D = {1,2} & D . 1 = X & D . 2 = Y ) ; ::_thesis: 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*> ) ) defpred S1[ set , set , set ] means $3 = <*$1,$2*>; A2: for x, y being set st x in X & y in Y holds ex z being set st ( z in product D & S1[x,y,z] ) proof let x, y be set ; ::_thesis: ( x in X & y in Y implies ex z being set st ( z in product D & S1[x,y,z] ) ) assume A3: ( x in X & y in Y ) ; ::_thesis: ex z being set st ( z in product D & S1[x,y,z] ) A4: dom <*x,y*> = Seg (len <*x,y*>) by FINSEQ_1:def_3 .= {1,2} by FINSEQ_1:2, FINSEQ_1:44 ; now__::_thesis:_for_i_being_set_st_i_in_dom_<*x,y*>_holds_ <*x,y*>_._i_in_D_._i let i be set ; ::_thesis: ( i in dom <*x,y*> implies <*x,y*> . i in D . i ) assume i in dom <*x,y*> ; ::_thesis: <*x,y*> . i in D . i then ( i = 1 or i = 2 ) by A4, TARSKI:def_2; hence <*x,y*> . i in D . i by A1, A3, FINSEQ_1:44; ::_thesis: verum end; then <*x,y*> in product D by A4, A1, CARD_3:9; hence ex z being set st ( z in product D & S1[x,y,z] ) ; ::_thesis: verum end; consider I being Function of [:X,Y:],(product D) such that A5: for x, y being set st x in X & y in Y holds S1[x,y,I . (x,y)] from BINOP_1:sch_1(A2); now__::_thesis:_not_{}_in_rng_D assume {} in rng D ; ::_thesis: contradiction then ex x being set st ( x in dom D & D . x = {} ) by FUNCT_1:def_3; hence contradiction by A1, TARSKI:def_2; ::_thesis: verum end; then A6: product D <> {} by CARD_3:26; now__::_thesis:_for_z1,_z2_being_set_st_z1_in_[:X,Y:]_&_z2_in_[:X,Y:]_&_I_._z1_=_I_._z2_holds_ z1_=_z2 let z1, z2 be set ; ::_thesis: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 implies z1 = z2 ) assume A7: ( z1 in [:X,Y:] & z2 in [:X,Y:] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2 then consider x1, y1 being set such that A8: ( x1 in X & y1 in Y & z1 = [x1,y1] ) by ZFMISC_1:def_2; consider x2, y2 being set such that A9: ( x2 in X & y2 in Y & z2 = [x2,y2] ) by A7, ZFMISC_1:def_2; <*x1,y1*> = I . (x1,y1) by A5, A8 .= I . (x2,y2) by A7, A8, A9 .= <*x2,y2*> by A5, A9 ; then ( x1 = x2 & y1 = y2 ) by FINSEQ_1:77; hence z1 = z2 by A8, A9; ::_thesis: verum end; then A10: I is one-to-one by A6, FUNCT_2:19; now__::_thesis:_for_w_being_set_st_w_in_product_D_holds_ w_in_rng_I let w be set ; ::_thesis: ( w in product D implies w in rng I ) assume w in product D ; ::_thesis: w in rng I then consider g being Function such that A11: ( w = g & dom g = dom D & ( for i being set st i in dom D holds g . i in D . i ) ) by CARD_3:def_5; reconsider g = g as FinSequence by A1, A11, FINSEQ_1:2, FINSEQ_1:def_2; set x = g . 1; set y = g . 2; A12: len g = 2 by A1, A11, FINSEQ_1:2, FINSEQ_1:def_3; ( 1 in dom D & 2 in dom D ) by A1, TARSKI:def_2; then A13: ( g . 1 in X & g . 2 in Y & w = <*(g . 1),(g . 2)*> ) by A11, A12, A1, FINSEQ_1:44; reconsider z = [(g . 1),(g . 2)] as Element of [:X,Y:] by A13, ZFMISC_1:87; w = I . ((g . 1),(g . 2)) by A5, A13 .= I . z ; hence w in rng I by A6, FUNCT_2:112; ::_thesis: verum end; then product D c= rng I by TARSKI:def_3; then product D = rng I by XBOOLE_0:def_10; then I is onto by FUNCT_2:def_3; hence 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*> ) ) by A5, A10; ::_thesis: verum 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 let X be non empty set ; ::_thesis: 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*> ) ) ( dom <*X*> = {1} & <*X*> . 1 = X ) by FINSEQ_1:2, FINSEQ_1:38, FINSEQ_1:40; hence 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*> ) ) by Th2; ::_thesis: verum end; registration let X, Y be non empty non-empty FinSequence; clusterX ^ Y -> non-empty ; correctness coherence X ^ Y is non-empty ; proof now__::_thesis:_for_z_being_set_st_z_in_dom_(X_^_Y)_holds_ not_(X_^_Y)_._z_is_empty let z be set ; ::_thesis: ( z in dom (X ^ Y) implies not (X ^ Y) . b1 is empty ) assume A1: z in dom (X ^ Y) ; ::_thesis: not (X ^ Y) . b1 is empty then reconsider k = z as Element of NAT ; percases ( k in dom X or ex n being Nat st ( n in dom Y & k = (len X) + n ) ) by A1, FINSEQ_1:25; supposeA2: k in dom X ; ::_thesis: not (X ^ Y) . b1 is empty then X . k = (X ^ Y) . k by FINSEQ_1:def_7; hence not (X ^ Y) . z is empty by A2; ::_thesis: verum end; suppose ex n being Nat st ( n in dom Y & k = (len X) + n ) ; ::_thesis: not (X ^ Y) . b1 is empty then consider n being Nat such that A3: ( n in dom Y & k = (len X) + n ) ; Y . n = (X ^ Y) . k by A3, FINSEQ_1:def_7; hence not (X ^ Y) . z is empty by A3; ::_thesis: verum end; end; end; hence X ^ Y is non-empty by FUNCT_1:def_9; ::_thesis: verum 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 let X, Y be non empty set ; ::_thesis: 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*> ) ) ( dom <*X,Y*> = {1,2} & <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:2, FINSEQ_1:44, FINSEQ_1:89; hence 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*> ) ) by Th3; ::_thesis: verum 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 let X, Y be non empty non-empty FinSequence; ::_thesis: 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 ) ) defpred S1[ set , set , set ] means ex x, y being FinSequence st ( x = $1 & y = $2 & $3 = x ^ y ); A1: for x, y being set st x in product X & y in product Y holds ex z being set st ( z in product (X ^ Y) & S1[x,y,z] ) proof let x, y be set ; ::_thesis: ( x in product X & y in product Y implies ex z being set st ( z in product (X ^ Y) & S1[x,y,z] ) ) assume A2: ( x in product X & y in product Y ) ; ::_thesis: ex z being set st ( z in product (X ^ Y) & S1[x,y,z] ) then consider g being Function such that A3: ( x = g & dom g = dom X & ( for z being set st z in dom X holds g . z in X . z ) ) by CARD_3:def_5; A4: dom g = Seg (len X) by A3, FINSEQ_1:def_3; then reconsider g = g as FinSequence by FINSEQ_1:def_2; consider h being Function such that A5: ( y = h & dom h = dom Y & ( for z being set st z in dom Y holds h . z in Y . z ) ) by A2, CARD_3:def_5; A6: dom h = Seg (len Y) by A5, FINSEQ_1:def_3; then reconsider h = h as FinSequence by FINSEQ_1:def_2; A7: ( len g = len X & len h = len Y ) by A4, A6, FINSEQ_1:def_3; A8: dom (g ^ h) = Seg ((len g) + (len h)) by FINSEQ_1:def_7 .= Seg (len (X ^ Y)) by A7, FINSEQ_1:22 .= dom (X ^ Y) by FINSEQ_1:def_3 ; for z being set st z in dom (X ^ Y) holds (g ^ h) . z in (X ^ Y) . z proof let z be set ; ::_thesis: ( z in dom (X ^ Y) implies (g ^ h) . z in (X ^ Y) . z ) assume A9: z in dom (X ^ Y) ; ::_thesis: (g ^ h) . z in (X ^ Y) . z then reconsider k = z as Element of NAT ; percases ( k in dom X or ex n being Nat st ( n in dom Y & k = (len X) + n ) ) by A9, FINSEQ_1:25; supposeA10: k in dom X ; ::_thesis: (g ^ h) . z in (X ^ Y) . z then A11: g . k in X . k by A3; g . k = (g ^ h) . k by A10, A3, FINSEQ_1:def_7; hence (g ^ h) . z in (X ^ Y) . z by A11, A10, FINSEQ_1:def_7; ::_thesis: verum end; suppose ex n being Nat st ( n in dom Y & k = (len X) + n ) ; ::_thesis: (g ^ h) . z in (X ^ Y) . z then consider n being Nat such that A12: ( n in dom Y & k = (len X) + n ) ; A13: h . n in Y . n by A12, A5; h . n = (g ^ h) . k by A12, A7, A5, FINSEQ_1:def_7; hence (g ^ h) . z in (X ^ Y) . z by A13, A12, FINSEQ_1:def_7; ::_thesis: verum end; end; end; then g ^ h in product (X ^ Y) by A8, CARD_3:9; hence ex z being set st ( z in product (X ^ Y) & S1[x,y,z] ) by A3, A5; ::_thesis: verum end; consider I being Function of [:(product X),(product Y):],(product (X ^ Y)) such that A14: for x, y being set st x in product X & y in product Y holds S1[x,y,I . (x,y)] from BINOP_1:sch_1(A1); A15: for x, y being FinSequence st x in product X & y in product Y holds I . (x,y) = x ^ y proof let x, y be FinSequence; ::_thesis: ( x in product X & y in product Y implies I . (x,y) = x ^ y ) assume ( x in product X & y in 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 A14; hence I . (x,y) = x ^ y ; ::_thesis: verum end; now__::_thesis:_for_z1,_z2_being_set_st_z1_in_[:(product_X),(product_Y):]_&_z2_in_[:(product_X),(product_Y):]_&_I_._z1_=_I_._z2_holds_ z1_=_z2 let z1, z2 be set ; ::_thesis: ( z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 implies z1 = z2 ) assume A16: ( z1 in [:(product X),(product Y):] & z2 in [:(product X),(product Y):] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2 consider x1, y1 being set such that A17: ( x1 in product X & y1 in product Y & z1 = [x1,y1] ) by A16, ZFMISC_1:def_2; consider x2, y2 being set such that A18: ( x2 in product X & y2 in product Y & z2 = [x2,y2] ) by A16, ZFMISC_1:def_2; consider xx1, yy1 being FinSequence such that A19: ( xx1 = x1 & yy1 = y1 & I . (x1,y1) = xx1 ^ yy1 ) by A14, A17; consider xx2, yy2 being FinSequence such that A20: ( xx2 = x2 & yy2 = y2 & I . (x2,y2) = xx2 ^ yy2 ) by A14, A18; A21: dom xx1 = dom X by A17, A19, CARD_3:9 .= dom xx2 by A18, A20, CARD_3:9 ; xx1 = (xx1 ^ yy1) | (dom xx1) by FINSEQ_1:21 .= xx2 by A16, A17, A18, A19, A20, A21, FINSEQ_1:21 ; hence z1 = z2 by A16, A17, A18, A19, A20, FINSEQ_1:33; ::_thesis: verum end; then A22: I is one-to-one by FUNCT_2:19; now__::_thesis:_for_w_being_set_st_w_in_product_(X_^_Y)_holds_ w_in_rng_I let w be set ; ::_thesis: ( w in product (X ^ Y) implies w in rng I ) assume w in product (X ^ Y) ; ::_thesis: w in rng I then consider g being Function such that A23: ( w = g & dom g = dom (X ^ Y) & ( for i being set st i in dom (X ^ Y) holds g . i in (X ^ Y) . i ) ) by CARD_3:def_5; A24: dom g = Seg (len (X ^ Y)) by A23, FINSEQ_1:def_3; then reconsider g = g as FinSequence by FINSEQ_1:def_2; set x = g | (len X); set y = g /^ (len X); A25: g is FinSequence of rng g by FINSEQ_1:def_4; rng g <> {} by A23, RELAT_1:42; then A26: (g | (len X)) ^ (g /^ (len X)) = g by A25, RFINSEQ:8; A27: len (X ^ Y) = (len X) + (len Y) by FINSEQ_1:22; then A28: len X <= len (X ^ Y) by NAT_1:11; A29: len g = len (X ^ Y) by A24, FINSEQ_1:def_3; then len (g | (len X)) = len X by A27, FINSEQ_1:59, NAT_1:11; then A30: dom (g | (len X)) = Seg (len X) by FINSEQ_1:def_3 .= dom X by FINSEQ_1:def_3 ; for z being set st z in dom X holds (g | (len X)) . z in X . z proof let z be set ; ::_thesis: ( z in dom X implies (g | (len X)) . z in X . z ) assume A31: z in dom X ; ::_thesis: (g | (len X)) . z in X . z then reconsider k = z as Element of NAT ; A32: dom X c= dom (X ^ Y) by FINSEQ_1:26; A33: (g | (len X)) . k = g . k by A31, A26, A30, FINSEQ_1:def_7; X . k = (X ^ Y) . k by A31, FINSEQ_1:def_7; hence (g | (len X)) . z in X . z by A33, A23, A31, A32; ::_thesis: verum end; then A34: g | (len X) in product X by A30, CARD_3:9; dom (g | (len X)) = Seg (len X) by A30, FINSEQ_1:def_3; then A35: len (g | (len X)) = len X by FINSEQ_1:def_3; len (g /^ (len X)) = (len g) - (len X) by A28, A29, RFINSEQ:def_1 .= len Y by A29, A27 ; then Seg (len (g /^ (len X))) = dom Y by FINSEQ_1:def_3; then A36: dom (g /^ (len X)) = dom Y by FINSEQ_1:def_3; for z being set st z in dom Y holds (g /^ (len X)) . z in Y . z proof let z be set ; ::_thesis: ( z in dom Y implies (g /^ (len X)) . z in Y . z ) assume A37: z in dom Y ; ::_thesis: (g /^ (len X)) . z in Y . z then reconsider k = z as Element of NAT ; A38: (g /^ (len X)) . k = g . ((len X) + k) by A37, A26, A35, A36, FINSEQ_1:def_7; Y . k = (X ^ Y) . ((len X) + k) by A37, FINSEQ_1:def_7; hence (g /^ (len X)) . z in Y . z by A38, A23, A37, FINSEQ_1:28; ::_thesis: verum end; then A39: g /^ (len X) in product Y by A36, CARD_3:9; reconsider z = [(g | (len X)),(g /^ (len X))] as Element of [:(product X),(product Y):] by A34, A39, ZFMISC_1:87; w = I . ((g | (len X)),(g /^ (len X))) by A23, A26, A15, A34, A39 .= I . z ; hence w in rng I by FUNCT_2:112; ::_thesis: verum end; then product (X ^ Y) c= rng I by TARSKI:def_3; then product (X ^ Y) = rng I by XBOOLE_0:def_10; then I is onto by FUNCT_2:def_3; hence 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 ) ) by A15, A22; ::_thesis: verum 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 defpred S1[ set , set , set ] means ex g1, g2 being Point of G ex f1, f2 being Point of F st ( $1 = [g1,f1] & $2 = [g2,f2] & $3 = [(g1 + g2),(f1 + f2)] ); A1: for x, y being set st x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] holds ex z being set st ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) proof let x, y be set ; ::_thesis: ( x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] implies ex z being set st ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) ) assume A2: ( x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] ) ; ::_thesis: ex z being set st ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) then consider x1 being Point of G, x2 being Point of F such that A3: x = [x1,x2] by Lm1; consider y1 being Point of G, y2 being Point of F such that A4: y = [y1,y2] by Lm1, A2; reconsider z = [(x1 + y1),(x2 + y2)] as Element of [: the carrier of G, the carrier of F:] ; ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) by A3, A4; hence ex z being set st ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) ; ::_thesis: verum end; consider 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:] such that A5: for x, y being set st x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] holds S1[x,y,ADGF . (x,y)] from BINOP_1:sch_1(A1); now__::_thesis:_for_g1,_g2_being_Point_of_G for_f1,_f2_being_Point_of_F_holds_ADGF_._([g1,f1],[g2,f2])_=_[(g1_+_g2),(f1_+_f2)] let g1, g2 be Point of G; ::_thesis: for f1, f2 being Point of F holds ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] let f1, f2 be Point of F; ::_thesis: ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] consider gg1, gg2 being Point of G, ff1, ff2 being Point of F such that A6: ( [g1,f1] = [gg1,ff1] & [g2,f2] = [gg2,ff2] & ADGF . ([g1,f1],[g2,f2]) = [(gg1 + gg2),(ff1 + ff2)] ) by A5; ( g1 = gg1 & f1 = ff1 & g2 = gg2 & f2 = ff2 ) by A6, XTUPLE_0:1; hence ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] by A6; ::_thesis: verum end; hence 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)] ; ::_thesis: verum 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 let H1, H2 be BinOp of [: the carrier of G, the carrier of F:]; ::_thesis: ( ( for g1, g2 being Point of G for f1, f2 being Point of F holds H1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) & ( for g1, g2 being Point of G for f1, f2 being Point of F holds H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ) implies H1 = H2 ) assume A7: for g1, g2 being Point of G for f1, f2 being Point of F holds H1 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ; ::_thesis: ( ex g1, g2 being Point of G ex f1, f2 being Point of F st not H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] or H1 = H2 ) assume A8: for g1, g2 being Point of G for f1, f2 being Point of F holds H2 . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ; ::_thesis: H1 = H2 now__::_thesis:_for_x,_y_being_Element_of_[:_the_carrier_of_G,_the_carrier_of_F:]_holds_H1_._(x,y)_=_H2_._(x,y) let x, y be Element of [: the carrier of G, the carrier of F:]; ::_thesis: H1 . (x,y) = H2 . (x,y) consider x1 being Point of G, x2 being Point of F such that A9: x = [x1,x2] by Lm1; consider y1 being Point of G, y2 being Point of F such that A10: y = [y1,y2] by Lm1; thus H1 . (x,y) = [(x1 + y1),(x2 + y2)] by A7, A9, A10 .= H2 . (x,y) by A8, A9, A10 ; ::_thesis: verum end; hence H1 = H2 by BINOP_1:2; ::_thesis: verum 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 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)] proof defpred S1[ set , set , set ] means ex r being Element of REAL ex g being Point of G ex f being Point of F st ( r = $1 & $2 = [g,f] & $3 = [(r * g),(r * f)] ); set CarrG = the carrier of G; set CarrF = the carrier of F; A1: for x, y being set st x in REAL & y in [: the carrier of G, the carrier of F:] holds ex z being set st ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) proof let x, y be set ; ::_thesis: ( x in REAL & y in [: the carrier of G, the carrier of F:] implies ex z being set st ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) ) assume A2: ( x in REAL & y in [: the carrier of G, the carrier of F:] ) ; ::_thesis: ex z being set st ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) then reconsider r = x as Element of REAL ; consider y1 being Point of G, y2 being Point of F such that A3: y = [y1,y2] by A2, Lm1; set z = [(r * y1),(r * y2)]; ( [(r * y1),(r * y2)] in [: the carrier of G, the carrier of F:] & S1[x,y,[(r * y1),(r * y2)]] ) by A3; hence ex z being set st ( z in [: the carrier of G, the carrier of F:] & S1[x,y,z] ) ; ::_thesis: verum end; consider MLTGF being Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] such that A4: for x, y being set st x in REAL & y in [: the carrier of G, the carrier of F:] holds S1[x,y,MLTGF . (x,y)] from BINOP_1:sch_1(A1); now__::_thesis:_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)] let r be Element of REAL ; ::_thesis: for g being Point of G for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)] let g be Point of G; ::_thesis: for f being Point of F holds MLTGF . (r,[g,f]) = [(r * g),(r * f)] let f be Point of F; ::_thesis: MLTGF . (r,[g,f]) = [(r * g),(r * f)] S1[r,[g,f],MLTGF . (r,[g,f])] by A4; then consider rr being Element of REAL , gg being Point of G, ff being Point of F such that A5: ( rr = r & [g,f] = [gg,ff] & MLTGF . (r,[g,f]) = [(rr * gg),(r * ff)] ) ; ( g = gg & f = ff ) by A5, XTUPLE_0:1; hence MLTGF . (r,[g,f]) = [(r * g),(r * f)] by A5; ::_thesis: verum end; hence 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)] ; ::_thesis: verum 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 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 proof let H1, H2 be Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:]; ::_thesis: ( ( for r being Element of REAL for g being Point of G for f being Point of F holds H1 . (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 H2 . (r,[g,f]) = [(r * g),(r * f)] ) implies H1 = H2 ) assume A6: for r being Element of REAL for g being Point of G for f being Point of F holds H1 . (r,[g,f]) = [(r * g),(r * f)] ; ::_thesis: ( ex r being Element of REAL ex g being Point of G ex f being Point of F st not H2 . (r,[g,f]) = [(r * g),(r * f)] or H1 = H2 ) assume A7: for r being Element of REAL for g being Point of G for f being Point of F holds H2 . (r,[g,f]) = [(r * g),(r * f)] ; ::_thesis: H1 = H2 now__::_thesis:_for_r_being_Element_of_REAL_ for_x_being_Element_of_[:_the_carrier_of_G,_the_carrier_of_F:]_holds_H1_._(r,x)_=_H2_._(r,x) let r be Element of REAL ; ::_thesis: for x being Element of [: the carrier of G, the carrier of F:] holds H1 . (r,x) = H2 . (r,x) let x be Element of [: the carrier of G, the carrier of F:]; ::_thesis: H1 . (r,x) = H2 . (r,x) consider x1 being Point of G, x2 being Point of F such that A8: x = [x1,x2] by Lm1; thus H1 . (r,x) = [(r * x1),(r * x2)] by A6, A8 .= H2 . (r,x) by A7, A8 ; ::_thesis: verum end; hence H1 = H2 by BINOP_1:2; ::_thesis: verum 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 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 ; proof let x, y be Element of [:G,F:]; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; consider y1 being Point of G, y2 being Point of F such that A2: y = [y1,y2] by Lm1; thus x + y = [(x1 + y1),(x2 + y2)] by A1, A2, Def1 .= y + x by A1, A2, Def1 ; ::_thesis: verum 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 let x, y, z be Element of [:G,F:]; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z) consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; consider y1 being Point of G, y2 being Point of F such that A2: y = [y1,y2] by Lm1; consider z1 being Point of G, z2 being Point of F such that A3: z = [z1,z2] by Lm1; A4: ( (x1 + y1) + z1 = x1 + (y1 + z1) & (x2 + y2) + z2 = x2 + (y2 + z2) ) by RLVECT_1:def_3; thus (x + y) + z = (prod_ADD (G,F)) . ([(x1 + y1),(x2 + y2)],[z1,z2]) by A1, A2, A3, Def1 .= [((x1 + y1) + z1),((x2 + y2) + z2)] by Def1 .= (prod_ADD (G,F)) . ([x1,x2],[(y1 + z1),(y2 + z2)]) by A4, Def1 .= x + (y + z) by A1, A2, A3, Def1 ; ::_thesis: verum 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 let x be Element of [:G,F:]; :: according to RLVECT_1:def_4 ::_thesis: x + (0. [:G,F:]) = x consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; ( x1 + (0. G) = x1 & x2 + (0. F) = x2 ) by RLVECT_1:def_4; hence x + (0. [:G,F:]) = x by A1, Def1; ::_thesis: verum 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 let x be Element of [:G,F:]; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; consider y1 being Point of G such that A2: x1 + y1 = 0. G by ALGSTR_0:def_11; consider y2 being Point of F such that A3: x2 + y2 = 0. F by ALGSTR_0:def_11; reconsider y = [y1,y2] as Element of [:G,F:] ; take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. [:G,F:] thus x + y = 0. [:G,F:] by A1, A2, A3, Def1; ::_thesis: verum 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 let G, F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: 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)] let x be Point of [:G,F:]; ::_thesis: for x1 being Point of G for x2 being Point of F st x = [x1,x2] holds - x = [(- x1),(- x2)] let x1 be Point of G; ::_thesis: for x2 being Point of F st x = [x1,x2] holds - x = [(- x1),(- x2)] let x2 be Point of F; ::_thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] ) assume A1: x = [x1,x2] ; ::_thesis: - x = [(- x1),(- x2)] reconsider y = [(- x1),(- x2)] as Point of [:G,F:] ; x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, Def1 .= [(0. G),(x2 + (- x2))] by RLVECT_1:def_10 .= 0. [:G,F:] by RLVECT_1:def_10 ; hence - x = [(- x1),(- x2)] by RLVECT_1:def_10; ::_thesis: verum 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 let x, y be Element of [:G,F:]; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; consider y1 being Point of G, y2 being Point of F such that A2: y = [y1,y2] by Lm1; x + y = [(x1 + y1),(x2 + y2)] by A1, A2, Def1; hence x + y = y + x by A1, A2, Def1; ::_thesis: verum 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 let x, y, z be Element of [:G,F:]; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z) consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; consider y1 being Point of G, y2 being Point of F such that A2: y = [y1,y2] by Lm1; consider z1 being Point of G, z2 being Point of F such that A3: z = [z1,z2] by Lm1; A4: ( (x1 + y1) + z1 = x1 + (y1 + z1) & (x2 + y2) + z2 = x2 + (y2 + z2) ) by RLVECT_1:def_3; thus (x + y) + z = (prod_ADD (G,F)) . ([(x1 + y1),(x2 + y2)],[z1,z2]) by A1, A2, A3, Def1 .= [(x1 + (y1 + z1)),(x2 + (y2 + z2))] by A4, Def1 .= (prod_ADD (G,F)) . ([x1,x2],[(y1 + z1),(y2 + z2)]) by Def1 .= x + (y + z) by A1, A2, A3, Def1 ; ::_thesis: verum 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 let x be Element of [:G,F:]; :: according to RLVECT_1:def_4 ::_thesis: x + (0. [:G,F:]) = x consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; ( x1 + (0. G) = x1 & x2 + (0. F) = x2 ) by RLVECT_1:def_4; hence x + (0. [:G,F:]) = x by A1, Def1; ::_thesis: verum 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 let x be Element of [:G,F:]; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; consider y1 being Point of G such that A2: x1 + y1 = 0. G by ALGSTR_0:def_11; consider y2 being Point of F such that A3: x2 + y2 = 0. F by ALGSTR_0:def_11; reconsider y = [y1,y2] as Element of [:G,F:] ; take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. [:G,F:] thus x + y = 0. [:G,F:] by A1, A2, A3, Def1; ::_thesis: verum 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 let G, F be non empty RLSStruct ; ::_thesis: ( ( 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)] ) ) 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 let x be Point of [:G,F:]; ::_thesis: 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)] let x1 be Point of G; ::_thesis: for x2 being Point of F for a being real number st x = [x1,x2] holds a * x = [(a * x1),(a * x2)] let x2 be Point of F; ::_thesis: for a being real number st x = [x1,x2] holds a * x = [(a * x1),(a * x2)] let a be real number ; ::_thesis: ( x = [x1,x2] implies a * x = [(a * x1),(a * x2)] ) reconsider a0 = a as Element of REAL by XREAL_0:def_1; assume A1: x = [x1,x2] ; ::_thesis: a * x = [(a * x1),(a * x2)] a * x = (prod_MLT (G,F)) . (a0,x) ; hence a * x = [(a * x1),(a * x2)] by A1, Def2; ::_thesis: verum end; hence ( ( 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)] ) ) by Def1, Lm1; ::_thesis: verum 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 let G, F be non empty right_complementable add-associative right_zeroed RLSStruct ; ::_thesis: 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)] let x be Point of [:G,F:]; ::_thesis: for x1 being Point of G for x2 being Point of F st x = [x1,x2] holds - x = [(- x1),(- x2)] let x1 be Point of G; ::_thesis: for x2 being Point of F st x = [x1,x2] holds - x = [(- x1),(- x2)] let x2 be Point of F; ::_thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] ) assume A1: x = [x1,x2] ; ::_thesis: - x = [(- x1),(- x2)] reconsider y = [(- x1),(- x2)] as Point of [:G,F:] ; x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, Def1 .= [(0. G),(x2 + (- x2))] by RLVECT_1:def_10 .= 0. [:G,F:] by RLVECT_1:def_10 ; hence - x = [(- x1),(- x2)] by RLVECT_1:def_10; ::_thesis: verum 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 let a0 be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of [:G,F:] holds a0 * (b1 + b2) = (a0 * b1) + (a0 * b2) let x, y be VECTOR of [:G,F:]; ::_thesis: a0 * (x + y) = (a0 * x) + (a0 * y) reconsider a = a0 as Element of REAL by XREAL_0:def_1; consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; consider y1 being Point of G, y2 being Point of F such that A2: y = [y1,y2] by Lm1; A3: ( a * (x1 + y1) = (a0 * x1) + (a0 * y1) & a * (x2 + y2) = (a0 * x2) + (a0 * y2) ) by RLVECT_1:def_5; thus a0 * (x + y) = (prod_MLT (G,F)) . (a,[(x1 + y1),(x2 + y2)]) by A1, A2, Def1 .= [(a * (x1 + y1)),(a * (x2 + y2))] by Def2 .= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(a * y1),(a * y2)]) by A3, Def1 .= (prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(a * y1),(a * y2)]) by Def2 .= (a0 * x) + (a0 * y) by A1, A2, Def2 ; ::_thesis: verum 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 let a0, b0 be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of [:G,F:] holds (a0 + b0) * b1 = (a0 * b1) + (b0 * b1) let x be VECTOR of [:G,F:]; ::_thesis: (a0 + b0) * x = (a0 * x) + (b0 * x) reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def_1; consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; A2: ( (a + b) * x1 = (a0 * x1) + (b0 * x1) & (a + b) * x2 = (a0 * x2) + (b0 * x2) ) by RLVECT_1:def_6; thus (a0 + b0) * x = [((a + b) * x1),((a + b) * x2)] by A1, Def2 .= (prod_ADD (G,F)) . ([(a * x1),(a * x2)],[(b * x1),(b * x2)]) by A2, Def1 .= (prod_ADD (G,F)) . (((prod_MLT (G,F)) . (a,[x1,x2])),[(b * x1),(b * x2)]) by Def2 .= (a0 * x) + (b0 * x) by A1, Def2 ; ::_thesis: verum 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 let a0, b0 be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of [:G,F:] holds (a0 * b0) * b1 = a0 * (b0 * b1) let x be VECTOR of [:G,F:]; ::_thesis: (a0 * b0) * x = a0 * (b0 * x) reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def_1; consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; A2: ( (a * b) * x1 = a0 * (b0 * x1) & (a * b) * x2 = a0 * (b0 * x2) ) by RLVECT_1:def_7; thus (a0 * b0) * x = [((a * b) * x1),((a * b) * x2)] by A1, Def2 .= (prod_MLT (G,F)) . (a,[(b * x1),(b * x2)]) by A2, Def2 .= a0 * (b0 * x) by A1, Def2 ; ::_thesis: verum 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 let x be VECTOR of [:G,F:]; :: according to RLVECT_1:def_8 ::_thesis: 1 * x = x consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; ( 1 * x1 = x1 & 1 * x2 = x2 ) by RLVECT_1:def_8; hence 1 * x = x by A1, Def2; ::_thesis: verum 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 let S be set ; :: according to PRVECT_2:def_3 ::_thesis: ( not S in rng <*G*> or S is RLSStruct ) assume S in rng <*G*> ; ::_thesis: S is RLSStruct then consider i being set such that A1: ( i in dom <*G*> & <*G*> . i = S ) by FUNCT_1:def_3; reconsider i = i as Element of NAT by A1; dom <*G*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8; then i = 1 by A1, TARSKI:def_1; hence S is RealLinearSpace by A1, FINSEQ_1:40; ::_thesis: verum 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 let S be set ; :: according to PRVECT_2:def_3 ::_thesis: ( not S in rng <*G,F*> or S is RLSStruct ) assume S in rng <*G,F*> ; ::_thesis: S is RLSStruct then consider i being set such that A1: ( i in dom <*G,F*> & <*G,F*> . i = S ) by FUNCT_1:def_3; dom <*G,F*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then ( i = 1 or i = 2 ) by A1, TARSKI:def_2; hence S is RealLinearSpace by A1, FINSEQ_1:44; ::_thesis: verum 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 let X be RealLinearSpace; ::_thesis: 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*>) ) set CarrX = the carrier of X; consider I being Function of the carrier of X,(product <* the carrier of X*>) such that A1: ( I is one-to-one & I is onto & ( for x being set st x in the carrier of X holds I . x = <*x*> ) ) by Th4; len (carr <*X*>) = len <*X*> by PRVECT_2:def_4; then A2: len (carr <*X*>) = 1 by FINSEQ_1:40; A3: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8; A4: <*X*> . 1 = X by FINSEQ_1:def_8; 1 in {1} by TARSKI:def_1; then (carr <*X*>) . 1 = the carrier of X by A3, A4, PRVECT_2:def_4; then A5: carr <*X*> = <* the carrier of X*> by A2, FINSEQ_1:40; then reconsider I = I as Function of X,(product <*X*>) ; A6: for x being Point of X holds I . x = <*x*> by A1; A7: for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) proof let v, w be Point of X; ::_thesis: I . (v + w) = (I . v) + (I . w) A8: ( I . v = <*v*> & I . w = <*w*> & I . (v + w) = <*(v + w)*> ) by A1; A9: ( <*v*> . 1 = v & <*w*> . 1 = w ) by FINSEQ_1:40; reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X*>) ; 1 in {1} by TARSKI:def_1; then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def_3; A10: (addop <*X*>) . j1 = the addF of (<*X*> . j1) by PRVECT_2:def_5; A11: ([:(addop <*X*>):] . (Iv,Iw)) . j1 = ((addop <*X*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def_8 .= v + w by A10, A8, A9, FINSEQ_1:40 ; consider Ivw being Function such that A12: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being set st i in dom (carr <*X*>) holds Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def_5; A13: dom Ivw = Seg 1 by A2, A12, FINSEQ_1:def_3; then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def_2; len Ivw = 1 by A13, FINSEQ_1:def_3; hence I . (v + w) = (I . v) + (I . w) by A8, A12, A11, FINSEQ_1:40; ::_thesis: verum end; A14: for v being Point of X for r being Element of REAL holds I . (r * v) = r * (I . v) proof let v be Point of X; ::_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) A15: ( I . v = <*v*> & I . (r * v) = <*(r * v)*> ) by A1; A16: <*v*> . 1 = v by FINSEQ_1:40; 1 in {1} by TARSKI:def_1; then reconsider j1 = 1 as Element of dom (carr <*X*>) by A2, FINSEQ_1:2, FINSEQ_1:def_3; A17: (multop <*X*>) . j1 = the Mult of (<*X*> . j1) by PRVECT_2:def_8; reconsider Iv = I . v as Element of product (carr <*X*>) ; A18: ([:(multop <*X*>):] . (r,Iv)) . j1 = ((multop <*X*>) . j1) . (r,(Iv . j1)) by PRVECT_2:def_2 .= r * v by A17, A15, A16, FINSEQ_1:40 ; consider Ivw being Function such that A19: ( r * (I . v) = Ivw & dom Ivw = dom (carr <*X*>) & ( for i being set st i in dom (carr <*X*>) holds Ivw . i in (carr <*X*>) . i ) ) by CARD_3:def_5; A20: dom Ivw = Seg 1 by A2, A19, FINSEQ_1:def_3; then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def_2; len Ivw = 1 by A20, FINSEQ_1:def_3; hence I . (r * v) = r * (I . v) by A15, A19, A18, FINSEQ_1:40; ::_thesis: verum end; I . (0. X) = I . ((0. X) + (0. X)) by RLVECT_1:def_4 .= (I . (0. X)) + (I . (0. X)) by A7 ; then (I . (0. X)) - (I . (0. X)) = (I . (0. X)) + ((I . (0. X)) - (I . (0. X))) by RLVECT_1:28 .= (I . (0. X)) + (0. (product <*X*>)) by RLVECT_1:15 .= I . (0. X) by RLVECT_1:def_4 ; then 0. (product <*X*>) = I . (0. X) by RLVECT_1:15; hence 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*>) ) by A1, A6, A5, A7, A14; ::_thesis: verum end; registration let G, F be non empty RealLinearSpace-yielding FinSequence; clusterG ^ F -> RealLinearSpace-yielding ; correctness coherence G ^ F is RealLinearSpace-yielding ; proof let S be set ; :: according to PRVECT_2:def_3 ::_thesis: ( not S in rng (G ^ F) or S is RLSStruct ) assume S in rng (G ^ F) ; ::_thesis: S is RLSStruct then consider i being set such that A1: ( i in dom (G ^ F) & (G ^ F) . i = S ) by FUNCT_1:def_3; reconsider i = i as Element of NAT by A1; percases ( i in dom G or ex n being Nat st ( n in dom F & i = (len G) + n ) ) by A1, FINSEQ_1:25; supposeA2: i in dom G ; ::_thesis: S is RLSStruct then A3: (G ^ F) . i = G . i by FINSEQ_1:def_7; G . i in rng G by A2, FUNCT_1:3; hence S is RealLinearSpace by A3, A1, PRVECT_2:def_3; ::_thesis: verum end; suppose ex n being Nat st ( n in dom F & i = (len G) + n ) ; ::_thesis: S is RLSStruct then consider n being Nat such that A4: ( n in dom F & i = (len G) + n ) ; A5: (G ^ F) . i = F . n by A4, FINSEQ_1:def_7; F . n in rng F by A4, FUNCT_1:3; hence S is RealLinearSpace by A5, A1, PRVECT_2:def_3; ::_thesis: verum end; end; 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 let X, Y be RealLinearSpace; ::_thesis: 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*>) ) set CarrX = the carrier of X; set CarrY = the carrier of Y; consider I being Function of [: the carrier of X, the carrier of Y:],(product <* the carrier of X, the carrier of Y*>) such that A1: ( I is one-to-one & I is onto & ( for x, y being set st x in the carrier of X & y in the carrier of Y holds I . (x,y) = <*x,y*> ) ) by Th5; len (carr <*X,Y*>) = len <*X,Y*> by PRVECT_2:def_4; then A2: len (carr <*X,Y*>) = 2 by FINSEQ_1:44; then A3: dom (carr <*X,Y*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; len <*X,Y*> = 2 by FINSEQ_1:44; then A4: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; A5: ( <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:44; ( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def_2; then ( (carr <*X,Y*>) . 1 = the carrier of X & (carr <*X,Y*>) . 2 = the carrier of Y ) by A4, A5, PRVECT_2:def_4; then A6: carr <*X,Y*> = <* the carrier of X, the carrier of Y*> by A2, FINSEQ_1:44; then reconsider I = I as Function of [:X,Y:],(product <*X,Y*>) ; A7: for x being Point of X for y being Point of Y holds I . (x,y) = <*x,y*> by A1; A8: for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) proof let v, w be Point of [:X,Y:]; ::_thesis: I . (v + w) = (I . v) + (I . w) consider x1 being Point of X, y1 being Point of Y such that A9: v = [x1,y1] by Lm1; consider x2 being Point of X, y2 being Point of Y such that A10: w = [x2,y2] by Lm1; ( I . v = I . (x1,y1) & I . w = I . (x2,y2) ) by A9, A10; then A11: ( I . v = <*x1,y1*> & I . w = <*x2,y2*> ) by A1; A12: I . (v + w) = I . ((x1 + x2),(y1 + y2)) by A9, A10, Def1 .= <*(x1 + x2),(y1 + y2)*> by A1 ; A13: ( <*x1,y1*> . 1 = x1 & <*x2,y2*> . 1 = x2 & <*x1,y1*> . 2 = y1 & <*x2,y2*> . 2 = y2 ) by FINSEQ_1:44; reconsider Iv = I . v, Iw = I . w as Element of product (carr <*X,Y*>) ; reconsider j1 = 1, j2 = 2 as Element of dom (carr <*X,Y*>) by A3, TARSKI:def_2; A14: (addop <*X,Y*>) . j1 = the addF of (<*X,Y*> . j1) by PRVECT_2:def_5; A15: ([:(addop <*X,Y*>):] . (Iv,Iw)) . j1 = ((addop <*X,Y*>) . j1) . ((Iv . j1),(Iw . j1)) by PRVECT_1:def_8 .= x1 + x2 by A14, A11, A13, FINSEQ_1:44 ; A16: (addop <*X,Y*>) . j2 = the addF of (<*X,Y*> . j2) by PRVECT_2:def_5; A17: ([:(addop <*X,Y*>):] . (Iv,Iw)) . j2 = ((addop <*X,Y*>) . j2) . ((Iv . j2),(Iw . j2)) by PRVECT_1:def_8 .= y1 + y2 by A16, A11, A13, FINSEQ_1:44 ; consider Ivw being Function such that A18: ( (I . v) + (I . w) = Ivw & dom Ivw = dom (carr <*X,Y*>) & ( for i being set st i in dom (carr <*X,Y*>) holds Ivw . i in (carr <*X,Y*>) . i ) ) by CARD_3:def_5; A19: dom Ivw = Seg 2 by A2, A18, FINSEQ_1:def_3; then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def_2; len Ivw = 2 by A19, FINSEQ_1:def_3; hence I . (v + w) = (I . v) + (I . w) by A12, A18, A15, A17, FINSEQ_1:44; ::_thesis: verum end; A20: for v being Point of [:X,Y:] for r being Element of REAL holds I . (r * v) = r * (I . v) proof let v be Point of [:X,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) consider x1 being Point of X, y1 being Point of Y such that A21: v = [x1,y1] by Lm1; A22: I . v = I . (x1,y1) by A21 .= <*x1,y1*> by A1 ; A23: I . (r * v) = I . ((r * x1),(r * y1)) by A21, Def2 .= <*(r * x1),(r * y1)*> by A1 ; A24: ( <*x1,y1*> . 1 = x1 & <*x1,y1*> . 2 = y1 ) by FINSEQ_1:44; reconsider j1 = 1, j2 = 2 as Element of dom (carr <*X,Y*>) by A3, TARSKI:def_2; A25: ( (multop <*X,Y*>) . j1 = the Mult of (<*X,Y*> . j1) & (multop <*X,Y*>) . j2 = the Mult of (<*X,Y*> . j2) ) by PRVECT_2:def_8; reconsider Iv = I . v as Element of product (carr <*X,Y*>) ; ( ([:(multop <*X,Y*>):] . (r,Iv)) . j1 = ((multop <*X,Y*>) . j1) . (r,(Iv . j1)) & ([:(multop <*X,Y*>):] . (r,Iv)) . j2 = ((multop <*X,Y*>) . j2) . (r,(Iv . j2)) ) by PRVECT_2:def_2; then A26: ( ([:(multop <*X,Y*>):] . (r,Iv)) . j1 = r * x1 & ([:(multop <*X,Y*>):] . (r,Iv)) . j2 = r * y1 ) by A25, A22, A24, FINSEQ_1:44; consider Ivw being Function such that A27: ( r * (I . v) = Ivw & dom Ivw = dom (carr <*X,Y*>) & ( for i being set st i in dom (carr <*X,Y*>) holds Ivw . i in (carr <*X,Y*>) . i ) ) by CARD_3:def_5; A28: dom Ivw = Seg 2 by A2, A27, FINSEQ_1:def_3; then reconsider Ivw = Ivw as FinSequence by FINSEQ_1:def_2; len Ivw = 2 by A28, FINSEQ_1:def_3; hence I . (r * v) = r * (I . v) by A23, A27, A26, FINSEQ_1:44; ::_thesis: verum end; I . (0. [:X,Y:]) = I . ((0. [:X,Y:]) + (0. [:X,Y:])) by RLVECT_1:def_4 .= (I . (0. [:X,Y:])) + (I . (0. [:X,Y:])) by A8 ; then (I . (0. [:X,Y:])) - (I . (0. [:X,Y:])) = (I . (0. [:X,Y:])) + ((I . (0. [:X,Y:])) - (I . (0. [:X,Y:]))) by RLVECT_1:28 .= (I . (0. [:X,Y:])) + (0. (product <*X,Y*>)) by RLVECT_1:15 .= I . (0. [:X,Y:]) by RLVECT_1:def_4 ; then 0. (product <*X,Y*>) = I . (0. [:X,Y:]) by RLVECT_1:15; hence 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*>) ) by A7, A8, A20, A1, A6; ::_thesis: verum end; Lm2: for X being non empty non-empty FinSequence for x being set st x in product X holds x is FinSequence proof let X be non empty non-empty FinSequence; ::_thesis: for x being set st x in product X holds x is FinSequence let x be set ; ::_thesis: ( x in product X implies x is FinSequence ) assume x in product X ; ::_thesis: x is FinSequence then consider g being Function such that A1: ( x = g & dom g = dom X & ( for i being set st i in dom X holds g . i in X . i ) ) by CARD_3:def_5; dom g = Seg (len X) by A1, FINSEQ_1:def_3; hence x is FinSequence by A1, FINSEQ_1:def_2; ::_thesis: verum 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 let X, Y be RealLinearSpace-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)) ) reconsider CX = carr X, CY = carr Y as non empty non-empty FinSequence ; A1: ( len CX = len X & len CY = len Y & len (carr (X ^ Y)) = len (X ^ Y) ) by PRVECT_2:def_4; consider I being Function of [:(product CX),(product CY):],(product (CX ^ CY)) such that A2: ( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product CX & y in product CY holds I . (x,y) = x ^ y ) ) by Th6; set PX = product X; set PY = product Y; ( len (carr (X ^ Y)) = (len X) + (len Y) & len (CX ^ CY) = (len X) + (len Y) ) by A1, FINSEQ_1:22; then A3: dom (carr (X ^ Y)) = dom (CX ^ CY) by FINSEQ_3:29; A4: for k being Nat st k in dom (carr (X ^ Y)) holds (carr (X ^ Y)) . k = (CX ^ CY) . k proof let k be Nat; ::_thesis: ( k in dom (carr (X ^ Y)) implies (carr (X ^ Y)) . k = (CX ^ CY) . k ) assume A5: k in dom (carr (X ^ Y)) ; ::_thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k then reconsider k1 = k as Element of dom (X ^ Y) by A1, FINSEQ_3:29; A6: (carr (X ^ Y)) . k = the carrier of ((X ^ Y) . k1) by PRVECT_2:def_4; A7: k in dom (X ^ Y) by A1, A5, FINSEQ_3:29; percases ( k in dom X or ex n being Nat st ( n in dom Y & k = (len X) + n ) ) by A7, FINSEQ_1:25; supposeA8: k in dom X ; ::_thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k then A9: k in dom CX by A1, FINSEQ_3:29; reconsider k2 = k1 as Element of dom X by A8; thus (carr (X ^ Y)) . k = the carrier of (X . k2) by A6, FINSEQ_1:def_7 .= CX . k by PRVECT_2:def_4 .= (CX ^ CY) . k by A9, FINSEQ_1:def_7 ; ::_thesis: verum end; suppose ex n being Nat st ( n in dom Y & k = (len X) + n ) ; ::_thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k then consider n being Nat such that A10: ( n in dom Y & k = (len X) + n ) ; A11: n in dom CY by A1, A10, FINSEQ_3:29; reconsider n1 = n as Element of dom Y by A10; thus (carr (X ^ Y)) . k = the carrier of (Y . n1) by A6, A10, FINSEQ_1:def_7 .= CY . n by PRVECT_2:def_4 .= (CX ^ CY) . k by A11, A10, A1, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; then A12: carr (X ^ Y) = CX ^ CY by A3, FINSEQ_1:13; reconsider I = I as Function of [:(product X),(product Y):],(product (X ^ Y)) by A3, A4, FINSEQ_1:13; A13: 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 ) proof let x be Point of (product X); ::_thesis: for y being Point of (product Y) ex x1, y1 being FinSequence st ( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) let y be Point of (product Y); ::_thesis: ex x1, y1 being FinSequence st ( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) reconsider x1 = x, y1 = y as FinSequence by Lm2; I . (x,y) = x1 ^ y1 by A2; hence ex x1, y1 being FinSequence st ( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ; ::_thesis: verum end; A14: for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) proof let v, w be Point of [:(product X),(product Y):]; ::_thesis: I . (v + w) = (I . v) + (I . w) consider x1 being Point of (product X), y1 being Point of (product Y) such that A15: v = [x1,y1] by Lm1; consider x2 being Point of (product X), y2 being Point of (product Y) such that A16: w = [x2,y2] by Lm1; reconsider xx1 = x1, xx2 = x2 as FinSequence by Lm2; reconsider yy1 = y1, yy2 = y2 as FinSequence by Lm2; reconsider xx12 = x1 + x2, yy12 = y1 + y2 as FinSequence by Lm2; A17: ( dom xx1 = dom CX & dom xx2 = dom CX & dom xx12 = dom CX & dom yy1 = dom CY & dom yy2 = dom CY & dom yy12 = dom CY ) by CARD_3:9; ( I . v = I . (x1,y1) & I . w = I . (x2,y2) ) by A15, A16; then A18: ( I . v = xx1 ^ yy1 & I . w = xx2 ^ yy2 ) by A2; I . (v + w) = I . ((x1 + x2),(y1 + y2)) by A15, A16, Def1; then A19: I . (v + w) = xx12 ^ yy12 by A2; then A20: dom (xx12 ^ yy12) = dom (carr (X ^ Y)) by CARD_3:9; reconsider Iv = I . v, Iw = I . w as Element of product (carr (X ^ Y)) ; reconsider Ivw = (I . v) + (I . w) as FinSequence by Lm2; A21: dom Ivw = dom (carr (X ^ Y)) by CARD_3:9; for j0 being Nat st j0 in dom Ivw holds Ivw . j0 = (xx12 ^ yy12) . j0 proof let j0 be Nat; ::_thesis: ( j0 in dom Ivw implies Ivw . j0 = (xx12 ^ yy12) . j0 ) assume j0 in dom Ivw ; ::_thesis: Ivw . j0 = (xx12 ^ yy12) . j0 then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:9; A22: Ivw . j0 = ((addop (X ^ Y)) . j) . ((Iv . j),(Iw . j)) by PRVECT_1:def_8 .= the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) by PRVECT_2:def_5 ; percases ( j0 in dom CX or ex n being Nat st ( n in dom CY & j0 = (len CX) + n ) ) by A22, A3, FINSEQ_1:25; supposeA23: j0 in dom CX ; ::_thesis: Ivw . j0 = (xx12 ^ yy12) . j0 then j0 in dom X by A1, FINSEQ_3:29; then A24: (X ^ Y) . j = X . j0 by FINSEQ_1:def_7; A25: ( Iv . j = xx1 . j & Iw . j = xx2 . j ) by A23, A17, A18, FINSEQ_1:def_7; A26: (xx12 ^ yy12) . j0 = xx12 . j0 by A23, A17, FINSEQ_1:def_7; reconsider j1 = j0 as Element of dom (carr X) by A23; the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop X) . j1) . ((xx1 . j1),(xx2 . j1)) by A24, A25, PRVECT_2:def_5 .= (xx12 ^ yy12) . j0 by A26, PRVECT_1:def_8 ; hence Ivw . j0 = (xx12 ^ yy12) . j0 by A22; ::_thesis: verum end; suppose ex n being Nat st ( n in dom CY & j0 = (len CX) + n ) ; ::_thesis: Ivw . j0 = (xx12 ^ yy12) . j0 then consider n being Nat such that A27: ( n in dom CY & j0 = (len CX) + n ) ; A28: ( len CX = len xx1 & len CX = len xx2 & len CX = len xx12 ) by A17, FINSEQ_3:29; n in dom Y by A1, A27, FINSEQ_3:29; then A29: (X ^ Y) . j = Y . n by A27, A1, FINSEQ_1:def_7; A30: ( Iv . j = yy1 . n & Iw . j = yy2 . n ) by A17, A18, A27, A28, FINSEQ_1:def_7; A31: (xx12 ^ yy12) . j0 = yy12 . n by A27, A28, A17, FINSEQ_1:def_7; reconsider j1 = n as Element of dom (carr Y) by A27; the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop Y) . j1) . ((yy1 . j1),(yy2 . j1)) by A29, A30, PRVECT_2:def_5 .= (xx12 ^ yy12) . j0 by A31, PRVECT_1:def_8 ; hence Ivw . j0 = (xx12 ^ yy12) . j0 by A22; ::_thesis: verum end; end; end; hence I . (v + w) = (I . v) + (I . w) by A19, A20, A21, FINSEQ_1:13; ::_thesis: verum end; A32: for v being Point of [:(product X),(product Y):] for r being Element of REAL holds I . (r * v) = r * (I . 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) consider x1 being Point of (product X), y1 being Point of (product Y) such that A33: v = [x1,y1] by Lm1; reconsider xx1 = x1, yy1 = y1 as FinSequence by Lm2; reconsider rxx1 = r * x1, ryy1 = r * y1 as FinSequence by Lm2; A34: ( dom xx1 = dom CX & dom yy1 = dom CY & dom rxx1 = dom CX & dom ryy1 = dom CY ) by CARD_3:9; A35: I . v = I . (x1,y1) by A33 .= xx1 ^ yy1 by A2 ; A36: I . (r * v) = I . ((r * x1),(r * y1)) by A33, Def2 .= rxx1 ^ ryy1 by A2 ; reconsider Iv = I . v as Element of product (carr (X ^ Y)) ; reconsider rIv = r * (I . v) as FinSequence by Lm2; A37: dom rIv = dom (carr (X ^ Y)) by CARD_3:9; A38: dom (rxx1 ^ ryy1) = dom (carr (X ^ Y)) by A36, CARD_3:9; for j0 being Nat st j0 in dom rIv holds rIv . j0 = (rxx1 ^ ryy1) . j0 proof let j0 be Nat; ::_thesis: ( j0 in dom rIv implies rIv . j0 = (rxx1 ^ ryy1) . j0 ) assume A39: j0 in dom rIv ; ::_thesis: rIv . j0 = (rxx1 ^ ryy1) . j0 then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:9; A40: rIv . j0 = ((multop (X ^ Y)) . j) . (r,(Iv . j)) by PRVECT_2:def_2 .= the Mult of ((X ^ Y) . j) . (r,(Iv . j)) by PRVECT_2:def_8 ; percases ( j0 in dom CX or ex n being Nat st ( n in dom CY & j0 = (len CX) + n ) ) by A3, A39, A37, FINSEQ_1:25; supposeA41: j0 in dom CX ; ::_thesis: rIv . j0 = (rxx1 ^ ryy1) . j0 then j0 in dom X by A1, FINSEQ_3:29; then A42: (X ^ Y) . j = X . j0 by FINSEQ_1:def_7; A43: Iv . j = xx1 . j by A41, A34, A35, FINSEQ_1:def_7; A44: (rxx1 ^ ryy1) . j0 = rxx1 . j0 by A41, A34, FINSEQ_1:def_7; reconsider j1 = j0 as Element of dom (carr X) by A41; the Mult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop X) . j1) . (r,(xx1 . j1)) by A42, A43, PRVECT_2:def_8 .= (rxx1 ^ ryy1) . j0 by A44, PRVECT_2:def_2 ; hence rIv . j0 = (rxx1 ^ ryy1) . j0 by A40; ::_thesis: verum end; suppose ex n being Nat st ( n in dom CY & j0 = (len CX) + n ) ; ::_thesis: rIv . j0 = (rxx1 ^ ryy1) . j0 then consider n being Nat such that A45: ( n in dom CY & j0 = (len CX) + n ) ; A46: ( len CX = len xx1 & len CX = len rxx1 ) by A34, FINSEQ_3:29; n in dom Y by A45, A1, FINSEQ_3:29; then A47: (X ^ Y) . j = Y . n by A45, A1, FINSEQ_1:def_7; A48: Iv . j = yy1 . n by A35, A45, A34, A46, FINSEQ_1:def_7; A49: (rxx1 ^ ryy1) . j0 = ryy1 . n by A45, A46, A34, FINSEQ_1:def_7; reconsider j1 = n as Element of dom (carr Y) by A45; the Mult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop Y) . j1) . (r,(yy1 . j1)) by A47, A48, PRVECT_2:def_8 .= (rxx1 ^ ryy1) . j0 by A49, PRVECT_2:def_2 ; hence rIv . j0 = (rxx1 ^ ryy1) . j0 by A40; ::_thesis: verum end; end; end; hence I . (r * v) = r * (I . v) by A36, A38, A37, FINSEQ_1:13; ::_thesis: verum end; I . (0. [:(product X),(product Y):]) = I . ((0. [:(product X),(product Y):]) + (0. [:(product X),(product Y):])) by RLVECT_1:def_4 .= (I . (0. [:(product X),(product Y):])) + (I . (0. [:(product X),(product Y):])) by A14 ; then (I . (0. [:(product X),(product Y):])) - (I . (0. [:(product X),(product Y):])) = (I . (0. [:(product X),(product Y):])) + ((I . (0. [:(product X),(product Y):])) - (I . (0. [:(product X),(product Y):]))) by RLVECT_1:28 .= (I . (0. [:(product X),(product Y):])) + (0. (product (X ^ Y))) by RLVECT_1:15 .= I . (0. [:(product X),(product Y):]) by RLVECT_1:def_4 ; then 0. (product (X ^ Y)) = I . (0. [:(product X),(product Y):]) by RLVECT_1:15; hence 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)) ) by A13, A14, A32, A2, A12; ::_thesis: verum 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 let G, F be RealLinearSpace; ::_thesis: ( ( 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)*> ) ) consider I being Function of [:G,F:],(product <*G,F*>) such that A1: ( I is one-to-one & I is onto & ( for x being Point of G for y being Point of F holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:G,F:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:G,F:] for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*G,F*>) = I . (0. [:G,F:]) ) by Th12; thus A2: 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*> ) ::_thesis: ( ( 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 let y be set ; ::_thesis: ( y is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> ) hereby ::_thesis: ( ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> implies y is Point of (product <*G,F*>) ) assume y is Point of (product <*G,F*>) ; ::_thesis: ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> then y in the carrier of (product <*G,F*>) ; then y in rng I by A1, FUNCT_2:def_3; then consider x being Element of the carrier of [:G,F:] such that A3: y = I . x by FUNCT_2:113; consider x1 being Point of G, x2 being Point of F such that A4: x = [x1,x2] by Lm1; take x1 = x1; ::_thesis: ex x2 being Point of F st y = <*x1,x2*> take x2 = x2; ::_thesis: y = <*x1,x2*> I . (x1,x2) = <*x1,x2*> by A1; hence y = <*x1,x2*> by A3, A4; ::_thesis: verum end; now__::_thesis:_(_ex_x1_being_Point_of_G_ex_x2_being_Point_of_F_st_y_=_<*x1,x2*>_implies_y_is_Point_of_(product_<*G,F*>)_) assume ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> ; ::_thesis: y is Point of (product <*G,F*>) then consider x1 being Point of G, x2 being Point of F such that A5: y = <*x1,x2*> ; A6: I . [x1,x2] in rng I by FUNCT_2:112; I . (x1,x2) = <*x1,x2*> by A1; hence y is Point of (product <*G,F*>) by A5, A6; ::_thesis: verum end; hence ( ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> implies y is Point of (product <*G,F*>) ) ; ::_thesis: verum end; thus A7: 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)*> ::_thesis: ( 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 let x, y be Point of (product <*G,F*>); ::_thesis: 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)*> let x1, y1 be Point of G; ::_thesis: for x2, y2 being Point of F st x = <*x1,x2*> & y = <*y1,y2*> holds x + y = <*(x1 + y1),(x2 + y2)*> let x2, y2 be Point of F; ::_thesis: ( x = <*x1,x2*> & y = <*y1,y2*> implies x + y = <*(x1 + y1),(x2 + y2)*> ) assume A8: ( x = <*x1,x2*> & y = <*y1,y2*> ) ; ::_thesis: x + y = <*(x1 + y1),(x2 + y2)*> reconsider z = [x1,x2], w = [y1,y2] as Point of [:G,F:] ; A9: z + w = [(x1 + y1),(x2 + y2)] by Def1; ( I . ((x1 + y1),(x2 + y2)) = <*(x1 + y1),(x2 + y2)*> & I . (x1,x2) = <*x1,x2*> & I . (y1,y2) = <*y1,y2*> ) by A1; hence <*(x1 + y1),(x2 + y2)*> = x + y by A1, A9, A8; ::_thesis: verum end; thus A10: 0. (product <*G,F*>) = <*(0. G),(0. F)*> ::_thesis: ( ( 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 I . ((0. G),(0. F)) = <*(0. G),(0. F)*> by A1; hence 0. (product <*G,F*>) = <*(0. G),(0. F)*> by A1; ::_thesis: verum end; thus 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)*> ::_thesis: 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 let x be Point of (product <*G,F*>); ::_thesis: for x1 being Point of G for x2 being Point of F st x = <*x1,x2*> holds - x = <*(- x1),(- x2)*> let x1 be Point of G; ::_thesis: for x2 being Point of F st x = <*x1,x2*> holds - x = <*(- x1),(- x2)*> let x2 be Point of F; ::_thesis: ( x = <*x1,x2*> implies - x = <*(- x1),(- x2)*> ) assume A11: x = <*x1,x2*> ; ::_thesis: - x = <*(- x1),(- x2)*> reconsider y = <*(- x1),(- x2)*> as Point of (product <*G,F*>) by A2; x + y = <*(x1 + (- x1)),(x2 + (- x2))*> by A7, A11 .= <*(0. G),(x2 + (- x2))*> by RLVECT_1:def_10 .= 0. (product <*G,F*>) by A10, RLVECT_1:def_10 ; hence - x = <*(- x1),(- x2)*> by RLVECT_1:def_10; ::_thesis: verum end; thus 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)*> ::_thesis: verum proof let x be Point of (product <*G,F*>); ::_thesis: 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)*> let x1 be Point of G; ::_thesis: for x2 being Point of F for a being real number st x = <*x1,x2*> holds a * x = <*(a * x1),(a * x2)*> let x2 be Point of F; ::_thesis: for a being real number st x = <*x1,x2*> holds a * x = <*(a * x1),(a * x2)*> let a be real number ; ::_thesis: ( x = <*x1,x2*> implies a * x = <*(a * x1),(a * x2)*> ) assume A12: x = <*x1,x2*> ; ::_thesis: a * x = <*(a * x1),(a * x2)*> reconsider a0 = a as Element of REAL by XREAL_0:def_1; reconsider y = [x1,x2] as Point of [:G,F:] ; A13: <*x1,x2*> = I . (x1,x2) by A1; I . (a * y) = I . ((a0 * x1),(a0 * x2)) by Th9 .= <*(a0 * x1),(a0 * x2)*> by A1 ; hence a * x = <*(a * x1),(a * x2)*> by A1, A12, A13; ::_thesis: verum end; end; 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.| ) proof defpred S1[ set , set , set ] means ex g being Point of G ex f being Point of F ex v being Element of REAL 2 st ( $1 = g & $2 = f & v = <*||.g.||,||.f.||*> & $3 = |.v.| ); A1: for x, y being set st x in the carrier of G & y in the carrier of F holds ex z being set st ( z in REAL & S1[x,y,z] ) proof let x, y be set ; ::_thesis: ( x in the carrier of G & y in the carrier of F implies ex z being set st ( z in REAL & S1[x,y,z] ) ) assume A2: ( x in the carrier of G & y in the carrier of F ) ; ::_thesis: ex z being set st ( z in REAL & S1[x,y,z] ) then reconsider g = x as Point of G ; reconsider f = y as Point of F by A2; reconsider v = <*||.g.||,||.f.||*> as Element of REAL 2 by FINSEQ_2:101; |.v.| in REAL ; hence ex z being set st ( z in REAL & S1[x,y,z] ) ; ::_thesis: verum end; consider NORMGF being Function of [: the carrier of G, the carrier of F:],REAL such that A3: for x, y being set st x in the carrier of G & y in the carrier of F holds S1[x,y,NORMGF . (x,y)] from BINOP_1:sch_1(A1); now__::_thesis:_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.|_) let g be Point of G; ::_thesis: for f being Point of F ex v being Element of REAL 2 st ( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| ) let f be Point of F; ::_thesis: ex v being Element of REAL 2 st ( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| ) ex gg being Point of G ex ff being Point of F ex v being Element of REAL 2 st ( g = gg & f = ff & v = <*||.gg.||,||.ff.||*> & NORMGF . (g,f) = |.v.| ) by A3; hence ex v being Element of REAL 2 st ( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| ) ; ::_thesis: verum end; hence 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.| ) ; ::_thesis: verum 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 let H1, H2 be Function of [: the carrier of G, the carrier of F:],REAL; ::_thesis: ( ( for g being Point of G for f being Point of F ex v being Element of REAL 2 st ( v = <*||.g.||,||.f.||*> & H1 . (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.||*> & H2 . (g,f) = |.v.| ) ) implies H1 = H2 ) assume A4: for g being Point of G for f being Point of F ex v being Element of REAL 2 st ( v = <*||.g.||,||.f.||*> & H1 . (g,f) = |.v.| ) ; ::_thesis: ( ex g being Point of G ex f being Point of F st for v being Element of REAL 2 holds ( not v = <*||.g.||,||.f.||*> or not H2 . (g,f) = |.v.| ) or H1 = H2 ) assume A5: for g being Point of G for f being Point of F ex v being Element of REAL 2 st ( v = <*||.g.||,||.f.||*> & H2 . (g,f) = |.v.| ) ; ::_thesis: H1 = H2 now__::_thesis:_for_g_being_Element_of_the_carrier_of_G for_f_being_Element_of_the_carrier_of_F_holds_H1_._(g,f)_=_H2_._(g,f) let g be Element of the carrier of G; ::_thesis: for f being Element of the carrier of F holds H1 . (g,f) = H2 . (g,f) let f be Element of the carrier of F; ::_thesis: H1 . (g,f) = H2 . (g,f) A6: ex v1 being Element of REAL 2 st ( v1 = <*||.g.||,||.f.||*> & H1 . (g,f) = |.v1.| ) by A4; ex v2 being Element of REAL 2 st ( v2 = <*||.g.||,||.f.||*> & H2 . (g,f) = |.v2.| ) by A5; hence H1 . (g,f) = H2 . (g,f) by A6; ::_thesis: verum end; hence H1 = H2 by BINOP_1:2; ::_thesis: verum 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)) #); 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 now__::_thesis:_for_x_being_Point_of_[:G,F:]_st_x_=_0._[:G,F:]_holds_ ||.x.||_=_0 let x be Point of [:G,F:]; ::_thesis: ( x = 0. [:G,F:] implies ||.x.|| = 0 ) consider x1 being Point of G, x2 being Point of F such that A1: x = [x1,x2] by Lm1; consider v being Element of REAL 2 such that A2: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6; assume x = 0. [:G,F:] ; ::_thesis: ||.x.|| = 0 then ( x1 = 0. G & x2 = 0. F ) by A1, XTUPLE_0:1; then ( ||.x1.|| = 0 & ||.x2.|| = 0 ) ; then v = 0* 2 by A2, FINSEQ_2:61; hence ||.x.|| = 0 by A2, A1, EUCLID:7; ::_thesis: verum end; then ||.(0. [:G,F:]).|| = 0 ; hence [:G,F:] is reflexive by NORMSP_0:def_6; ::_thesis: ( [:G,F:] is discerning & [:G,F:] is RealNormSpace-like ) now__::_thesis:_for_x_being_Point_of_[:G,F:]_st_||.x.||_=_0_holds_ x_=_0._[:G,F:] let x be Point of [:G,F:]; ::_thesis: ( ||.x.|| = 0 implies x = 0. [:G,F:] ) consider x1 being Point of G, x2 being Point of F such that A3: x = [x1,x2] by Lm1; consider v being Element of REAL 2 such that A4: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6; assume ||.x.|| = 0 ; ::_thesis: x = 0. [:G,F:] then v = 0* 2 by A4, A3, EUCLID:8; then A5: v = <*0,0*> by FINSEQ_2:61; ( ||.x1.|| = v . 1 & ||.x2.|| = v . 2 ) by A4, FINSEQ_1:44; then ( ||.x1.|| = 0 & ||.x2.|| = 0 ) by A5, FINSEQ_1:44; then ( x1 = 0. G & x2 = 0. F ) by NORMSP_0:def_5; hence x = 0. [:G,F:] by A3; ::_thesis: verum end; hence [:G,F:] is discerning by NORMSP_0:def_5; ::_thesis: [:G,F:] is RealNormSpace-like now__::_thesis:_for_x,_y_being_Point_of_[:G,F:] for_a_being_Real_holds_ (_||.(a_*_x).||_=_(abs_a)_*_||.x.||_&_||.(x_+_y).||_<=_||.x.||_+_||.y.||_) let x, y be Point of [:G,F:]; ::_thesis: for a being Real holds ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) let a be Real; ::_thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) consider x1 being Point of G, x2 being Point of F such that A6: x = [x1,x2] by Lm1; consider y1 being Point of G, y2 being Point of F such that A7: y = [y1,y2] by Lm1; consider v being Element of REAL 2 such that A8: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by Def6; consider z being Element of REAL 2 such that A9: ( z = <*||.y1.||,||.y2.||*> & (prod_NORM (G,F)) . (y1,y2) = |.z.| ) by Def6; thus ||.(a * x).|| = (abs a) * ||.x.|| ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.|| proof consider w being Element of REAL 2 such that A10: ( w = <*||.(a * x1).||,||.(a * x2).||*> & (prod_NORM (G,F)) . ((a * x1),(a * x2)) = |.w.| ) by Def6; reconsider aa = abs a, xx1 = ||.x1.||, xx2 = ||.x2.|| as real number ; ( ||.(a * x1).|| = (abs a) * ||.x1.|| & ||.(a * x2).|| = (abs a) * ||.x2.|| ) by NORMSP_1:def_1; then w = aa * |[xx1,xx2]| by A10, EUCLID:58 .= (abs a) * v by A8, EUCLID:65 ; then |.w.| = (abs (abs a)) * |.v.| by EUCLID:11 .= (abs a) * |.v.| ; hence ||.(a * x).|| = (abs a) * ||.x.|| by A8, A10, A6, Def2; ::_thesis: verum end; thus ||.(x + y).|| <= ||.x.|| + ||.y.|| ::_thesis: verum proof consider w being Element of REAL 2 such that A11: ( w = <*||.(x1 + y1).||,||.(x2 + y2).||*> & (prod_NORM (G,F)) . ((x1 + y1),(x2 + y2)) = |.w.| ) by Def6; A12: ||.(x + y).|| = |.w.| by A11, A6, A7, Def1; A13: ( ||.(x1 + y1).|| <= ||.x1.|| + ||.y1.|| & ||.(x2 + y2).|| <= ||.x2.|| + ||.y2.|| ) by NORMSP_1:def_1; set t = <*(||.x1.|| + ||.y1.||),(||.x2.|| + ||.y2.||)*>; reconsider t = <*(||.x1.|| + ||.y1.||),(||.x2.|| + ||.y2.||)*> as FinSequence of REAL ; A14: ( len w = 2 & len t = 2 ) by A11, FINSEQ_1:44; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_(len_w)_holds_ (_0_<=_w_._i_&_w_._i_<=_t_._i_) let i be Element of NAT ; ::_thesis: ( i in Seg (len w) implies ( 0 <= w . b1 & w . b1 <= t . b1 ) ) assume i in Seg (len w) ; ::_thesis: ( 0 <= w . b1 & w . b1 <= t . b1 ) then A15: i in Seg 2 by A11, FINSEQ_1:44; percases ( i = 1 or i = 2 ) by A15, FINSEQ_1:2, TARSKI:def_2; supposeA16: i = 1 ; ::_thesis: ( 0 <= w . b1 & w . b1 <= t . b1 ) then w . i = ||.(x1 + y1).|| by A11, FINSEQ_1:44; hence ( 0 <= w . i & w . i <= t . i ) by A13, A16, FINSEQ_1:44, NORMSP_1:4; ::_thesis: verum end; supposeA17: i = 2 ; ::_thesis: ( 0 <= w . b1 & w . b1 <= t . b1 ) then w . i = ||.(x2 + y2).|| by A11, FINSEQ_1:44; hence ( 0 <= w . i & w . i <= t . i ) by A13, A17, FINSEQ_1:44, NORMSP_1:4; ::_thesis: verum end; end; end; then A18: |.w.| <= |.t.| by A14, PRVECT_2:2; t = |[||.x1.||,||.x2.||]| + |[||.y1.||,||.y2.||]| by EUCLID:56 .= v + z by A8, A9, EUCLID:64 ; then |.t.| <= |.v.| + |.z.| by EUCLID:12; hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A12, A6, A8, A7, A9, A18, XXREAL_0:2; ::_thesis: verum end; end; hence [:G,F:] is RealNormSpace-like by NORMSP_1:def_1; ::_thesis: verum 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 reconsider G0 = G, F0 = F as RealLinearSpace ; RLSStruct(# the carrier of [:G,F:], the ZeroF of [:G,F:], the addF of [:G,F:], the Mult of [:G,F:] #) = [:G0,F0:] ; hence ( [: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 ) by RSSPACE3:2; ::_thesis: verum 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 let S be set ; :: according to PRVECT_2:def_10 ::_thesis: ( not S in rng <*G*> or S is NORMSTR ) assume S in rng <*G*> ; ::_thesis: S is NORMSTR then consider i being set such that A1: ( i in dom <*G*> & <*G*> . i = S ) by FUNCT_1:def_3; reconsider i = i as Element of NAT by A1; len <*G*> = 1 by FINSEQ_1:40; then dom <*G*> = {1} by FINSEQ_1:2, FINSEQ_1:def_3; then i = 1 by A1, TARSKI:def_1; hence S is RealNormSpace by A1, FINSEQ_1:40; ::_thesis: verum 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 let S be set ; :: according to PRVECT_2:def_10 ::_thesis: ( not S in rng <*G,F*> or S is NORMSTR ) assume S in rng <*G,F*> ; ::_thesis: S is NORMSTR then consider i being set such that A1: ( i in dom <*G,F*> & <*G,F*> . i = S ) by FUNCT_1:def_3; reconsider i = i as Element of NAT by A1; dom <*G,F*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; then ( i = 1 or i = 2 ) by A1, TARSKI:def_2; hence S is RealNormSpace by A1, FINSEQ_1:44; ::_thesis: verum 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 let X, Y be RealNormSpace; ::_thesis: 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.|| ) ) reconsider X0 = X, Y0 = Y as RealLinearSpace ; consider I0 being Function of [:X0,Y0:],(product <*X0,Y0*>) such that A1: ( I0 is one-to-one & I0 is onto & ( for x being Point of X for y being Point of Y holds I0 . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X0,Y0:] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:X0,Y0:] for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0,Y0*>) = I0 . (0. [:X0,Y0:]) ) by Th12; A2: 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 [:X,Y:],(product <*X,Y*>) ; take I ; ::_thesis: ( 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.|| ) ) thus ( 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*> ) ) by A1, A2; ::_thesis: ( ( 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.|| ) ) thus for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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 let v, w be Point of [:X,Y:]; ::_thesis: I . (v + w) = (I . v) + (I . w) reconsider v0 = v, w0 = w as Point of [:X0,Y0:] ; thus I . (v + w) = I0 . (v0 + w0) .= (I0 . v0) + (I0 . w0) by A1 .= (I . v) + (I . w) by A2 ; ::_thesis: verum end; thus for v being Point of [:X,Y:] for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) ) proof let v be Point of [:X,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 [:X0,Y0:] ; thus I . (r * v) = I0 . (r * v0) .= r * (I0 . v0) by A1 .= r * (I . v) by A2 ; ::_thesis: verum end; thus 0. (product <*X,Y*>) = I . (0. [:X,Y:]) by A1, A2; ::_thesis: for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| proof let v be Point of [:X,Y:]; ::_thesis: ||.(I . v).|| = ||.v.|| consider x1 being Point of X, y1 being Point of Y such that A3: v = [x1,y1] by Lm1; consider v1 being Element of REAL 2 such that A4: ( v1 = <*||.x1.||,||.y1.||*> & (prod_NORM (X,Y)) . (x1,y1) = |.v1.| ) by Def6; A5: I . v = I . (x1,y1) by A3 .= <*x1,y1*> by A1 ; reconsider Iv = I . v as Element of product (carr <*X,Y*>) by A2; A6: ( <*x1,y1*> . 1 = x1 & <*x1,y1*> . 2 = y1 ) by FINSEQ_1:44; ( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def_2; then reconsider j1 = 1, j2 = 2 as Element of dom <*X,Y*> by FINSEQ_1:2, FINSEQ_1:89; A7: (normsequence (<*X,Y*>,Iv)) . j1 = the normF of (<*X,Y*> . j1) . (Iv . j1) by PRVECT_2:def_11 .= ||.x1.|| by A5, A6, FINSEQ_1:44 ; A8: (normsequence (<*X,Y*>,Iv)) . j2 = the normF of (<*X,Y*> . j2) . (Iv . j2) by PRVECT_2:def_11 .= ||.y1.|| by A5, A6, FINSEQ_1:44 ; len (normsequence (<*X,Y*>,Iv)) = len <*X,Y*> by PRVECT_2:def_11 .= 2 by FINSEQ_1:44 ; then normsequence (<*X,Y*>,Iv) = v1 by A4, A7, A8, FINSEQ_1:44; hence ||.(I . v).|| = ||.v.|| by A4, A3, A2, PRVECT_2:def_12; ::_thesis: verum end; hence for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ; ::_thesis: verum 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 let X be RealNormSpace; ::_thesis: 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.|| ) ) reconsider X0 = X as RealLinearSpace ; consider I0 being Function of X0,(product <*X0*>) such that A1: ( I0 is one-to-one & I0 is onto & ( for x being Point of X holds I0 . x = <*x*> ) & ( for v, w being Point of X0 holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of X0 for r being Element of REAL holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0*>) = I0 . (0. X0) ) by Th11; A2: product <*X*> = NORMSTR(# (product (carr <*X*>)),(zeros <*X*>),[:(addop <*X*>):],[:(multop <*X*>):],(productnorm <*X*>) #) by PRVECT_2:6; then reconsider I = I0 as Function of X,(product <*X*>) ; take I ; ::_thesis: ( 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.|| ) ) thus ( I is one-to-one & I is onto & ( for x being Point of X holds I . x = <*x*> ) ) by A1, A2; ::_thesis: ( ( 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.|| ) ) thus for v, w being Point of X holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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 let v, w be Point of X; ::_thesis: I . (v + w) = (I . v) + (I . w) reconsider v0 = v, w0 = w as Point of X0 ; thus I . (v + w) = (I0 . v0) + (I0 . w0) by A1 .= (I . v) + (I . w) by A2 ; ::_thesis: verum end; thus for v being Point of X for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( 0. (product <*X*>) = I . (0. X) & ( for v being Point of X holds ||.(I . v).|| = ||.v.|| ) ) proof let v be Point of X; ::_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 X0 ; thus I . (r * v) = r * (I0 . v0) by A1 .= r * (I . v) by A2 ; ::_thesis: verum end; thus 0. (product <*X*>) = I . (0. X) by A1, A2; ::_thesis: for v being Point of X holds ||.(I . v).|| = ||.v.|| thus for v being Point of X holds ||.(I . v).|| = ||.v.|| ::_thesis: verum proof let v be Point of X; ::_thesis: ||.(I . v).|| = ||.v.|| len <*||.v.||*> = 1 by FINSEQ_1:40; then reconsider v1 = <*||.v.||*> as Element of REAL 1 by FINSEQ_2:92; A3: |.v1.| = sqrt (Sum <*(||.v.|| ^2)*>) by RVSUM_1:55 .= sqrt (||.v.|| ^2) by RVSUM_1:73 .= ||.v.|| by NORMSP_1:4, SQUARE_1:22 ; A4: I . v = <*v*> by A1; reconsider Iv = I . v as Element of product (carr <*X*>) by A2; A5: <*v*> . 1 = v by FINSEQ_1:40; 1 in {1} by TARSKI:def_1; then reconsider j1 = 1 as Element of dom <*X*> by FINSEQ_1:2, FINSEQ_1:def_8; A6: (normsequence (<*X*>,Iv)) . j1 = the normF of (<*X*> . j1) . (Iv . j1) by PRVECT_2:def_11 .= ||.v.|| by A4, A5, FINSEQ_1:40 ; len (normsequence (<*X*>,Iv)) = len <*X*> by PRVECT_2:def_11 .= 1 by FINSEQ_1:40 ; then normsequence (<*X*>,Iv) = v1 by A6, FINSEQ_1:40; hence ||.(I . v).|| = ||.v.|| by A3, A2, PRVECT_2:def_12; ::_thesis: verum end; end; 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 ); proof for S being set st S in rng (G ^ F) holds S is RealNormSpace proof let S be set ; ::_thesis: ( S in rng (G ^ F) implies S is RealNormSpace ) assume S in rng (G ^ F) ; ::_thesis: S is RealNormSpace then consider i being set such that A1: ( i in dom (G ^ F) & (G ^ F) . i = S ) by FUNCT_1:def_3; reconsider i = i as Element of NAT by A1; percases ( i in dom G or ex n being Nat st ( n in dom F & i = (len G) + n ) ) by A1, FINSEQ_1:25; supposeA2: i in dom G ; ::_thesis: S is RealNormSpace then G . i in rng G by FUNCT_1:3; then G . i is RealNormSpace by PRVECT_2:def_10; hence S is RealNormSpace by A1, A2, FINSEQ_1:def_7; ::_thesis: verum end; suppose ex n being Nat st ( n in dom F & i = (len G) + n ) ; ::_thesis: S is RealNormSpace then consider n being Nat such that A3: ( n in dom F & i = (len G) + n ) ; F . n in rng F by A3, FUNCT_1:3; then F . n is RealNormSpace by PRVECT_2:def_10; hence S is RealNormSpace by A1, A3, FINSEQ_1:def_7; ::_thesis: verum end; end; end; hence ( not G ^ F is empty & G ^ F is RealNormSpace-yielding ) by PRVECT_2:def_10; ::_thesis: verum 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 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 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 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_2:def_4; 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; A14: |.v1.| = sqrt (Sum <*(||.x1.|| ^2),(||.y1.|| ^2)*>) 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; percases ( k in dom X or ex n being Nat st ( n in dom Y & k = (len X) + n ) ) by A19, FINSEQ_1:25; supposeA23: 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 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 let G, F be RealNormSpace; ::_thesis: ( ( 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.| ) ) ) thus 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] ) by Lm1; ::_thesis: ( ( 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.| ) ) ) thus 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)] by Def1; ::_thesis: ( 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.| ) ) ) thus 0. [:G,F:] = [(0. G),(0. F)] ; ::_thesis: ( ( 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.| ) ) ) thus 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)] ::_thesis: ( ( 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 let x be Point of [:G,F:]; ::_thesis: for x1 being Point of G for x2 being Point of F st x = [x1,x2] holds - x = [(- x1),(- x2)] let x1 be Point of G; ::_thesis: for x2 being Point of F st x = [x1,x2] holds - x = [(- x1),(- x2)] let x2 be Point of F; ::_thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] ) assume A1: x = [x1,x2] ; ::_thesis: - x = [(- x1),(- x2)] reconsider y = [(- x1),(- x2)] as Point of [:G,F:] ; x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, Def1 .= [(0. G),(x2 + (- x2))] by RLVECT_1:def_10 .= 0. [:G,F:] by RLVECT_1:def_10 ; hence - x = [(- x1),(- x2)] by RLVECT_1:def_10; ::_thesis: verum end; thus 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)] ::_thesis: 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 let x be Point of [:G,F:]; ::_thesis: 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)] let x1 be Point of G; ::_thesis: for x2 being Point of F for a being real number st x = [x1,x2] holds a * x = [(a * x1),(a * x2)] let x2 be Point of F; ::_thesis: for a being real number st x = [x1,x2] holds a * x = [(a * x1),(a * x2)] let a be real number ; ::_thesis: ( x = [x1,x2] implies a * x = [(a * x1),(a * x2)] ) assume A2: x = [x1,x2] ; ::_thesis: a * x = [(a * x1),(a * x2)] reconsider a0 = a as Element of REAL by XREAL_0:def_1; thus a * x = (prod_MLT (G,F)) . (a0,x) .= [(a * x1),(a * x2)] by A2, Def2 ; ::_thesis: verum end; thus 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.| ) ::_thesis: verum proof let x be Point of [:G,F:]; ::_thesis: 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.| ) let x1 be Point of G; ::_thesis: for x2 being Point of F st x = [x1,x2] holds ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) let x2 be Point of F; ::_thesis: ( x = [x1,x2] implies ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) assume A3: x = [x1,x2] ; ::_thesis: ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.w.| ) by Def6; hence ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) by A3; ::_thesis: verum end; 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 let G, F be RealNormSpace; ::_thesis: ( ( 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.| ) ) ) consider I being Function of [:G,F:],(product <*G,F*>) such that A1: ( I is one-to-one & I is onto & ( for x being Point of G for y being Point of F holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:G,F:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:G,F:] for r being Element of REAL holds I . (r * v) = r * (I . v) ) & 0. (product <*G,F*>) = I . (0. [:G,F:]) & ( for v being Point of [:G,F:] holds ||.(I . v).|| = ||.v.|| ) ) by Th15; thus A2: 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*> ) ::_thesis: ( ( 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 let y be set ; ::_thesis: ( y is Point of (product <*G,F*>) iff ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> ) hereby ::_thesis: ( ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> implies y is Point of (product <*G,F*>) ) assume y is Point of (product <*G,F*>) ; ::_thesis: ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> then y in the carrier of (product <*G,F*>) ; then y in rng I by A1, FUNCT_2:def_3; then consider x being Element of the carrier of [:G,F:] such that A3: y = I . x by FUNCT_2:113; consider x1 being Point of G, x2 being Point of F such that A4: x = [x1,x2] by Lm1; take x1 = x1; ::_thesis: ex x2 being Point of F st y = <*x1,x2*> take x2 = x2; ::_thesis: y = <*x1,x2*> I . (x1,x2) = <*x1,x2*> by A1; hence y = <*x1,x2*> by A3, A4; ::_thesis: verum end; hereby ::_thesis: verum assume ex x1 being Point of G ex x2 being Point of F st y = <*x1,x2*> ; ::_thesis: y is Point of (product <*G,F*>) then consider x1 being Point of G, x2 being Point of F such that A5: y = <*x1,x2*> ; A6: I . [x1,x2] in rng I by FUNCT_2:112; I . (x1,x2) = <*x1,x2*> by A1; hence y is Point of (product <*G,F*>) by A5, A6; ::_thesis: verum end; end; thus A7: 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)*> ::_thesis: ( 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 let x, y be Point of (product <*G,F*>); ::_thesis: 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)*> let x1, y1 be Point of G; ::_thesis: for x2, y2 being Point of F st x = <*x1,x2*> & y = <*y1,y2*> holds x + y = <*(x1 + y1),(x2 + y2)*> let x2, y2 be Point of F; ::_thesis: ( x = <*x1,x2*> & y = <*y1,y2*> implies x + y = <*(x1 + y1),(x2 + y2)*> ) assume A8: ( x = <*x1,x2*> & y = <*y1,y2*> ) ; ::_thesis: x + y = <*(x1 + y1),(x2 + y2)*> reconsider z = [x1,x2], w = [y1,y2] as Point of [:G,F:] ; A9: z + w = [(x1 + y1),(x2 + y2)] by Def1; A10: I . ((x1 + y1),(x2 + y2)) = <*(x1 + y1),(x2 + y2)*> by A1; ( I . (x1,x2) = <*x1,x2*> & I . (y1,y2) = <*y1,y2*> ) by A1; hence <*(x1 + y1),(x2 + y2)*> = x + y by A1, A9, A10, A8; ::_thesis: verum end; thus A11: 0. (product <*G,F*>) = <*(0. G),(0. F)*> ::_thesis: ( ( 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 I . ((0. G),(0. F)) = <*(0. G),(0. F)*> by A1; hence 0. (product <*G,F*>) = <*(0. G),(0. F)*> by A1; ::_thesis: verum end; thus 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)*> ::_thesis: ( ( 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 let x be Point of (product <*G,F*>); ::_thesis: for x1 being Point of G for x2 being Point of F st x = <*x1,x2*> holds - x = <*(- x1),(- x2)*> let x1 be Point of G; ::_thesis: for x2 being Point of F st x = <*x1,x2*> holds - x = <*(- x1),(- x2)*> let x2 be Point of F; ::_thesis: ( x = <*x1,x2*> implies - x = <*(- x1),(- x2)*> ) assume A12: x = <*x1,x2*> ; ::_thesis: - x = <*(- x1),(- x2)*> reconsider y = <*(- x1),(- x2)*> as Point of (product <*G,F*>) by A2; x + y = <*(x1 + (- x1)),(x2 + (- x2))*> by A7, A12 .= <*(0. G),(x2 + (- x2))*> by RLVECT_1:def_10 .= 0. (product <*G,F*>) by A11, RLVECT_1:def_10 ; hence - x = <*(- x1),(- x2)*> by RLVECT_1:def_10; ::_thesis: verum end; thus 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)*> ::_thesis: 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 let x be Point of (product <*G,F*>); ::_thesis: 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)*> let x1 be Point of G; ::_thesis: for x2 being Point of F for a being real number st x = <*x1,x2*> holds a * x = <*(a * x1),(a * x2)*> let x2 be Point of F; ::_thesis: for a being real number st x = <*x1,x2*> holds a * x = <*(a * x1),(a * x2)*> let a be real number ; ::_thesis: ( x = <*x1,x2*> implies a * x = <*(a * x1),(a * x2)*> ) assume A13: x = <*x1,x2*> ; ::_thesis: a * x = <*(a * x1),(a * x2)*> reconsider a0 = a as Element of REAL by XREAL_0:def_1; reconsider y = [x1,x2] as Point of [:G,F:] ; A14: <*x1,x2*> = I . (x1,x2) by A1; I . (a * y) = I . ((a0 * x1),(a0 * x2)) by Th18 .= <*(a0 * x1),(a0 * x2)*> by A1 ; hence a * x = <*(a * x1),(a * x2)*> by A13, A14, A1; ::_thesis: verum end; thus 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.| ) ::_thesis: verum proof let x be Point of (product <*G,F*>); ::_thesis: 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.| ) let x1 be Point of G; ::_thesis: for x2 being Point of F st x = <*x1,x2*> holds ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) let x2 be Point of F; ::_thesis: ( x = <*x1,x2*> implies ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) assume A15: x = <*x1,x2*> ; ::_thesis: ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) reconsider y = [x1,x2] as Point of [:G,F:] ; consider w being Element of REAL 2 such that A16: ( w = <*||.x1.||,||.x2.||*> & ||.y.|| = |.w.| ) by Th18; take w ; ::_thesis: ( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) A17: I . y = I . (x1,x2) .= x by A1, A15 ; thus w = <*||.x1.||,||.x2.||*> by A16; ::_thesis: ||.x.|| = |.w.| thus ||.x.|| = |.w.| by A1, A16, A17; ::_thesis: verum end; end; registration let X, Y be complete RealNormSpace; cluster[:X,Y:] -> non empty strict complete ; coherence [:X,Y:] is complete proof A1: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; now__::_thesis:_for_i_being_Element_of_dom_<*X,Y*>_holds_<*X,Y*>_._i_is_complete let i be Element of dom <*X,Y*>; ::_thesis: <*X,Y*> . i is complete ( i = 1 or i = 2 ) by A1, TARSKI:def_2; hence <*X,Y*> . i is complete by FINSEQ_1:44; ::_thesis: verum end; then A2: product <*X,Y*> is complete by PRVECT_2:14; consider I being Function of [:X,Y:],(product <*X,Y*>) such that A3: ( 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.|| ) ) by Th15; A4: now__::_thesis:_for_v,_w_being_Point_of_[:X,Y:]_holds_I_._(v_-_w)_=_(I_._v)_-_(I_._w) let v, w be Point of [:X,Y:]; ::_thesis: I . (v - w) = (I . v) - (I . w) thus I . (v - w) = I . (v + ((- 1) * w)) by RLVECT_1:16 .= (I . v) + (I . ((- 1) * w)) by A3 .= (I . v) + ((- 1) * (I . w)) by A3 .= (I . v) - (I . w) by RLVECT_1:16 ; ::_thesis: verum end; A5: now__::_thesis:_for_v,_w_being_Point_of_[:X,Y:]_holds_||.((I_._v)_-_(I_._w)).||_=_||.(v_-_w).|| let v, w be Point of [:X,Y:]; ::_thesis: ||.((I . v) - (I . w)).|| = ||.(v - w).|| thus ||.((I . v) - (I . w)).|| = ||.(I . (v - w)).|| by A4 .= ||.(v - w).|| by A3 ; ::_thesis: verum end; now__::_thesis:_for_seq_being_sequence_of_[:X,Y:]_st_seq_is_Cauchy_sequence_by_Norm_holds_ seq_is_convergent let seq be sequence of [:X,Y:]; ::_thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent ) assume A6: seq is Cauchy_sequence_by_Norm ; ::_thesis: seq is convergent reconsider Iseq = I * seq as sequence of (product <*X,Y*>) ; now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.((Iseq_._n)_-_(Iseq_._m)).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Iseq . n) - (Iseq . m)).|| < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((Iseq . n) - (Iseq . m)).|| < r then consider k being Element of NAT such that A7: for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r by A6, RSSPACE3:8; take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.((Iseq . n) - (Iseq . m)).|| < r hereby ::_thesis: verum let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((Iseq . n) - (Iseq . m)).|| < r ) assume ( n >= k & m >= k ) ; ::_thesis: ||.((Iseq . n) - (Iseq . m)).|| < r then A8: ||.((seq . n) - (seq . m)).|| < r by A7; NAT = dom seq by FUNCT_2:def_1; then ( Iseq . n = I . (seq . n) & Iseq . m = I . (seq . m) ) by FUNCT_1:13; hence ||.((Iseq . n) - (Iseq . m)).|| < r by A8, A5; ::_thesis: verum end; end; then Iseq is Cauchy_sequence_by_Norm by RSSPACE3:8; then A9: Iseq is convergent by A2, LOPBAN_1:def_15; ( dom (I ") = rng I & rng (I ") = dom I ) by A3, FUNCT_1:33; then ( dom (I ") = the carrier of (product <*X,Y*>) & rng (I ") = the carrier of [:X,Y:] ) by A3, FUNCT_2:def_1, FUNCT_2:def_3; then reconsider Lseq = (I ") . (lim Iseq) as Point of [:X,Y:] by FUNCT_1:3; rng I = the carrier of (product <*X,Y*>) by A3, FUNCT_2:def_3; then A10: I . Lseq = lim Iseq by A3, FUNCT_1:35; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ ||.((seq_._n)_-_Lseq).||_<_r let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((seq . n) - Lseq).|| < r ) assume 0 < r ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((seq . n) - Lseq).|| < r then consider m being Element of NAT such that A11: for n being Element of NAT st m <= n holds ||.((Iseq . n) - (lim Iseq)).|| < r by A9, NORMSP_1:def_7; take m = m; ::_thesis: for n being Element of NAT st m <= n holds ||.((seq . n) - Lseq).|| < r thus for n being Element of NAT st m <= n holds ||.((seq . n) - Lseq).|| < r ::_thesis: verum proof let n be Element of NAT ; ::_thesis: ( m <= n implies ||.((seq . n) - Lseq).|| < r ) assume m <= n ; ::_thesis: ||.((seq . n) - Lseq).|| < r then A12: ||.((Iseq . n) - (lim Iseq)).|| < r by A11; NAT = dom seq by FUNCT_2:def_1; then Iseq . n = I . (seq . n) by FUNCT_1:13; hence ||.((seq . n) - Lseq).|| < r by A10, A5, A12; ::_thesis: verum end; end; hence seq is convergent by NORMSP_1:def_6; ::_thesis: verum end; hence [:X,Y:] is complete by LOPBAN_1:def_15; ::_thesis: verum 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 let X, Y be RealNormSpace-Sequence; ::_thesis: 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.|| ) ) set PX = product X; set PY = product Y; set PXY = product (X ^ Y); consider K being Function of [:(product X),(product Y):],(product (X ^ Y)) such that A1: ( K is one-to-one & K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),(product Y):] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(K . v).|| = ||.v.|| ) ) by Th17; consider J being Function of [:(product X),(product Y):],(product <*(product X),(product Y)*>) such that A2: ( J is one-to-one & J is onto & ( for x being Point of (product X) for y being Point of (product Y) holds J . (x,y) = <*x,y*> ) & ( for v, w being Point of [:(product X),(product Y):] holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of [:(product X),(product Y):] for r being Element of REAL holds J . (r * v) = r * (J . v) ) & 0. (product <*(product X),(product Y)*>) = J . (0. [:(product X),(product Y):]) & ( for v being Point of [:(product X),(product Y):] holds ||.(J . v).|| = ||.v.|| ) ) by Th15; A3: rng J = the carrier of (product <*(product X),(product Y)*>) by A2, FUNCT_2:def_3; then reconsider JB = J " as Function of the carrier of (product <*(product X),(product Y)*>), the carrier of [:(product X),(product Y):] by A2, FUNCT_2:25; A4: ( dom (J ") = rng J & rng (J ") = dom J ) by A2, FUNCT_1:33; then A5: dom (J ") = the carrier of (product <*(product X),(product Y)*>) by A2, FUNCT_2:def_3; A6: rng (J ") = the carrier of [:(product X),(product Y):] by A4, FUNCT_2:def_1; reconsider I = K * JB as Function of (product <*(product X),(product Y)*>),(product (X ^ Y)) ; 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 <*(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.|| ) ) thus I is one-to-one by A1, A2; ::_thesis: ( 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.|| ) ) rng K = the carrier of (product (X ^ Y)) by A1, FUNCT_2:def_3; then rng I = the carrier of (product (X ^ Y)) by A6, FUNCT_2:14; hence I is onto by FUNCT_2:def_3; ::_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 <*(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.|| ) ) 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 ) ::_thesis: ( ( 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 let x be Point of (product X); ::_thesis: for y being Point of (product Y) ex x1, y1 being FinSequence st ( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) let y be Point of (product Y); ::_thesis: ex x1, y1 being FinSequence st ( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) consider x1, y1 being FinSequence such that A7: ( x = x1 & y = y1 & K . (x,y) = x1 ^ y1 ) by A1; A8: J . (x,y) = <*x,y*> by A2; [x,y] in the carrier of [:(product X),(product Y):] ; then A9: [x,y] in dom J by FUNCT_2:def_1; <*x,y*> is Point of (product <*(product X),(product Y)*>) by Th19; then I . <*x,y*> = K . (JB . (J . [x,y])) by A8, A5, FUNCT_1:13; then I . <*x,y*> = x1 ^ y1 by A7, A9, A2, FUNCT_1:34; hence ex x1, y1 being FinSequence st ( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) by A7; ::_thesis: verum end; thus for v, w being Point of (product <*(product X),(product Y)*>) holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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 let v, w be Point of (product <*(product X),(product Y)*>); ::_thesis: I . (v + w) = (I . v) + (I . w) consider x being Element of the carrier of [:(product X),(product Y):] such that A10: v = J . x by A3, FUNCT_2:113; consider y being Element of the carrier of [:(product X),(product Y):] such that A11: w = J . y by A3, FUNCT_2:113; ( x in the carrier of [:(product X),(product Y):] & y in the carrier of [:(product X),(product Y):] & x + y in the carrier of [:(product X),(product Y):] ) ; then ( x in dom J & y in dom J & x + y in dom J ) by FUNCT_2:def_1; then A12: ( JB . v = x & JB . w = y & JB . (J . (x + y)) = x + y ) by A10, A11, A2, FUNCT_1:34; ( v in rng J & w in rng J ) by A3; then A13: ( v in dom JB & w in dom JB ) by A2, FUNCT_1:33; v + w = J . (x + y) by A10, A11, A2; then I . (v + w) = K . (x + y) by A12, A5, FUNCT_1:13 .= (K . x) + (K . y) by A1 .= ((K * JB) . v) + (K . (JB . w)) by A12, A13, FUNCT_1:13 ; hence I . (v + w) = (I . v) + (I . w) by A13, FUNCT_1:13; ::_thesis: verum end; thus for v being Point of (product <*(product X),(product Y)*>) for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( 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 let v be Point of (product <*(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) consider x being Element of the carrier of [:(product X),(product Y):] such that A14: v = J . x by A3, FUNCT_2:113; x in the carrier of [:(product X),(product Y):] ; then x in dom J by FUNCT_2:def_1; then A15: JB . v = x by A14, A2, FUNCT_1:34; v in rng J by A3; then A16: v in dom JB by A2, FUNCT_1:33; r * x in the carrier of [:(product X),(product Y):] ; then A17: r * x in dom J by FUNCT_2:def_1; r * v = J . (r * x) by A14, A2; then I . (r * v) = K . (JB . (J . (r * x))) by A5, FUNCT_1:13; hence I . (r * v) = K . (r * x) by A17, A2, FUNCT_1:34 .= r * (K . x) by A1 .= r * (I . v) by A15, A16, FUNCT_1:13 ; ::_thesis: verum end; thus I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) ::_thesis: for v being Point of (product <*(product X),(product Y)*>) holds ||.(I . v).|| = ||.v.|| proof 0. [:(product X),(product Y):] in the carrier of [:(product X),(product Y):] ; then A18: 0. [:(product X),(product Y):] in dom J by FUNCT_2:def_1; 0. (product <*(product X),(product Y)*>) in rng J by A3; then 0. (product <*(product X),(product Y)*>) in dom JB by A2, FUNCT_1:33; then I . (0. (product <*(product X),(product Y)*>)) = K . (JB . (J . (0. [:(product X),(product Y):]))) by A2, FUNCT_1:13; hence I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) by A1, A18, A2, FUNCT_1:34; ::_thesis: verum end; thus for v being Point of (product <*(product X),(product Y)*>) holds ||.(I . v).|| = ||.v.|| ::_thesis: verum proof let v be Point of (product <*(product X),(product Y)*>); ::_thesis: ||.(I . v).|| = ||.v.|| consider x being Element of the carrier of [:(product X),(product Y):] such that A19: v = J . x by A3, FUNCT_2:113; x in the carrier of [:(product X),(product Y):] ; then A20: x in dom J by FUNCT_2:def_1; v in rng J by A3; then v in dom JB by A2, FUNCT_1:33; then I . v = K . (JB . (J . x)) by A19, FUNCT_1:13 .= K . x by A20, A2, FUNCT_1:34 ; then ||.(I . v).|| = ||.x.|| by A1; hence ||.(I . v).|| = ||.v.|| by A2, A19; ::_thesis: verum end; 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 let X, Y be RealLinearSpace; ::_thesis: 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*>):] ) consider J being Function of Y,(product <*Y*>) such that A1: ( J is one-to-one & J is onto & ( for y being Point of Y holds J . y = <*y*> ) & ( for v, w being Point of Y holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of Y for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. Y) = 0. (product <*Y*>) ) by Th11; defpred S1[ set , set , set ] means $3 = [$1,<*$2*>]; A2: for x, y being set st x in the carrier of X & y in the carrier of Y holds ex z being set st ( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) proof let x, y be set ; ::_thesis: ( x in the carrier of X & y in the carrier of Y implies ex z being set st ( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) ) assume A3: ( x in the carrier of X & y in the carrier of Y ) ; ::_thesis: ex z being set st ( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) then reconsider y0 = y as Point of Y ; J . y0 = <*y0*> by A1; then [x,<*y*>] in [: the carrier of X, the carrier of (product <*Y*>):] by A3, ZFMISC_1:87; hence ex z being set st ( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) ; ::_thesis: verum end; consider I being Function of [: the carrier of X, the carrier of Y:], the carrier of [:X,(product <*Y*>):] such that A4: for x, y being set st x in the carrier of X & y in the carrier of Y holds S1[x,y,I . (x,y)] from BINOP_1:sch_1(A2); reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ; take I ; ::_thesis: ( 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*>):] ) now__::_thesis:_for_z1,_z2_being_set_st_z1_in_the_carrier_of_[:X,Y:]_&_z2_in_the_carrier_of_[:X,Y:]_&_I_._z1_=_I_._z2_holds_ z1_=_z2 let z1, z2 be set ; ::_thesis: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 implies z1 = z2 ) assume A5: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2 consider x1, y1 being set such that A6: ( x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1] ) by A5, ZFMISC_1:def_2; consider x2, y2 being set such that A7: ( x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2] ) by A5, ZFMISC_1:def_2; [x1,<*y1*>] = I . (x1,y1) by A4, A6 .= I . (x2,y2) by A5, A6, A7 .= [x2,<*y2*>] by A4, A7 ; then ( x1 = x2 & <*y1*> = <*y2*> ) by XTUPLE_0:1; hence z1 = z2 by A6, A7, FINSEQ_1:76; ::_thesis: verum end; hence I is one-to-one by FUNCT_2:19; ::_thesis: ( 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*>):] ) now__::_thesis:_for_w_being_set_st_w_in_the_carrier_of_[:X,(product_<*Y*>):]_holds_ w_in_rng_I let w be set ; ::_thesis: ( w in the carrier of [:X,(product <*Y*>):] implies w in rng I ) assume w in the carrier of [:X,(product <*Y*>):] ; ::_thesis: w in rng I then consider x, y1 being set such that A8: ( x in the carrier of X & y1 in the carrier of (product <*Y*>) & w = [x,y1] ) by ZFMISC_1:def_2; y1 in rng J by A1, A8, FUNCT_2:def_3; then consider y being set such that A9: ( y in the carrier of Y & y1 = J . y ) by FUNCT_2:11; reconsider z = [x,y] as Element of [: the carrier of X, the carrier of Y:] by A8, A9, ZFMISC_1:87; J . y = <*y*> by A9, A1; then w = I . (x,y) by A4, A8, A9; then w = I . z ; hence w in rng I by FUNCT_2:4; ::_thesis: verum end; then the carrier of [:X,(product <*Y*>):] c= rng I by TARSKI:def_3; then the carrier of [:X,(product <*Y*>):] = rng I by XBOOLE_0:def_10; hence I is onto by FUNCT_2:def_3; ::_thesis: ( ( 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*>):] ) thus for x being Point of X for y being Point of Y holds I . (x,y) = [x,<*y*>] by A4; ::_thesis: ( ( 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*>):] ) thus for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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 let v, w be Point of [:X,Y:]; ::_thesis: I . (v + w) = (I . v) + (I . w) consider x1 being Point of X, x2 being Point of Y such that A10: v = [x1,x2] by Lm1; consider y1 being Point of X, y2 being Point of Y such that A11: w = [y1,y2] by Lm1; A12: I . (v + w) = I . ((x1 + y1),(x2 + y2)) by A10, A11, Def1 .= [(x1 + y1),<*(x2 + y2)*>] by A4 ; ( I . v = I . (x1,x2) & I . w = I . (y1,y2) ) by A10, A11; then A13: ( I . v = [x1,<*x2*>] & I . w = [y1,<*y2*>] ) by A4; A14: ( J . x2 = <*x2*> & J . y2 = <*y2*> ) by A1; then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ; reconsider yy2 = <*y2*> as Point of (product <*Y*>) by A14; <*(x2 + y2)*> = J . (x2 + y2) by A1 .= xx2 + yy2 by A14, A1 ; hence (I . v) + (I . w) = I . (v + w) by A12, A13, Def1; ::_thesis: verum end; thus for v being Point of [:X,Y:] for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] proof let v be Point of [:X,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) consider x1 being Point of X, x2 being Point of Y such that A15: v = [x1,x2] by Lm1; A16: I . (r * v) = I . ((r * x1),(r * x2)) by A15, Th9 .= [(r * x1),<*(r * x2)*>] by A4 ; A17: I . v = I . (x1,x2) by A15 .= [x1,<*x2*>] by A4 ; A18: J . x2 = <*x2*> by A1; then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ; <*(r * x2)*> = J . (r * x2) by A1 .= r * xx2 by A18, A1 ; hence r * (I . v) = I . (r * v) by A16, A17, Th9; ::_thesis: verum end; A19: <*(0. Y)*> = 0. (product <*Y*>) by A1; I . (0. [:X,Y:]) = I . ((0. X),(0. Y)) ; hence I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] by A19, A4; ::_thesis: verum 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 let X be RealLinearSpace-Sequence; ::_thesis: 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*>)) ) let Y be RealLinearSpace; ::_thesis: 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*>)) ) consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that A1: ( I is one-to-one & I is onto & ( for x being Point of (product X) for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( 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),(product <*Y*>):] ) by Th21; consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*Y*>)) such that A2: ( J is one-to-one & J 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 & J . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product <*Y*>):] holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of [:(product X),(product <*Y*>):] for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. [:(product X),(product <*Y*>):]) = 0. (product (X ^ <*Y*>)) ) by Th13; set K = J * I; reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ; take K ; ::_thesis: ( K is one-to-one & K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) ) thus K is one-to-one by A1, A2; ::_thesis: ( K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) ) A3: rng J = the carrier of (product (X ^ <*Y*>)) by A2, FUNCT_2:def_3; rng I = the carrier of [:(product X),(product <*Y*>):] by A1, FUNCT_2:def_3; then rng (J * I) = J .: the carrier of [:(product X),(product <*Y*>):] by RELAT_1:127 .= the carrier of (product (X ^ <*Y*>)) by A3, RELSET_1:22 ; hence K is onto by FUNCT_2:def_3; ::_thesis: ( ( for x being Point of (product X) for y being Point of Y ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) ) thus for x being Point of (product X) for y being Point of Y ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ::_thesis: ( ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) ) proof let x be Point of (product X); ::_thesis: for y being Point of Y ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) let y be Point of Y; ::_thesis: ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) A4: I . (x,y) = [x,<*y*>] by A1; [x,y] in the carrier of [:(product X),Y:] ; then [x,<*y*>] in the carrier of [:(product X),(product <*Y*>):] by A4, FUNCT_2:5; then reconsider yy = <*y*> as Point of (product <*Y*>) by ZFMISC_1:87; consider x1, y1 being FinSequence such that A5: ( x = x1 & yy = y1 & J . (x,yy) = x1 ^ y1 ) by A2; J . (x,yy) = J . (I . [x,y]) by A4 .= K . (x,y) by FUNCT_2:15 ; hence ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) by A5; ::_thesis: verum end; thus for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ::_thesis: ( ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) ) proof let v, w be Point of [:(product X),Y:]; ::_thesis: K . (v + w) = (K . v) + (K . w) thus K . (v + w) = J . (I . (v + w)) by FUNCT_2:15 .= J . ((I . v) + (I . w)) by A1 .= (J . (I . v)) + (J . (I . w)) by A2 .= (K . v) + (J . (I . w)) by FUNCT_2:15 .= (K . v) + (K . w) by FUNCT_2:15 ; ::_thesis: verum end; thus for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ::_thesis: K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) proof let v be Point of [:(product X),Y:]; ::_thesis: for r being Element of REAL holds K . (r * v) = r * (K . v) let r be Element of REAL ; ::_thesis: K . (r * v) = r * (K . v) thus K . (r * v) = J . (I . (r * v)) by FUNCT_2:15 .= J . (r * (I . v)) by A1 .= r * (J . (I . v)) by A2 .= r * (K . v) by FUNCT_2:15 ; ::_thesis: verum end; thus K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) by A1, A2, FUNCT_2:15; ::_thesis: verum 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 let X, Y be RealNormSpace; ::_thesis: 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.|| ) ) consider J being Function of Y,(product <*Y*>) such that A1: ( J is one-to-one & J is onto & ( for y being Point of Y holds J . y = <*y*> ) & ( for v, w being Point of Y holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of Y for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. Y) = 0. (product <*Y*>) & ( for v being Point of Y holds ||.(J . v).|| = ||.v.|| ) ) by Th16; defpred S1[ set , set , set ] means $3 = [$1,<*$2*>]; A2: for x, y being set st x in the carrier of X & y in the carrier of Y holds ex z being set st ( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) proof let x, y be set ; ::_thesis: ( x in the carrier of X & y in the carrier of Y implies ex z being set st ( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) ) assume A3: ( x in the carrier of X & y in the carrier of Y ) ; ::_thesis: ex z being set st ( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) then reconsider y0 = y as Point of Y ; J . y0 = <*y0*> by A1; then [x,<*y*>] in [: the carrier of X, the carrier of (product <*Y*>):] by A3, ZFMISC_1:87; hence ex z being set st ( z in the carrier of [:X,(product <*Y*>):] & S1[x,y,z] ) ; ::_thesis: verum end; consider I being Function of [: the carrier of X, the carrier of Y:], the carrier of [:X,(product <*Y*>):] such that A4: for x, y being set st x in the carrier of X & y in the carrier of Y holds S1[x,y,I . (x,y)] from BINOP_1:sch_1(A2); reconsider I = I as Function of [:X,Y:],[:X,(product <*Y*>):] ; take I ; ::_thesis: ( 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.|| ) ) thus I is one-to-one ::_thesis: ( 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 now__::_thesis:_for_z1,_z2_being_set_st_z1_in_the_carrier_of_[:X,Y:]_&_z2_in_the_carrier_of_[:X,Y:]_&_I_._z1_=_I_._z2_holds_ z1_=_z2 let z1, z2 be set ; ::_thesis: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 implies z1 = z2 ) assume A5: ( z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I . z1 = I . z2 ) ; ::_thesis: z1 = z2 then consider x1, y1 being set such that A6: ( x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1] ) by ZFMISC_1:def_2; consider x2, y2 being set such that A7: ( x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2] ) by A5, ZFMISC_1:def_2; A8: [x1,<*y1*>] = I . (x1,y1) by A4, A6 .= I . (x2,y2) by A5, A6, A7 .= [x2,<*y2*>] by A4, A7 ; then <*y1*> = <*y2*> by XTUPLE_0:1; then y1 = y2 by FINSEQ_1:76; hence z1 = z2 by A6, A7, A8, XTUPLE_0:1; ::_thesis: verum end; hence I is one-to-one by FUNCT_2:19; ::_thesis: verum end; thus I is onto ::_thesis: ( ( 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 now__::_thesis:_for_w_being_set_st_w_in_the_carrier_of_[:X,(product_<*Y*>):]_holds_ w_in_rng_I let w be set ; ::_thesis: ( w in the carrier of [:X,(product <*Y*>):] implies w in rng I ) assume w in the carrier of [:X,(product <*Y*>):] ; ::_thesis: w in rng I then consider x, y1 being set such that A9: ( x in the carrier of X & y1 in the carrier of (product <*Y*>) & w = [x,y1] ) by ZFMISC_1:def_2; y1 in rng J by A1, A9, FUNCT_2:def_3; then consider y being set such that A10: ( y in the carrier of Y & y1 = J . y ) by FUNCT_2:11; A11: J . y = <*y*> by A10, A1; reconsider z = [x,y] as Element of [: the carrier of X, the carrier of Y:] by A9, A10, ZFMISC_1:87; w = I . (x,y) by A4, A9, A10, A11 .= I . z ; hence w in rng I by FUNCT_2:4; ::_thesis: verum end; then the carrier of [:X,(product <*Y*>):] c= rng I by TARSKI:def_3; then the carrier of [:X,(product <*Y*>):] = rng I by XBOOLE_0:def_10; hence I is onto by FUNCT_2:def_3; ::_thesis: verum end; thus for x being Point of X for y being Point of Y holds I . (x,y) = [x,<*y*>] by A4; ::_thesis: ( ( 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.|| ) ) thus for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ::_thesis: ( ( 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 let v, w be Point of [:X,Y:]; ::_thesis: I . (v + w) = (I . v) + (I . w) consider x1 being Point of X, x2 being Point of Y such that A12: v = [x1,x2] by Lm1; consider y1 being Point of X, y2 being Point of Y such that A13: w = [y1,y2] by Lm1; A14: I . (v + w) = I . ((x1 + y1),(x2 + y2)) by A12, A13, Def1 .= [(x1 + y1),<*(x2 + y2)*>] by A4 ; ( I . v = I . (x1,x2) & I . w = I . (y1,y2) ) by A12, A13; then A15: ( I . v = [x1,<*x2*>] & I . w = [y1,<*y2*>] ) by A4; A16: ( J . x2 = <*x2*> & J . y2 = <*y2*> ) by A1; then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ; reconsider yy2 = <*y2*> as Point of (product <*Y*>) by A16; <*(x2 + y2)*> = J . (x2 + y2) by A1 .= xx2 + yy2 by A16, A1 ; hence (I . v) + (I . w) = I . (v + w) by A14, A15, Def1; ::_thesis: verum end; thus for v being Point of [:X,Y:] for r being Element of REAL holds I . (r * v) = r * (I . v) ::_thesis: ( I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) ) proof let v be Point of [:X,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) consider x1 being Point of X, x2 being Point of Y such that A17: v = [x1,x2] by Lm1; A18: I . (r * v) = I . ((r * x1),(r * x2)) by A17, Th18 .= [(r * x1),<*(r * x2)*>] by A4 ; A19: I . v = I . (x1,x2) by A17 .= [x1,<*x2*>] by A4 ; A20: J . x2 = <*x2*> by A1; then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ; <*(r * x2)*> = J . (r * x2) by A1 .= r * xx2 by A20, A1 ; hence r * (I . v) = I . (r * v) by A18, A19, Th18; ::_thesis: verum end; A21: <*(0. Y)*> = 0. (product <*Y*>) by A1; I . (0. [:X,Y:]) = I . ((0. X),(0. Y)) ; hence I . (0. [:X,Y:]) = 0. [:X,(product <*Y*>):] by A21, A4; ::_thesis: for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| thus for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ::_thesis: verum proof let v be Point of [:X,Y:]; ::_thesis: ||.(I . v).|| = ||.v.|| consider x1 being Point of X, x2 being Point of Y such that A22: v = [x1,x2] by Lm1; A23: J . x2 = <*x2*> by A1; then reconsider xx2 = <*x2*> as Point of (product <*Y*>) ; A24: ex w being Element of REAL 2 st ( w = <*||.x1.||,||.x2.||*> & ||.v.|| = |.w.| ) by A22, Th18; I . v = I . (x1,x2) by A22 .= [x1,<*x2*>] by A4 ; then ex s being Element of REAL 2 st ( s = <*||.x1.||,||.xx2.||*> & ||.(I . v).|| = |.s.| ) by Th18; hence ||.(I . v).|| = ||.v.|| by A23, A1, A24; ::_thesis: verum end; 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 let X be RealNormSpace-Sequence; ::_thesis: 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.|| ) ) let Y be RealNormSpace; ::_thesis: 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.|| ) ) consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that A1: ( I is one-to-one & I is onto & ( for x being Point of (product X) for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( 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),(product <*Y*>):] & ( for v being Point of [:(product X),Y:] holds ||.(I . v).|| = ||.v.|| ) ) by Th23; consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*Y*>)) such that A2: ( J is one-to-one & J 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 & J . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product <*Y*>):] holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of [:(product X),(product <*Y*>):] for r being Element of REAL holds J . (r * v) = r * (J . v) ) & J . (0. [:(product X),(product <*Y*>):]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),(product <*Y*>):] holds ||.(J . v).|| = ||.v.|| ) ) by Th17; set K = J * I; reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ; take K ; ::_thesis: ( K is one-to-one & K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) ) thus K is one-to-one by A1, A2; ::_thesis: ( K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) ) A3: rng J = the carrier of (product (X ^ <*Y*>)) by A2, FUNCT_2:def_3; rng I = the carrier of [:(product X),(product <*Y*>):] by A1, FUNCT_2:def_3; then rng (J * I) = J .: the carrier of [:(product X),(product <*Y*>):] by RELAT_1:127 .= the carrier of (product (X ^ <*Y*>)) by A3, RELSET_1:22 ; hence K is onto by FUNCT_2:def_3; ::_thesis: ( ( for x being Point of (product X) for y being Point of Y ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) ) thus for x being Point of (product X) for y being Point of Y ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ::_thesis: ( ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) ) proof let x be Point of (product X); ::_thesis: for y being Point of Y ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) let y be Point of Y; ::_thesis: ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) A4: I . (x,y) = [x,<*y*>] by A1; [x,y] in the carrier of [:(product X),Y:] ; then [x,<*y*>] in the carrier of [:(product X),(product <*Y*>):] by A4, FUNCT_2:5; then reconsider yy = <*y*> as Point of (product <*Y*>) by ZFMISC_1:87; consider x1, y1 being FinSequence such that A5: ( x = x1 & yy = y1 & J . (x,yy) = x1 ^ y1 ) by A2; J . (x,yy) = J . (I . [x,y]) by A4 .= K . (x,y) by FUNCT_2:15 ; hence ex x1, y1 being FinSequence st ( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) by A5; ::_thesis: verum end; thus for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ::_thesis: ( ( for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) ) proof let v, w be Point of [:(product X),Y:]; ::_thesis: K . (v + w) = (K . v) + (K . w) thus K . (v + w) = J . (I . (v + w)) by FUNCT_2:15 .= J . ((I . v) + (I . w)) by A1 .= (J . (I . v)) + (J . (I . w)) by A2 .= (K . v) + (J . (I . w)) by FUNCT_2:15 .= (K . v) + (K . w) by FUNCT_2:15 ; ::_thesis: verum end; thus for v being Point of [:(product X),Y:] for r being Element of REAL holds K . (r * v) = r * (K . v) ::_thesis: ( K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) ) proof let v be Point of [:(product X),Y:]; ::_thesis: for r being Element of REAL holds K . (r * v) = r * (K . v) let r be Element of REAL ; ::_thesis: K . (r * v) = r * (K . v) thus K . (r * v) = J . (I . (r * v)) by FUNCT_2:15 .= J . (r * (I . v)) by A1 .= r * (J . (I . v)) by A2 .= r * (K . v) by FUNCT_2:15 ; ::_thesis: verum end; thus K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) by A1, A2, FUNCT_2:15; ::_thesis: for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| thus for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ::_thesis: verum proof let v be Point of [:(product X),Y:]; ::_thesis: ||.(K . v).|| = ||.v.|| thus ||.(K . v).|| = ||.(J . (I . v)).|| by FUNCT_2:15 .= ||.(I . v).|| by A2 .= ||.v.|| by A1 ; ::_thesis: verum end; end;