:: PRVECT_2 semantic presentation begin theorem :: PRVECT_2:1 for s, t being Real_Sequence for g being real number st ( for n being Element of NAT holds t . n = abs ((s . n) - g) ) holds ( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) ) proof let s, t be Real_Sequence; ::_thesis: for g being real number st ( for n being Element of NAT holds t . n = abs ((s . n) - g) ) holds ( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) ) let g be real number ; ::_thesis: ( ( for n being Element of NAT holds t . n = abs ((s . n) - g) ) implies ( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) ) ) assume A1: for n being Element of NAT holds t . n = abs ((s . n) - g) ; ::_thesis: ( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) ) hereby ::_thesis: ( t is convergent & lim t = 0 implies ( s is convergent & lim s = g ) ) assume A2: ( s is convergent & lim s = g ) ; ::_thesis: ( t is convergent & lim t = 0 ) A3: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((t_._m)_-_0)_<_r let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((t . m) - 0) < r ) assume 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((t . m) - 0) < r then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds abs ((s . m) - g) < r by A2, SEQ_2:def_7; take n = n; ::_thesis: for m being Element of NAT st n <= m holds abs ((t . m) - 0) < r now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((t_._m)_-_0)_<_r let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((t . m) - 0) < r ) assume n <= m ; ::_thesis: abs ((t . m) - 0) < r then abs (abs ((s . m) - g)) < r by A4; hence abs ((t . m) - 0) < r by A1; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds abs ((t . m) - 0) < r ; ::_thesis: verum end; hence t is convergent by SEQ_2:def_6; ::_thesis: lim t = 0 hence lim t = 0 by A3, SEQ_2:def_7; ::_thesis: verum end; assume A5: ( t is convergent & lim t = 0 ) ; ::_thesis: ( s is convergent & lim s = g ) A6: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((s_._m)_-_g)_<_r let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((s . m) - g) < r ) assume 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((s . m) - g) < r then consider n being Element of NAT such that A7: for m being Element of NAT st n <= m holds abs ((t . m) - 0) < r by A5, SEQ_2:def_7; take n = n; ::_thesis: for m being Element of NAT st n <= m holds abs ((s . m) - g) < r now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((s_._m)_-_g)_<_r let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((s . m) - g) < r ) assume n <= m ; ::_thesis: abs ((s . m) - g) < r then abs ((t . m) - 0) < r by A7; then abs (abs ((s . m) - g)) < r by A1; hence abs ((s . m) - g) < r ; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds abs ((s . m) - g) < r ; ::_thesis: verum end; hence s is convergent by SEQ_2:def_6; ::_thesis: lim s = g hence lim s = g by A6, SEQ_2:def_7; ::_thesis: verum end; theorem Th2: :: PRVECT_2:2 for x, y being FinSequence of REAL st len x = len y & ( for i being Element of NAT st i in Seg (len x) holds ( 0 <= x . i & x . i <= y . i ) ) holds |.x.| <= |.y.| proof let x, y be FinSequence of REAL ; ::_thesis: ( len x = len y & ( for i being Element of NAT st i in Seg (len x) holds ( 0 <= x . i & x . i <= y . i ) ) implies |.x.| <= |.y.| ) assume that A1: len x = len y and A2: for i being Element of NAT st i in Seg (len x) holds ( 0 <= x . i & x . i <= y . i ) ; ::_thesis: |.x.| <= |.y.| A3: for i being Nat st i in Seg (len x) holds (sqr x) . i <= (sqr y) . i proof let i be Nat; ::_thesis: ( i in Seg (len x) implies (sqr x) . i <= (sqr y) . i ) assume i in Seg (len x) ; ::_thesis: (sqr x) . i <= (sqr y) . i then A4: ( 0 <= x . i & x . i <= y . i ) by A2; ( (x . i) ^2 = (sqr x) . i & (y . i) ^2 = (sqr y) . i ) by VALUED_1:11; hence (sqr x) . i <= (sqr y) . i by A4, SQUARE_1:15; ::_thesis: verum end; ( Seg (len (sqr y)) = dom (sqr y) & dom (sqr y) = dom y ) by FINSEQ_1:def_3, VALUED_1:11; then A5: len (sqr y) = len y by FINSEQ_1:def_3; ( Seg (len (sqr x)) = dom (sqr x) & dom (sqr x) = dom x ) by FINSEQ_1:def_3, VALUED_1:11; then A6: len (sqr x) = len x by FINSEQ_1:def_3; A7: 0 <= Sum (sqr x) by RVSUM_1:86; ( sqr x is Element of (len (sqr x)) -tuples_on REAL & sqr y is Element of (len (sqr y)) -tuples_on REAL ) by FINSEQ_2:92; hence |.x.| <= |.y.| by A1, A3, A6, A5, A7, RVSUM_1:82, SQUARE_1:26; ::_thesis: verum end; theorem Th3: :: PRVECT_2:3 for F being FinSequence of REAL st ( for i being Element of NAT st i in dom F holds F . i = 0 ) holds Sum F = 0 proof let F be FinSequence of REAL ; ::_thesis: ( ( for i being Element of NAT st i in dom F holds F . i = 0 ) implies Sum F = 0 ) set i = len F; set R1 = (len F) |-> 0; reconsider R2 = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92; A1: Seg (len F) = dom F by FINSEQ_1:def_3; assume A2: for i being Element of NAT st i in dom F holds 0 = F . i ; ::_thesis: Sum F = 0 A3: for j being Nat st j in Seg (len F) holds ((len F) |-> 0) . j = R2 . j by A2, A1; len ((len F) |-> 0) = len F by CARD_1:def_7; then dom ((len F) |-> 0) = dom R2 by FINSEQ_3:29; then (len F) |-> 0 = R2 by A1, A3, FINSEQ_1:13; hence Sum F = 0 by RVSUM_1:81; ::_thesis: verum end; definition let f be Function; let X be set ; mode MultOps of X,f -> Function means :Def1: :: PRVECT_2:def 1 ( dom it = dom f & ( for i being set st i in dom f holds it . i is Function of [:X,(f . i):],(f . i) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for i being set st i in dom f holds b1 . i is Function of [:X,(f . i):],(f . i) ) ) proof deffunc H1( set ) -> Element of bool [:[:X,(f . $1):],(f . $1):] = pr2 (X,(f . $1)); consider g being Function such that A1: ( dom g = dom f & ( for x being set st x in dom f holds g . x = H1(x) ) ) from FUNCT_1:sch_3(); take g ; ::_thesis: ( dom g = dom f & ( for i being set st i in dom f holds g . i is Function of [:X,(f . i):],(f . i) ) ) thus dom g = dom f by A1; ::_thesis: for i being set st i in dom f holds g . i is Function of [:X,(f . i):],(f . i) let i be set ; ::_thesis: ( i in dom f implies g . i is Function of [:X,(f . i):],(f . i) ) assume i in dom f ; ::_thesis: g . i is Function of [:X,(f . i):],(f . i) then g . i = pr2 (X,(f . i)) by A1; hence g . i is Function of [:X,(f . i):],(f . i) ; ::_thesis: verum end; end; :: deftheorem Def1 defines MultOps PRVECT_2:def_1_:_ for f being Function for X being set for b3 being Function holds ( b3 is MultOps of X,f iff ( dom b3 = dom f & ( for i being set st i in dom f holds b3 . i is Function of [:X,(f . i):],(f . i) ) ) ); registration let F be Domain-Sequence; let X be set ; cluster -> FinSequence-like for MultOps of X,F; coherence for b1 being MultOps of X,F holds b1 is FinSequence-like proof let f be MultOps of X,F; ::_thesis: f is FinSequence-like ( dom F = dom f & dom F = Seg (len F) ) by Def1, FINSEQ_1:def_3; hence f is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum end; end; theorem Th4: :: PRVECT_2:4 for X being set for F being Domain-Sequence for p being FinSequence holds ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds p . i is Function of [:X,(F . i):],(F . i) ) ) ) proof let X be set ; ::_thesis: for F being Domain-Sequence for p being FinSequence holds ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds p . i is Function of [:X,(F . i):],(F . i) ) ) ) let F be Domain-Sequence; ::_thesis: for p being FinSequence holds ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds p . i is Function of [:X,(F . i):],(F . i) ) ) ) let p be FinSequence; ::_thesis: ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds p . i is Function of [:X,(F . i):],(F . i) ) ) ) ( dom p = dom F iff len p = len F ) by FINSEQ_3:29; hence ( p is MultOps of X,F iff ( len p = len F & ( for i being set st i in dom F holds p . i is Function of [:X,(F . i):],(F . i) ) ) ) by Def1; ::_thesis: verum end; definition let F be Domain-Sequence; let X be set ; let p be MultOps of X,F; let i be Element of dom F; :: original: . redefine funcp . i -> Function of [:X,(F . i):],(F . i); coherence p . i is Function of [:X,(F . i):],(F . i) by Th4; end; theorem Th5: :: PRVECT_2:5 for X being non empty set for F being Domain-Sequence for f, g being Function of [:X,(product F):],(product F) st ( for x being Element of X for d being Element of product F for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ) holds f = g proof let X be non empty set ; ::_thesis: for F being Domain-Sequence for f, g being Function of [:X,(product F):],(product F) st ( for x being Element of X for d being Element of product F for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ) holds f = g let F be Domain-Sequence; ::_thesis: for f, g being Function of [:X,(product F):],(product F) st ( for x being Element of X for d being Element of product F for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ) holds f = g let f, g be Function of [:X,(product F):],(product F); ::_thesis: ( ( for x being Element of X for d being Element of product F for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ) implies f = g ) assume A1: for x being Element of X for d being Element of product F for i being Element of dom F holds (f . (x,d)) . i = (g . (x,d)) . i ; ::_thesis: f = g now__::_thesis:_for_x_being_Element_of_X for_d_being_Element_of_product_F_holds_f_._(x,d)_=_g_._(x,d) let x be Element of X; ::_thesis: for d being Element of product F holds f . (x,d) = g . (x,d) let d be Element of product F; ::_thesis: f . (x,d) = g . (x,d) A2: ( dom (f . (x,d)) = dom F & dom (g . (x,d)) = dom F ) by CARD_3:9; for v being set st v in dom F holds (f . (x,d)) . v = (g . (x,d)) . v by A1; hence f . (x,d) = g . (x,d) by A2, FUNCT_1:2; ::_thesis: verum end; hence f = g by BINOP_1:2; ::_thesis: verum end; definition let F be Domain-Sequence; let X be non empty set ; let p be MultOps of X,F; func[:p:] -> Function of [:X,(product F):],(product F) means :Def2: :: PRVECT_2:def 2 for x being Element of X for d being Element of product F for i being Element of dom F holds (it . (x,d)) . i = (p . i) . (x,(d . i)); existence ex b1 being Function of [:X,(product F):],(product F) st for x being Element of X for d being Element of product F for i being Element of dom F holds (b1 . (x,d)) . i = (p . i) . (x,(d . i)) proof defpred S1[ Element of X, Element of product F, Element of product F] means for i being Element of dom F holds $3 . i = (p . i) . ($1,($2 . i)); A1: for x being Element of X for d being Element of product F ex z being Element of product F st S1[x,d,z] proof let x be Element of X; ::_thesis: for d being Element of product F ex z being Element of product F st S1[x,d,z] let d be Element of product F; ::_thesis: ex z being Element of product F st S1[x,d,z] defpred S2[ set , set ] means ex i being Element of dom F st ( $1 = i & $2 = (p . i) . (x,(d . i)) ); A2: for w being set st w in dom F holds ex z being set st S2[w,z] proof let w be set ; ::_thesis: ( w in dom F implies ex z being set st S2[w,z] ) assume w in dom F ; ::_thesis: ex z being set st S2[w,z] then reconsider i = w as Element of dom F ; take (p . i) . (x,(d . i)) ; ::_thesis: S2[w,(p . i) . (x,(d . i))] thus S2[w,(p . i) . (x,(d . i))] ; ::_thesis: verum end; consider z being Function such that A3: ( dom z = dom F & ( for w being set st w in dom F holds S2[w,z . w] ) ) from CLASSES1:sch_1(A2); now__::_thesis:_for_w_being_set_st_w_in_dom_F_holds_ z_._w_in_F_._w let w be set ; ::_thesis: ( w in dom F implies z . w in F . w ) assume w in dom F ; ::_thesis: z . w in F . w then ex i being Element of dom F st ( w = i & z . w = (p . i) . (x,(d . i)) ) by A3; hence z . w in F . w ; ::_thesis: verum end; then reconsider z9 = z as Element of product F by A3, CARD_3:9; take z9 ; ::_thesis: S1[x,d,z9] let i be Element of dom F; ::_thesis: z9 . i = (p . i) . (x,(d . i)) ex j being Element of dom F st ( j = i & z . i = (p . j) . (x,(d . j)) ) by A3; hence z9 . i = (p . i) . (x,(d . i)) ; ::_thesis: verum end; thus ex P being Function of [:X,(product F):],(product F) st for x being Element of X for d being Element of product F holds S1[x,d,P . (x,d)] from BINOP_1:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being Function of [:X,(product F):],(product F) st ( for x being Element of X for d being Element of product F for i being Element of dom F holds (b1 . (x,d)) . i = (p . i) . (x,(d . i)) ) & ( for x being Element of X for d being Element of product F for i being Element of dom F holds (b2 . (x,d)) . i = (p . i) . (x,(d . i)) ) holds b1 = b2 proof let P, Q be Function of [:X,(product F):],(product F); ::_thesis: ( ( for x being Element of X for d being Element of product F for i being Element of dom F holds (P . (x,d)) . i = (p . i) . (x,(d . i)) ) & ( for x being Element of X for d being Element of product F for i being Element of dom F holds (Q . (x,d)) . i = (p . i) . (x,(d . i)) ) implies P = Q ) assume that A4: for x being Element of X for f being Element of product F for i being Element of dom F holds (P . (x,f)) . i = (p . i) . (x,(f . i)) and A5: for x being Element of X for f being Element of product F for i being Element of dom F holds (Q . (x,f)) . i = (p . i) . (x,(f . i)) ; ::_thesis: P = Q now__::_thesis:_for_x_being_Element_of_X for_f_being_Element_of_product_F for_i_being_Element_of_dom_F_holds_(P_._(x,f))_._i_=_(Q_._(x,f))_._i let x be Element of X; ::_thesis: for f being Element of product F for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . i let f be Element of product F; ::_thesis: for i being Element of dom F holds (P . (x,f)) . i = (Q . (x,f)) . i let i be Element of dom F; ::_thesis: (P . (x,f)) . i = (Q . (x,f)) . i (P . (x,f)) . i = (p . i) . (x,(f . i)) by A4; hence (P . (x,f)) . i = (Q . (x,f)) . i by A5; ::_thesis: verum end; hence P = Q by Th5; ::_thesis: verum end; end; :: deftheorem Def2 defines [: PRVECT_2:def_2_:_ for F being Domain-Sequence for X being non empty set for p being MultOps of X,F for b4 being Function of [:X,(product F):],(product F) holds ( b4 = [:p:] iff for x being Element of X for d being Element of product F for i being Element of dom F holds (b4 . (x,d)) . i = (p . i) . (x,(d . i)) ); definition let R be Relation; attrR is RealLinearSpace-yielding means :Def3: :: PRVECT_2:def 3 for S being set st S in rng R holds S is RealLinearSpace; end; :: deftheorem Def3 defines RealLinearSpace-yielding PRVECT_2:def_3_:_ for R being Relation holds ( R is RealLinearSpace-yielding iff for S being set st S in rng R holds S is RealLinearSpace ); registration cluster Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable RealLinearSpace-yielding for set ; existence ex b1 being FinSequence st ( not b1 is empty & b1 is RealLinearSpace-yielding ) proof set S = the RealLinearSpace; take <* the RealLinearSpace*> ; ::_thesis: ( not <* the RealLinearSpace*> is empty & <* the RealLinearSpace*> is RealLinearSpace-yielding ) thus not <* the RealLinearSpace*> is empty ; ::_thesis: <* the RealLinearSpace*> is RealLinearSpace-yielding let x be set ; :: according to PRVECT_2:def_3 ::_thesis: ( x in rng <* the RealLinearSpace*> implies x is RealLinearSpace ) assume that A1: x in rng <* the RealLinearSpace*> and A2: x is not RealLinearSpace ; ::_thesis: contradiction x in { the RealLinearSpace} by A1, FINSEQ_1:38; hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; end; definition mode RealLinearSpace-Sequence is non empty RealLinearSpace-yielding FinSequence; end; definition let G be RealLinearSpace-Sequence; let j be Element of dom G; :: original: . redefine funcG . j -> RealLinearSpace; coherence G . j is RealLinearSpace proof G . j in rng G by FUNCT_1:def_3; hence G . j is RealLinearSpace by Def3; ::_thesis: verum end; end; definition let G be RealLinearSpace-Sequence; func carr G -> Domain-Sequence means :Def4: :: PRVECT_2:def 4 ( len it = len G & ( for j being Element of dom G holds it . j = the carrier of (G . j) ) ); existence ex b1 being Domain-Sequence st ( len b1 = len G & ( for j being Element of dom G holds b1 . j = the carrier of (G . j) ) ) proof defpred S1[ set , set ] means ex j9 being Element of dom G st ( j9 = $1 & $2 = the carrier of (G . j9) ); A1: for j being Nat st j in Seg (len G) holds ex x being set st S1[j,x] proof let j be Nat; ::_thesis: ( j in Seg (len G) implies ex x being set st S1[j,x] ) assume j in Seg (len G) ; ::_thesis: ex x being set st S1[j,x] then reconsider j9 = j as Element of dom G by FINSEQ_1:def_3; take the carrier of (G . j9) ; ::_thesis: S1[j, the carrier of (G . j9)] thus S1[j, the carrier of (G . j9)] ; ::_thesis: verum end; consider p being FinSequence such that A2: ( dom p = Seg (len G) & ( for j being Nat st j in Seg (len G) holds S1[j,p . j] ) ) from FINSEQ_1:sch_1(A1); now__::_thesis:_not_{}_in_rng_p assume {} in rng p ; ::_thesis: contradiction then consider x being set such that A3: x in dom p and A4: {} = p . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A3; ex x9 being Element of dom G st ( x9 = x & p . x = the carrier of (G . x9) ) by A2, A3; hence contradiction by A4; ::_thesis: verum end; then reconsider q = p as Domain-Sequence by A2, RELAT_1:def_9; take q ; ::_thesis: ( len q = len G & ( for j being Element of dom G holds q . j = the carrier of (G . j) ) ) thus len q = len G by A2, FINSEQ_1:def_3; ::_thesis: for j being Element of dom G holds q . j = the carrier of (G . j) let j be Element of dom G; ::_thesis: q . j = the carrier of (G . j) reconsider k = j as Element of NAT ; dom G = Seg (len G) by FINSEQ_1:def_3; then ex n being Element of dom G st ( n = k & q . k = the carrier of (G . n) ) by A2; hence q . j = the carrier of (G . j) ; ::_thesis: verum end; uniqueness for b1, b2 being Domain-Sequence st len b1 = len G & ( for j being Element of dom G holds b1 . j = the carrier of (G . j) ) & len b2 = len G & ( for j being Element of dom G holds b2 . j = the carrier of (G . j) ) holds b1 = b2 proof let f, h be Domain-Sequence; ::_thesis: ( len f = len G & ( for j being Element of dom G holds f . j = the carrier of (G . j) ) & len h = len G & ( for j being Element of dom G holds h . j = the carrier of (G . j) ) implies f = h ) assume that A5: len f = len G and A6: for j being Element of dom G holds f . j = the carrier of (G . j) and A7: len h = len G and A8: for j being Element of dom G holds h . j = the carrier of (G . j) ; ::_thesis: f = h reconsider f9 = f, h9 = h as FinSequence ; A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_f9_holds_ f9_._j_=_h9_._j let j be Nat; ::_thesis: ( j in dom f9 implies f9 . j = h9 . j ) assume j in dom f9 ; ::_thesis: f9 . j = h9 . j then reconsider j9 = j as Element of dom G by A5, FINSEQ_3:29; f9 . j = the carrier of (G . j9) by A6; hence f9 . j = h9 . j by A8; ::_thesis: verum end; ( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3; hence f = h by A5, A7, A9, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def4 defines carr PRVECT_2:def_4_:_ for G being RealLinearSpace-Sequence for b2 being Domain-Sequence holds ( b2 = carr G iff ( len b2 = len G & ( for j being Element of dom G holds b2 . j = the carrier of (G . j) ) ) ); definition let G be RealLinearSpace-Sequence; let j be Element of dom (carr G); :: original: . redefine funcG . j -> RealLinearSpace; coherence G . j is RealLinearSpace proof ( dom G = Seg (len G) & Seg (len (carr G)) = dom (carr G) ) by FINSEQ_1:def_3; then reconsider j9 = j as Element of dom G by Def4; G . j9 is RealLinearSpace ; hence G . j is RealLinearSpace ; ::_thesis: verum end; end; definition let G be RealLinearSpace-Sequence; func addop G -> BinOps of carr G means :Def5: :: PRVECT_2:def 5 ( len it = len (carr G) & ( for j being Element of dom (carr G) holds it . j = the addF of (G . j) ) ); existence ex b1 being BinOps of carr G st ( len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = the addF of (G . j) ) ) proof deffunc H1( Element of dom (carr G)) -> Element of bool [:[: the carrier of (G . $1), the carrier of (G . $1):], the carrier of (G . $1):] = the addF of (G . $1); consider p being non empty FinSequence such that A1: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H1(j) ) ) from PRVECT_1:sch_1(); now__::_thesis:_for_j_being_Element_of_dom_(carr_G)_holds_p_._j_is_BinOp_of_((carr_G)_._j) let j be Element of dom (carr G); ::_thesis: p . j is BinOp of ((carr G) . j) len G = len (carr G) by Def4; then reconsider k = j as Element of dom G by FINSEQ_3:29; ( p . j = the addF of (G . j) & the carrier of (G . k) = (carr G) . k ) by A1, Def4; hence p . j is BinOp of ((carr G) . j) ; ::_thesis: verum end; then reconsider p9 = p as BinOps of carr G by A1, PRVECT_1:11; take p9 ; ::_thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the addF of (G . j) ) ) thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the addF of (G . j) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being BinOps of carr G st len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = the addF of (G . j) ) & len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the addF of (G . j) ) holds b1 = b2 proof let f, h be BinOps of carr G; ::_thesis: ( len f = len (carr G) & ( for j being Element of dom (carr G) holds f . j = the addF of (G . j) ) & len h = len (carr G) & ( for j being Element of dom (carr G) holds h . j = the addF of (G . j) ) implies f = h ) assume that A2: len f = len (carr G) and A3: for j being Element of dom (carr G) holds f . j = the addF of (G . j) and A4: len h = len (carr G) and A5: for j being Element of dom (carr G) holds h . j = the addF of (G . j) ; ::_thesis: f = h reconsider f9 = f, h9 = h as FinSequence ; A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_ f9_._i_=_h9_._i let i be Nat; ::_thesis: ( i in dom f9 implies f9 . i = h9 . i ) assume i in dom f9 ; ::_thesis: f9 . i = h9 . i then reconsider i9 = i as Element of dom (carr G) by A2, FINSEQ_3:29; f9 . i = the addF of (G . i9) by A3; hence f9 . i = h9 . i by A5; ::_thesis: verum end; ( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3; hence f = h by A2, A4, A6, FINSEQ_1:13; ::_thesis: verum end; func complop G -> UnOps of carr G means :Def6: :: PRVECT_2:def 6 ( len it = len (carr G) & ( for j being Element of dom (carr G) holds it . j = comp (G . j) ) ); existence ex b1 being UnOps of carr G st ( len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = comp (G . j) ) ) proof deffunc H1( Element of dom (carr G)) -> Element of bool [: the carrier of (G . $1), the carrier of (G . $1):] = comp (G . $1); consider p being non empty FinSequence such that A7: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H1(j) ) ) from PRVECT_1:sch_1(); now__::_thesis:_for_j_being_Element_of_dom_(carr_G)_holds_p_._j_is_UnOp_of_((carr_G)_._j) let j be Element of dom (carr G); ::_thesis: p . j is UnOp of ((carr G) . j) len G = len (carr G) by Def4; then reconsider k = j as Element of dom G by FINSEQ_3:29; ( p . j = comp (G . j) & the carrier of (G . k) = (carr G) . k ) by A7, Def4; hence p . j is UnOp of ((carr G) . j) ; ::_thesis: verum end; then reconsider p9 = p as UnOps of carr G by A7, PRVECT_1:12; take p9 ; ::_thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = comp (G . j) ) ) thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = comp (G . j) ) ) by A7; ::_thesis: verum end; uniqueness for b1, b2 being UnOps of carr G st len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = comp (G . j) ) & len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = comp (G . j) ) holds b1 = b2 proof let f, h be UnOps of carr G; ::_thesis: ( len f = len (carr G) & ( for j being Element of dom (carr G) holds f . j = comp (G . j) ) & len h = len (carr G) & ( for j being Element of dom (carr G) holds h . j = comp (G . j) ) implies f = h ) assume that A8: len f = len (carr G) and A9: for j being Element of dom (carr G) holds f . j = comp (G . j) and A10: len h = len (carr G) and A11: for j being Element of dom (carr G) holds h . j = comp (G . j) ; ::_thesis: f = h reconsider f9 = f, h9 = h as FinSequence ; A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_ f_._i_=_h_._i let i be Nat; ::_thesis: ( i in dom f9 implies f . i = h . i ) assume i in dom f9 ; ::_thesis: f . i = h . i then reconsider i9 = i as Element of dom (carr G) by A8, FINSEQ_3:29; f . i = comp (G . i9) by A9; hence f . i = h . i by A11; ::_thesis: verum end; ( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3; hence f = h by A8, A10, A12, FINSEQ_1:13; ::_thesis: verum end; func zeros G -> Element of product (carr G) means :Def7: :: PRVECT_2:def 7 for j being Element of dom (carr G) holds it . j = the ZeroF of (G . j); existence ex b1 being Element of product (carr G) st for j being Element of dom (carr G) holds b1 . j = the ZeroF of (G . j) proof deffunc H1( Element of dom (carr G)) -> Element of the carrier of (G . $1) = the ZeroF of (G . $1); consider p being non empty FinSequence such that A13: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H1(j) ) ) from PRVECT_1:sch_1(); A14: dom (carr G) = Seg (len (carr G)) by FINSEQ_1:def_3; A15: dom G = Seg (len G) by FINSEQ_1:def_3; A16: now__::_thesis:_for_i_being_set_st_i_in_dom_(carr_G)_holds_ p_._i_in_(carr_G)_._i let i be set ; ::_thesis: ( i in dom (carr G) implies p . i in (carr G) . i ) assume i in dom (carr G) ; ::_thesis: p . i in (carr G) . i then reconsider x = i as Element of dom (carr G) ; reconsider x9 = x as Element of dom G by A15, A14, Def4; ( p . x = the ZeroF of (G . x) & (carr G) . x9 = the carrier of (G . x9) ) by A13, Def4; hence p . i in (carr G) . i ; ::_thesis: verum end; dom p = Seg (len p) by FINSEQ_1:def_3; then reconsider t = p as Element of product (carr G) by A13, A14, A16, CARD_3:9; take t ; ::_thesis: for j being Element of dom (carr G) holds t . j = the ZeroF of (G . j) thus for j being Element of dom (carr G) holds t . j = the ZeroF of (G . j) by A13; ::_thesis: verum end; uniqueness for b1, b2 being Element of product (carr G) st ( for j being Element of dom (carr G) holds b1 . j = the ZeroF of (G . j) ) & ( for j being Element of dom (carr G) holds b2 . j = the ZeroF of (G . j) ) holds b1 = b2 proof let f, h be Element of product (carr G); ::_thesis: ( ( for j being Element of dom (carr G) holds f . j = the ZeroF of (G . j) ) & ( for j being Element of dom (carr G) holds h . j = the ZeroF of (G . j) ) implies f = h ) assume that A17: for j being Element of dom (carr G) holds f . j = the ZeroF of (G . j) and A18: for j being Element of dom (carr G) holds h . j = the ZeroF of (G . j) ; ::_thesis: f = h reconsider f9 = f, h9 = h as Function ; A19: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_ f9_._x_=_h9_._x let x be set ; ::_thesis: ( x in dom (carr G) implies f9 . x = h9 . x ) assume x in dom (carr G) ; ::_thesis: f9 . x = h9 . x then reconsider i = x as Element of dom (carr G) ; thus f9 . x = the ZeroF of (G . i) by A17 .= h9 . x by A18 ; ::_thesis: verum end; ( dom f9 = dom (carr G) & dom h9 = dom (carr G) ) by CARD_3:9; hence f = h by A19, FUNCT_1:2; ::_thesis: verum end; func multop G -> MultOps of REAL , carr G means :Def8: :: PRVECT_2:def 8 ( len it = len (carr G) & ( for j being Element of dom (carr G) holds it . j = the Mult of (G . j) ) ); existence ex b1 being MultOps of REAL , carr G st ( len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = the Mult of (G . j) ) ) proof deffunc H1( Element of dom (carr G)) -> Element of bool [:[:REAL, the carrier of (G . $1):], the carrier of (G . $1):] = the Mult of (G . $1); consider p being non empty FinSequence such that A20: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H1(j) ) ) from PRVECT_1:sch_1(); now__::_thesis:_for_ai_being_set_st_ai_in_dom_(carr_G)_holds_ p_._ai_is_Function_of_[:REAL,((carr_G)_._ai):],((carr_G)_._ai) let ai be set ; ::_thesis: ( ai in dom (carr G) implies p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai) ) assume ai in dom (carr G) ; ::_thesis: p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai) then reconsider i = ai as Element of dom (carr G) ; len G = len (carr G) by Def4; then reconsider j = i as Element of dom G by FINSEQ_3:29; ( p . i = the Mult of (G . i) & the carrier of (G . j) = (carr G) . j ) by A20, Def4; hence p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai) ; ::_thesis: verum end; then reconsider p9 = p as MultOps of REAL , carr G by A20, Th4; take p9 ; ::_thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the Mult of (G . j) ) ) thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the Mult of (G . j) ) ) by A20; ::_thesis: verum end; uniqueness for b1, b2 being MultOps of REAL , carr G st len b1 = len (carr G) & ( for j being Element of dom (carr G) holds b1 . j = the Mult of (G . j) ) & len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the Mult of (G . j) ) holds b1 = b2 proof let f, h be MultOps of REAL , carr G; ::_thesis: ( len f = len (carr G) & ( for j being Element of dom (carr G) holds f . j = the Mult of (G . j) ) & len h = len (carr G) & ( for j being Element of dom (carr G) holds h . j = the Mult of (G . j) ) implies f = h ) assume that A21: len f = len (carr G) and A22: for j being Element of dom (carr G) holds f . j = the Mult of (G . j) and A23: len h = len (carr G) and A24: for j being Element of dom (carr G) holds h . j = the Mult of (G . j) ; ::_thesis: f = h reconsider f9 = f, h9 = h as FinSequence ; A25: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_ f9_._i_=_h9_._i let i be Nat; ::_thesis: ( i in dom f9 implies f9 . i = h9 . i ) assume i in dom f9 ; ::_thesis: f9 . i = h9 . i then reconsider i9 = i as Element of dom (carr G) by A21, FINSEQ_3:29; f9 . i = the Mult of (G . i9) by A22; hence f9 . i = h9 . i by A24; ::_thesis: verum end; ( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3; hence f = h by A21, A23, A25, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def5 defines addop PRVECT_2:def_5_:_ for G being RealLinearSpace-Sequence for b2 being BinOps of carr G holds ( b2 = addop G iff ( len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the addF of (G . j) ) ) ); :: deftheorem Def6 defines complop PRVECT_2:def_6_:_ for G being RealLinearSpace-Sequence for b2 being UnOps of carr G holds ( b2 = complop G iff ( len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = comp (G . j) ) ) ); :: deftheorem Def7 defines zeros PRVECT_2:def_7_:_ for G being RealLinearSpace-Sequence for b2 being Element of product (carr G) holds ( b2 = zeros G iff for j being Element of dom (carr G) holds b2 . j = the ZeroF of (G . j) ); :: deftheorem Def8 defines multop PRVECT_2:def_8_:_ for G being RealLinearSpace-Sequence for b2 being MultOps of REAL , carr G holds ( b2 = multop G iff ( len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the Mult of (G . j) ) ) ); definition let G be RealLinearSpace-Sequence; func product G -> non empty strict RLSStruct equals :: PRVECT_2:def 9 RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #); coherence RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) is non empty strict RLSStruct ; end; :: deftheorem defines product PRVECT_2:def_9_:_ for G being RealLinearSpace-Sequence holds product G = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #); Lm1: for LS being non empty addLoopStr st the addF of LS is commutative & the addF of LS is associative holds ( LS is Abelian & LS is add-associative ) proof deffunc H1( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1; let LS be non empty addLoopStr ; ::_thesis: ( the addF of LS is commutative & the addF of LS is associative implies ( LS is Abelian & LS is add-associative ) ) assume that A1: H1(LS) is commutative and A2: H1(LS) is associative ; ::_thesis: ( LS is Abelian & LS is add-associative ) for x, y being Element of LS holds x + y = y + x by A1, BINOP_1:def_2; hence LS is Abelian by RLVECT_1:def_2; ::_thesis: LS is add-associative for x, y, z being Element of LS holds (x + y) + z = x + (y + z) by A2, BINOP_1:def_3; hence LS is add-associative by RLVECT_1:def_3; ::_thesis: verum end; Lm2: for LS being non empty addLoopStr st the ZeroF of LS is_a_unity_wrt the addF of LS holds LS is right_zeroed proof let LS be non empty addLoopStr ; ::_thesis: ( the ZeroF of LS is_a_unity_wrt the addF of LS implies LS is right_zeroed ) assume A1: the ZeroF of LS is_a_unity_wrt the addF of LS ; ::_thesis: LS is right_zeroed let x be Element of LS; :: according to RLVECT_1:def_4 ::_thesis: x + (0. LS) = x thus x + (0. LS) = x by A1, BINOP_1:3; ::_thesis: verum end; Lm3: for G being RealLinearSpace-Sequence for v1, w1 being Element of product (carr G) for i being Element of dom (carr G) holds ( ([:(addop G):] . (v1,w1)) . i = the addF of (G . i) . ((v1 . i),(w1 . i)) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds ([:(addop G):] . (v1,w1)) . i = vi + wi ) ) proof let G be RealLinearSpace-Sequence; ::_thesis: for v1, w1 being Element of product (carr G) for i being Element of dom (carr G) holds ( ([:(addop G):] . (v1,w1)) . i = the addF of (G . i) . ((v1 . i),(w1 . i)) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds ([:(addop G):] . (v1,w1)) . i = vi + wi ) ) let v1, w1 be Element of product (carr G); ::_thesis: for i being Element of dom (carr G) holds ( ([:(addop G):] . (v1,w1)) . i = the addF of (G . i) . ((v1 . i),(w1 . i)) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds ([:(addop G):] . (v1,w1)) . i = vi + wi ) ) let i be Element of dom (carr G); ::_thesis: ( ([:(addop G):] . (v1,w1)) . i = the addF of (G . i) . ((v1 . i),(w1 . i)) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds ([:(addop G):] . (v1,w1)) . i = vi + wi ) ) ([:(addop G):] . (v1,w1)) . i = ((addop G) . i) . ((v1 . i),(w1 . i)) by PRVECT_1:def_8; hence ( ([:(addop G):] . (v1,w1)) . i = the addF of (G . i) . ((v1 . i),(w1 . i)) & ( for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds ([:(addop G):] . (v1,w1)) . i = vi + wi ) ) by Def5; ::_thesis: verum end; Lm4: for G being RealLinearSpace-Sequence for r being Real for v being Element of product (carr G) for i being Element of dom (carr G) holds ( ([:(multop G):] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds ([:(multop G):] . (r,v)) . i = r * vi ) ) proof let G be RealLinearSpace-Sequence; ::_thesis: for r being Real for v being Element of product (carr G) for i being Element of dom (carr G) holds ( ([:(multop G):] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds ([:(multop G):] . (r,v)) . i = r * vi ) ) let r be Real; ::_thesis: for v being Element of product (carr G) for i being Element of dom (carr G) holds ( ([:(multop G):] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds ([:(multop G):] . (r,v)) . i = r * vi ) ) let v be Element of product (carr G); ::_thesis: for i being Element of dom (carr G) holds ( ([:(multop G):] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds ([:(multop G):] . (r,v)) . i = r * vi ) ) let i be Element of dom (carr G); ::_thesis: ( ([:(multop G):] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds ([:(multop G):] . (r,v)) . i = r * vi ) ) ([:(multop G):] . (r,v)) . i = ((multop G) . i) . (r,(v . i)) by Def2; hence ( ([:(multop G):] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds ([:(multop G):] . (r,v)) . i = r * vi ) ) by Def8; ::_thesis: verum end; Lm5: for G being RealLinearSpace-Sequence holds ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) proof deffunc H1( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1; let G be RealLinearSpace-Sequence; ::_thesis: ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) reconsider GS = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) as non empty RLSStruct ; dom G = Seg (len G) by FINSEQ_1:def_3; then dom G = Seg (len (carr G)) by Def4; then A1: dom G = dom (carr G) by FINSEQ_1:def_3; now__::_thesis:_for_a1,_b1_being_real_number_ for_v,_w_being_VECTOR_of_GS_holds_ (_a1_*_(v_+_w)_=_(a1_*_v)_+_(a1_*_w)_&_(a1_+_b1)_*_v_=_(a1_*_v)_+_(b1_*_v)_&_(a1_*_b1)_*_v_=_a1_*_(b1_*_v)_&_1_*_v_=_v_) let a1, b1 be real number ; ::_thesis: for v, w being VECTOR of GS holds ( a1 * (v + w) = (a1 * v) + (a1 * w) & (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v ) reconsider a = a1, b = b1 as Real by XREAL_0:def_1; let v, w be VECTOR of GS; ::_thesis: ( a1 * (v + w) = (a1 * v) + (a1 * w) & (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v ) reconsider v1 = v, w1 = w as Element of product (carr G) ; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_ ([:(multop_G):]_._(1,v1))_._x_=_v1_._x let x be set ; ::_thesis: ( x in dom (carr G) implies ([:(multop G):] . (1,v1)) . x = v1 . x ) assume x in dom (carr G) ; ::_thesis: ([:(multop G):] . (1,v1)) . x = v1 . x then reconsider i = x as Element of dom (carr G) ; reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4; ([:(multop G):] . (1,v1)) . x = 1 * vi by Lm4; hence ([:(multop G):] . (1,v1)) . x = v1 . x by RLVECT_1:def_8; ::_thesis: verum end; A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_ ([:(multop_G):]_._((a_+_b),v1))_._x_=_([:(addop_G):]_._(([:(multop_G):]_._(a,v1)),([:(multop_G):]_._(b,v1))))_._x let x be set ; ::_thesis: ( x in dom (carr G) implies ([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . x ) assume x in dom (carr G) ; ::_thesis: ([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . x then reconsider i = x as Element of dom (carr G) ; reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4; ([:(multop G):] . ((a + b),v1)) . i = (a + b) * vi by Lm4 .= (a * vi) + (b * vi) by RLVECT_1:def_6 .= H1(G . i) . ((([:(multop G):] . (a,v1)) . i),(b * vi)) by Lm4 .= H1(G . i) . ((([:(multop G):] . (a,v1)) . i),(([:(multop G):] . (b,v1)) . i)) by Lm4 ; hence ([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . x by Lm3; ::_thesis: verum end; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_ ([:(multop_G):]_._(a,([:(addop_G):]_._(v1,w1))))_._x_=_([:(addop_G):]_._(([:(multop_G):]_._(a,v1)),([:(multop_G):]_._(a,w1))))_._x let x be set ; ::_thesis: ( x in dom (carr G) implies ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . x ) assume x in dom (carr G) ; ::_thesis: ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . x then reconsider i = x as Element of dom (carr G) ; reconsider vi = v1 . i, wi = w1 . i as VECTOR of (G . i) by A1, Def4; ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . i = the Mult of (G . i) . (a,(([:(addop G):] . (v1,w1)) . i)) by Lm4 .= a * (vi + wi) by Lm3 .= (a * vi) + (a * wi) by RLVECT_1:def_5 .= H1(G . i) . ((([:(multop G):] . (a,v1)) . i),(a * wi)) by Lm4 .= H1(G . i) . ((([:(multop G):] . (a,v1)) . i),(([:(multop G):] . (a,w1)) . i)) by Lm4 ; hence ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . x by Lm3; ::_thesis: verum end; ( dom ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) = dom (carr G) & dom ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) = dom (carr G) ) by CARD_3:9; hence a1 * (v + w) = (a1 * v) + (a1 * w) by A4, FUNCT_1:2; ::_thesis: ( (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v ) A5: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_G)_holds_ ([:(multop_G):]_._((a_*_b),v1))_._x_=_([:(multop_G):]_._(a,([:(multop_G):]_._(b,v1))))_._x let x be set ; ::_thesis: ( x in dom (carr G) implies ([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . x ) assume x in dom (carr G) ; ::_thesis: ([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . x then reconsider i = x as Element of dom (carr G) ; reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4; ([:(multop G):] . ((a * b),v1)) . i = (a * b) * vi by Lm4 .= a * (b * vi) by RLVECT_1:def_7 .= the Mult of (G . i) . (a,(([:(multop G):] . (b,v1)) . i)) by Lm4 ; hence ([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . x by Lm4; ::_thesis: verum end; ( dom ([:(multop G):] . ((a + b),v1)) = dom (carr G) & dom ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) = dom (carr G) ) by CARD_3:9; hence (a1 + b1) * v = (a1 * v) + (b1 * v) by A3, FUNCT_1:2; ::_thesis: ( (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v ) ( dom ([:(multop G):] . ((a * b),v1)) = dom (carr G) & dom ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) = dom (carr G) ) by CARD_3:9; hence (a1 * b1) * v = a1 * (b1 * v) by A5, FUNCT_1:2; ::_thesis: 1 * v = v ( dom ([:(multop G):] . (1,v1)) = dom (carr G) & dom v1 = dom (carr G) ) by CARD_3:9; hence 1 * v = v by A2, FUNCT_1:2; ::_thesis: verum end; hence ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) by RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: verum end; registration let G be RealLinearSpace-Sequence; cluster product G -> non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) proof deffunc H1( addLoopStr ) -> Element of the carrier of G = the ZeroF of G; reconsider GS = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) as non empty RLSStruct ; deffunc H2( 1-sorted ) -> set = the carrier of G; deffunc H3( addLoopStr ) -> Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:] = the addF of G; A1: now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(carr_G)_._i_=_H2(G_._i) let i be Element of dom (carr G); ::_thesis: (carr G) . i = H2(G . i) dom G = Seg (len G) by FINSEQ_1:def_3 .= Seg (len (carr G)) by Def4 .= dom (carr G) by FINSEQ_1:def_3 ; hence (carr G) . i = H2(G . i) by Def4; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(addop_G)_._i_is_associative let i be Element of dom (carr G); ::_thesis: (addop G) . i is associative ( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by A1, Def5; hence (addop G) . i is associative by FVSUM_1:2; ::_thesis: verum end; then A2: [:(addop G):] is associative by PRVECT_1:18; now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(zeros_G)_._i_is_a_unity_wrt_(addop_G)_._i let i be Element of dom (carr G); ::_thesis: (zeros G) . i is_a_unity_wrt (addop G) . i A3: (zeros G) . i = 0. (G . i) by Def7; ( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by A1, Def5; hence (zeros G) . i is_a_unity_wrt (addop G) . i by A3, PRVECT_1:1; ::_thesis: verum end; then A4: zeros G is_a_unity_wrt [:(addop G):] by PRVECT_1:19; A5: GS is right_complementable proof let x be Element of GS; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable reconsider y = (Frege (complop G)) . x as Element of GS by FUNCT_2:5; take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. GS now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_ (_(complop_G)_._i_is_an_inverseOp_wrt_(addop_G)_._i_&_(addop_G)_._i_is_having_a_unity_) let i be Element of dom (carr G); ::_thesis: ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) 0. (G . i) = H1(G . i) ; then A6: H1(G . i) is_a_unity_wrt H3(G . i) by PRVECT_1:1; A7: (complop G) . i = comp (G . i) by Def6; ( (carr G) . i = H2(G . i) & (addop G) . i = H3(G . i) ) by A1, Def5; hence ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) by A6, A7, PRVECT_1:2, SETWISEO:def_2; ::_thesis: verum end; then Frege (complop G) is_an_inverseOp_wrt [:(addop G):] by PRVECT_1:20; then [:(addop G):] . (x,y) = the_unity_wrt [:(addop G):] by FINSEQOP:def_1; hence x + y = 0. GS by A4, BINOP_1:def_8; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(addop_G)_._i_is_commutative let i be Element of dom (carr G); ::_thesis: (addop G) . i is commutative ( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by A1, Def5; hence (addop G) . i is commutative by FVSUM_1:1; ::_thesis: verum end; then [:(addop G):] is commutative by PRVECT_1:17; hence ( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) by A2, A4, A5, Lm1, Lm2, Lm5; ::_thesis: verum end; end; begin definition let R be Relation; attrR is RealNormSpace-yielding means :Def10: :: PRVECT_2:def 10 for x being set st x in rng R holds x is RealNormSpace; end; :: deftheorem Def10 defines RealNormSpace-yielding PRVECT_2:def_10_:_ for R being Relation holds ( R is RealNormSpace-yielding iff for x being set st x in rng R holds x is RealNormSpace ); registration cluster Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable RealNormSpace-yielding for set ; existence ex b1 being FinSequence st ( not b1 is empty & b1 is RealNormSpace-yielding ) proof set A = the RealNormSpace; take <* the RealNormSpace*> ; ::_thesis: ( not <* the RealNormSpace*> is empty & <* the RealNormSpace*> is RealNormSpace-yielding ) thus not <* the RealNormSpace*> is empty ; ::_thesis: <* the RealNormSpace*> is RealNormSpace-yielding let x be set ; :: according to PRVECT_2:def_10 ::_thesis: ( x in rng <* the RealNormSpace*> implies x is RealNormSpace ) assume that A1: x in rng <* the RealNormSpace*> and A2: x is not RealNormSpace ; ::_thesis: contradiction x in { the RealNormSpace} by A1, FINSEQ_1:38; hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; end; definition mode RealNormSpace-Sequence is non empty RealNormSpace-yielding FinSequence; end; definition let G be RealNormSpace-Sequence; let j be Element of dom G; :: original: . redefine funcG . j -> RealNormSpace; coherence G . j is RealNormSpace proof G . j in rng G by FUNCT_1:def_3; hence G . j is RealNormSpace by Def10; ::_thesis: verum end; end; Lm6: for g being RealNormSpace-yielding FinSequence holds g is RealLinearSpace-yielding proof let g be RealNormSpace-yielding FinSequence; ::_thesis: g is RealLinearSpace-yielding for x being set st x in rng g holds x is RealLinearSpace by Def10; hence g is RealLinearSpace-yielding by Def3; ::_thesis: verum end; registration cluster Relation-like Function-like FinSequence-like RealNormSpace-yielding -> RealLinearSpace-yielding for set ; coherence for b1 being FinSequence st b1 is RealNormSpace-yielding holds b1 is RealLinearSpace-yielding by Lm6; end; definition let G be RealNormSpace-Sequence; let x be Element of product (carr G); func normsequence (G,x) -> Element of REAL (len G) means :Def11: :: PRVECT_2:def 11 ( len it = len G & ( for j being Element of dom G holds it . j = the normF of (G . j) . (x . j) ) ); existence ex b1 being Element of REAL (len G) st ( len b1 = len G & ( for j being Element of dom G holds b1 . j = the normF of (G . j) . (x . j) ) ) proof deffunc H1( Element of dom G) -> Element of REAL = the normF of (G . $1) . (x . $1); consider f being Function of (dom G),REAL such that A1: for j being Element of dom G holds f . j = H1(j) from FUNCT_2:sch_4(); A2: rng f c= REAL ; dom f = dom G by FUNCT_2:def_1; then A3: dom f = Seg (len G) by FINSEQ_1:def_3; then f is FinSequence by FINSEQ_1:def_2; then reconsider f = f as FinSequence of REAL by A2, FINSEQ_1:def_4; A4: f in REAL * by FINSEQ_1:def_11; len f = len G by A3, FINSEQ_1:def_3; then f in (len G) -tuples_on REAL by A4; then reconsider f = f as Element of REAL (len G) ; take f ; ::_thesis: ( len f = len G & ( for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) ) ) thus len f = len G by CARD_1:def_7; ::_thesis: for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) let j be Element of dom G; ::_thesis: f . j = the normF of (G . j) . (x . j) thus f . j = the normF of (G . j) . (x . j) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL (len G) st len b1 = len G & ( for j being Element of dom G holds b1 . j = the normF of (G . j) . (x . j) ) & len b2 = len G & ( for j being Element of dom G holds b2 . j = the normF of (G . j) . (x . j) ) holds b1 = b2 proof let f, g be Element of REAL (len G); ::_thesis: ( len f = len G & ( for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) ) & len g = len G & ( for j being Element of dom G holds g . j = the normF of (G . j) . (x . j) ) implies f = g ) assume that len f = len G and A5: for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) and len g = len G and A6: for j being Element of dom G holds g . j = the normF of (G . j) . (x . j) ; ::_thesis: f = g now__::_thesis:_for_j_being_Nat_st_j_in_Seg_(len_G)_holds_ f_._j_=_g_._j let j be Nat; ::_thesis: ( j in Seg (len G) implies f . j = g . j ) assume j in Seg (len G) ; ::_thesis: f . j = g . j then reconsider j1 = j as Element of dom G by FINSEQ_1:def_3; f . j = the normF of (G . j1) . (x . j1) by A5; hence f . j = g . j by A6; ::_thesis: verum end; hence f = g by FINSEQ_2:119; ::_thesis: verum end; end; :: deftheorem Def11 defines normsequence PRVECT_2:def_11_:_ for G being RealNormSpace-Sequence for x being Element of product (carr G) for b3 being Element of REAL (len G) holds ( b3 = normsequence (G,x) iff ( len b3 = len G & ( for j being Element of dom G holds b3 . j = the normF of (G . j) . (x . j) ) ) ); definition let G be RealNormSpace-Sequence; func productnorm G -> Function of (product (carr G)),REAL means :Def12: :: PRVECT_2:def 12 for x being Element of product (carr G) holds it . x = |.(normsequence (G,x)).|; existence ex b1 being Function of (product (carr G)),REAL st for x being Element of product (carr G) holds b1 . x = |.(normsequence (G,x)).| proof deffunc H1( Element of product (carr G)) -> Element of REAL = |.(normsequence (G,$1)).|; consider f being Function of (product (carr G)),REAL such that A1: for x being Element of product (carr G) holds f . x = H1(x) from FUNCT_2:sch_4(); take f ; ::_thesis: for x being Element of product (carr G) holds f . x = |.(normsequence (G,x)).| let x be Element of product (carr G); ::_thesis: f . x = |.(normsequence (G,x)).| thus f . x = |.(normsequence (G,x)).| by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of (product (carr G)),REAL st ( for x being Element of product (carr G) holds b1 . x = |.(normsequence (G,x)).| ) & ( for x being Element of product (carr G) holds b2 . x = |.(normsequence (G,x)).| ) holds b1 = b2 proof let f, g be Function of (product (carr G)),REAL; ::_thesis: ( ( for x being Element of product (carr G) holds f . x = |.(normsequence (G,x)).| ) & ( for x being Element of product (carr G) holds g . x = |.(normsequence (G,x)).| ) implies f = g ) assume that A2: for x being Element of product (carr G) holds f . x = |.(normsequence (G,x)).| and A3: for x being Element of product (carr G) holds g . x = |.(normsequence (G,x)).| ; ::_thesis: f = g now__::_thesis:_for_x_being_Element_of_product_(carr_G)_holds_f_._x_=_g_._x let x be Element of product (carr G); ::_thesis: f . x = g . x f . x = |.(normsequence (G,x)).| by A2; hence f . x = g . x by A3; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def12 defines productnorm PRVECT_2:def_12_:_ for G being RealNormSpace-Sequence for b2 being Function of (product (carr G)),REAL holds ( b2 = productnorm G iff for x being Element of product (carr G) holds b2 . x = |.(normsequence (G,x)).| ); definition let G be RealNormSpace-Sequence; func product G -> non empty strict NORMSTR means :Def13: :: PRVECT_2:def 13 ( RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = product G & the normF of it = productnorm G ); existence ex b1 being non empty strict NORMSTR st ( RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = product G & the normF of b1 = productnorm G ) proof reconsider G0 = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) as non empty strict NORMSTR ; take G0 ; ::_thesis: ( RLSStruct(# the carrier of G0, the ZeroF of G0, the addF of G0, the Mult of G0 #) = product G & the normF of G0 = productnorm G ) thus ( RLSStruct(# the carrier of G0, the ZeroF of G0, the addF of G0, the Mult of G0 #) = product G & the normF of G0 = productnorm G ) ; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict NORMSTR st RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = product G & the normF of b1 = productnorm G & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = product G & the normF of b2 = productnorm G holds b1 = b2 ; end; :: deftheorem Def13 defines product PRVECT_2:def_13_:_ for G being RealNormSpace-Sequence for b2 being non empty strict NORMSTR holds ( b2 = product G iff ( RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = product G & the normF of b2 = productnorm G ) ); theorem Th6: :: PRVECT_2:6 for G being RealNormSpace-Sequence holds product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) proof let G be RealNormSpace-Sequence; ::_thesis: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) RLSStruct(# the carrier of (product G), the ZeroF of (product G), the addF of (product G), the Mult of (product G) #) = product G by Def13; hence product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Def13; ::_thesis: verum end; theorem Th7: :: PRVECT_2:7 for G being RealNormSpace-Sequence for x being VECTOR of (product G) for y being Element of product (carr G) st x = y holds ||.x.|| = |.(normsequence (G,y)).| proof let G be RealNormSpace-Sequence; ::_thesis: for x being VECTOR of (product G) for y being Element of product (carr G) st x = y holds ||.x.|| = |.(normsequence (G,y)).| let x be VECTOR of (product G); ::_thesis: for y being Element of product (carr G) st x = y holds ||.x.|| = |.(normsequence (G,y)).| let y be Element of product (carr G); ::_thesis: ( x = y implies ||.x.|| = |.(normsequence (G,y)).| ) assume A1: x = y ; ::_thesis: ||.x.|| = |.(normsequence (G,y)).| product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6; hence ||.x.|| = |.(normsequence (G,y)).| by A1, Def12; ::_thesis: verum end; theorem Th8: :: PRVECT_2:8 for G being RealNormSpace-Sequence for x, y, z being Element of product (carr G) for i being Element of NAT st i in dom x & z = [:(addop G):] . (x,y) holds (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i proof let G be RealNormSpace-Sequence; ::_thesis: for x, y, z being Element of product (carr G) for i being Element of NAT st i in dom x & z = [:(addop G):] . (x,y) holds (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i let x, y, z be Element of product (carr G); ::_thesis: for i being Element of NAT st i in dom x & z = [:(addop G):] . (x,y) holds (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i let i be Element of NAT ; ::_thesis: ( i in dom x & z = [:(addop G):] . (x,y) implies (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i ) assume that A1: i in dom x and A2: z = [:(addop G):] . (x,y) ; ::_thesis: (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i reconsider i0 = i as Element of dom (carr G) by A1, CARD_3:9; A3: z . i0 = ((addop G) . i0) . ((x . i0),(y . i0)) by A2, PRVECT_1:def_8; dom G = Seg (len G) by FINSEQ_1:def_3 .= Seg (len (carr G)) by Def4 .= dom (carr G) by FINSEQ_1:def_3 ; then reconsider i0 = i as Element of dom G by A1, CARD_3:9; ( dom x = dom (carr G) & (carr G) . i0 = the carrier of (G . i0) ) by Def4, CARD_3:9; then reconsider xi0 = x . i0, yi0 = y . i0, zi0 = z . i0 as Element of (G . i0) by A1, CARD_3:9; ||.zi0.|| = ||.(xi0 + yi0).|| by A3, Def5; then A4: ||.zi0.|| <= ||.xi0.|| + ||.yi0.|| by NORMSP_1:def_1; A5: ((normsequence (G,x)) . i0) + ((normsequence (G,y)) . i0) = ((normsequence (G,x)) + (normsequence (G,y))) . i0 by RVSUM_1:11; ( the normF of (G . i0) . yi0 = (normsequence (G,y)) . i0 & the normF of (G . i0) . zi0 = (normsequence (G,z)) . i0 ) by Def11; hence (normsequence (G,z)) . i <= ((normsequence (G,x)) + (normsequence (G,y))) . i by A4, A5, Def11; ::_thesis: verum end; theorem Th9: :: PRVECT_2:9 for G being RealNormSpace-Sequence for x being Element of product (carr G) for i being Element of NAT st i in dom x holds 0 <= (normsequence (G,x)) . i proof let G be RealNormSpace-Sequence; ::_thesis: for x being Element of product (carr G) for i being Element of NAT st i in dom x holds 0 <= (normsequence (G,x)) . i let x be Element of product (carr G); ::_thesis: for i being Element of NAT st i in dom x holds 0 <= (normsequence (G,x)) . i let i be Element of NAT ; ::_thesis: ( i in dom x implies 0 <= (normsequence (G,x)) . i ) assume A1: i in dom x ; ::_thesis: 0 <= (normsequence (G,x)) . i dom G = Seg (len G) by FINSEQ_1:def_3 .= Seg (len (carr G)) by Def4 .= dom (carr G) by FINSEQ_1:def_3 ; then reconsider i0 = i as Element of dom G by A1, CARD_3:9; ( dom x = dom (carr G) & (carr G) . i0 = the carrier of (G . i0) ) by Def4, CARD_3:9; then reconsider xi0 = x . i0 as Element of (G . i0) by A1, CARD_3:9; 0 <= ||.xi0.|| by NORMSP_1:4; hence 0 <= (normsequence (G,x)) . i by Def11; ::_thesis: verum end; Lm7: for G being RealNormSpace-Sequence holds ( product G is reflexive & product G is discerning & product G is RealNormSpace-like ) proof let G be RealNormSpace-Sequence; ::_thesis: ( product G is reflexive & product G is discerning & product G is RealNormSpace-like ) A1: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6; A2: len G = len (carr G) by Def4; reconsider n = len G as Element of NAT ; thus product G is reflexive ::_thesis: ( product G is discerning & product G is RealNormSpace-like ) proof reconsider z = 0. (product G) as Element of product (carr G) by A1; A3: for i being Element of dom (carr G) holds (normsequence (G,z)) . i = 0 proof let i be Element of dom (carr G); ::_thesis: (normsequence (G,z)) . i = 0 reconsider i0 = i as Element of dom G by A2, FINSEQ_3:29; (carr G) . i0 = the carrier of (G . i0) by Def4; then reconsider zi0 = z . i0 as Element of (G . i0) by CARD_3:9; z . i = 0. (G . i) by A1, Def7; then ||.zi0.|| = 0 ; hence (normsequence (G,z)) . i = 0 by Def11; ::_thesis: verum end; for i being Element of NAT st i in dom (sqr (normsequence (G,z))) holds (sqr (normsequence (G,z))) . i = 0 proof let i be Element of NAT ; ::_thesis: ( i in dom (sqr (normsequence (G,z))) implies (sqr (normsequence (G,z))) . i = 0 ) assume A4: i in dom (sqr (normsequence (G,z))) ; ::_thesis: (sqr (normsequence (G,z))) . i = 0 len (normsequence (G,z)) = len G by Def11; then A5: dom (normsequence (G,z)) = dom G by FINSEQ_3:29; dom (carr G) = dom G by A2, FINSEQ_3:29; then dom (sqr (normsequence (G,z))) = dom (carr G) by A5, VALUED_1:11; then ((normsequence (G,z)) . i) ^2 = 0 ^2 by A3, A4; hence (sqr (normsequence (G,z))) . i = 0 by VALUED_1:11; ::_thesis: verum end; then |.(normsequence (G,z)).| = 0 by Th3, SQUARE_1:17; hence ||.(0. (product G)).|| = 0 by Th7; :: according to NORMSP_0:def_6 ::_thesis: verum end; thus product G is discerning ::_thesis: product G is RealNormSpace-like proof let x be Point of (product G); :: according to NORMSP_0:def_5 ::_thesis: ( not ||.x.|| = 0 or x = 0. (product G) ) reconsider z = x as Element of product (carr G) by A1; assume A6: ||.x.|| = 0 ; ::_thesis: x = 0. (product G) now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_z_._i_=_the_ZeroF_of_(G_._i) let i be Element of dom (carr G); ::_thesis: z . i = the ZeroF of (G . i) reconsider i0 = i as Element of dom G by A2, FINSEQ_3:29; (carr G) . i0 = the carrier of (G . i0) by Def4; then reconsider zzi0 = z . i0 as Element of (G . i0) by CARD_3:9; ||.x.|| = |.(normsequence (G,z)).| by Th7; then normsequence (G,z) = 0* n by A6, EUCLID:8; then (normsequence (G,z)) . i = 0 ; then ||.zzi0.|| = 0 by Def11; then z . i = 0. (G . i) by NORMSP_0:def_5; hence z . i = the ZeroF of (G . i) ; ::_thesis: verum end; hence x = 0. (product G) by A1, Def7; ::_thesis: verum end; let x, y be Point of (product G); :: according to NORMSP_1:def_1 ::_thesis: for b1 being Element of REAL holds ( ||.(b1 * x).|| = (abs b1) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) let a be Real; ::_thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) reconsider z = x as Element of product (carr G) by A1; reconsider xx = x, yy = y as Element of product (carr G) by A1; reconsider ax = a * x as Element of product (carr G) by A1; A7: ( ||.y.|| = |.(normsequence (G,yy)).| & |.((normsequence (G,xx)) + (normsequence (G,yy))).| <= |.(normsequence (G,xx)).| + |.(normsequence (G,yy)).| ) by Th7, EUCLID:12; A8: len (normsequence (G,ax)) = n by CARD_1:def_7; then A9: dom (normsequence (G,ax)) = Seg n by FINSEQ_1:def_3; A10: for i being Nat st i in dom (normsequence (G,ax)) holds (normsequence (G,ax)) . i = ((abs a) * (normsequence (G,z))) . i proof let i be Nat; ::_thesis: ( i in dom (normsequence (G,ax)) implies (normsequence (G,ax)) . i = ((abs a) * (normsequence (G,z))) . i ) assume i in dom (normsequence (G,ax)) ; ::_thesis: (normsequence (G,ax)) . i = ((abs a) * (normsequence (G,z))) . i then reconsider i0 = i as Element of dom G by A9, FINSEQ_1:def_3; reconsider i1 = i0 as Element of dom (carr G) by A2, FINSEQ_3:29; ( (carr G) . i0 = the carrier of (G . i0) & dom (carr G) = dom G ) by A2, Def4, FINSEQ_3:29; then reconsider axi0 = ax . i0, zi0 = z . i0 as Element of (G . i0) by CARD_3:9; ([:(multop G):] . (a,z)) . i1 = ((multop G) . i1) . (a,zi0) by Def2; then axi0 = a * zi0 by A1, Def8; then ||.axi0.|| = (abs a) * ||.zi0.|| by NORMSP_1:def_1; then ||.axi0.|| = (abs a) * ((normsequence (G,z)) . i0) by Def11; then ||.axi0.|| = ((abs a) * (normsequence (G,z))) . i0 by RVSUM_1:44; hence (normsequence (G,ax)) . i = ((abs a) * (normsequence (G,z))) . i by Def11; ::_thesis: verum end; len ((abs a) * (normsequence (G,z))) = n by CARD_1:def_7; then |.(normsequence (G,ax)).| = |.((abs a) * (normsequence (G,z))).| by A8, A10, FINSEQ_2:9; then A11: |.(normsequence (G,ax)).| = (abs (abs a)) * |.(normsequence (G,z)).| by EUCLID:11; reconsider z = x + y as Element of product (carr G) by A1; A12: for i being Element of NAT st i in Seg n holds ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i ) proof A13: dom xx = dom (carr G) by CARD_3:9; A14: ( Seg n = dom G & dom (carr G) = dom G ) by A2, FINSEQ_1:def_3, FINSEQ_3:29; let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i ) ) assume A15: i in Seg n ; ::_thesis: ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i ) i in dom z by A15, A14, CARD_3:9; hence ( 0 <= (normsequence (G,z)) . i & (normsequence (G,z)) . i <= ((normsequence (G,xx)) + (normsequence (G,yy))) . i ) by A1, A15, A14, A13, Th8, Th9; ::_thesis: verum end; A16: len (normsequence (G,z)) = n by Def11; then len (normsequence (G,z)) = len ((normsequence (G,xx)) + (normsequence (G,yy))) by CARD_1:def_7; then A17: |.(normsequence (G,z)).| <= |.((normsequence (G,xx)) + (normsequence (G,yy))).| by A16, A12, Th2; ( ||.(x + y).|| = |.(normsequence (G,z)).| & ||.x.|| = |.(normsequence (G,xx)).| ) by Th7; hence ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by A11, A17, A7, Th7, XXREAL_0:2; ::_thesis: verum end; registration let G be RealNormSpace-Sequence; cluster product G -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ; coherence ( product G is reflexive & product G is discerning & product G is RealNormSpace-like & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital & product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable ) proof reconsider G1 = G as RealLinearSpace-Sequence ; A1: RLSStruct(# the carrier of (product G), the ZeroF of (product G), the addF of (product G), the Mult of (product G) #) = product G by Def13; A2: now__::_thesis:_for_v_being_VECTOR_of_(product_G)_holds_1_*_v_=_v let v be VECTOR of (product G); ::_thesis: 1 * v = v reconsider v1 = v as VECTOR of (product G1) by A1; 1 * v = 1 * v1 by A1; hence 1 * v = v by RLVECT_1:def_8; ::_thesis: verum end; A3: product G is right_complementable proof let v be VECTOR of (product G); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable reconsider v1 = v as VECTOR of (product G1) by A1; reconsider w = - v1 as VECTOR of (product G) by A1; take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. (product G) v + w = v1 - v1 by A1; then v + w = 0. (product G1) by RLVECT_1:15; hence v + w = 0. (product G) by A1; ::_thesis: verum end; A4: now__::_thesis:_for_a_being_real_number_ for_v,_w_being_VECTOR_of_(product_G)_holds_a_*_(v_+_w)_=_(a_*_v)_+_(a_*_w) let a be real number ; ::_thesis: for v, w being VECTOR of (product G) holds a * (v + w) = (a * v) + (a * w) let v, w be VECTOR of (product G); ::_thesis: a * (v + w) = (a * v) + (a * w) reconsider v1 = v, w1 = w as VECTOR of (product G1) by A1; a * (v + w) = a * (v1 + w1) by A1; then a * (v + w) = (a * v1) + (a * w1) by RLVECT_1:def_5; hence a * (v + w) = (a * v) + (a * w) by A1; ::_thesis: verum end; A5: now__::_thesis:_for_a,_b_being_real_number_ for_v_being_VECTOR_of_(product_G)_holds_(a_*_b)_*_v_=_a_*_(b_*_v) let a, b be real number ; ::_thesis: for v being VECTOR of (product G) holds (a * b) * v = a * (b * v) let v be VECTOR of (product G); ::_thesis: (a * b) * v = a * (b * v) reconsider v1 = v as VECTOR of (product G1) by A1; (a * b) * v = (a * b) * v1 by A1; then (a * b) * v = a * (b * v1) by RLVECT_1:def_7; hence (a * b) * v = a * (b * v) by A1; ::_thesis: verum end; A6: now__::_thesis:_for_a,_b_being_real_number_ for_v_being_VECTOR_of_(product_G)_holds_(a_+_b)_*_v_=_(a_*_v)_+_(b_*_v) let a, b be real number ; ::_thesis: for v being VECTOR of (product G) holds (a + b) * v = (a * v) + (b * v) let v be VECTOR of (product G); ::_thesis: (a + b) * v = (a * v) + (b * v) reconsider v1 = v as VECTOR of (product G1) by A1; (a + b) * v = (a + b) * v1 by A1; then (a + b) * v = (a * v1) + (b * v1) by RLVECT_1:def_6; hence (a + b) * v = (a * v) + (b * v) by A1; ::_thesis: verum end; A7: product G is add-associative proof let v, w, x be VECTOR of (product G); :: according to RLVECT_1:def_3 ::_thesis: (v + w) + x = v + (w + x) reconsider v1 = v, w1 = w, x1 = x as VECTOR of (product G1) by A1; (v + w) + x = (v1 + w1) + x1 by A1; then (v + w) + x = v1 + (w1 + x1) by RLVECT_1:def_3; hence (v + w) + x = v + (w + x) by A1; ::_thesis: verum end; A8: product G is Abelian proof let v, w be VECTOR of (product G); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v reconsider v1 = v, w1 = w as VECTOR of (product G1) by A1; v + w = v1 + w1 by A1; then v + w = w1 + v1 ; hence v + w = w + v by A1; ::_thesis: verum end; product G is right_zeroed proof let v be VECTOR of (product G); :: according to RLVECT_1:def_4 ::_thesis: v + (0. (product G)) = v reconsider v1 = v as VECTOR of (product G1) by A1; v + (0. (product G)) = v1 + (0. (product G1)) by A1; hence v + (0. (product G)) = v by RLVECT_1:def_4; ::_thesis: verum end; hence ( product G is reflexive & product G is discerning & product G is RealNormSpace-like & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital & product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable ) by A8, A7, A3, A4, A6, A5, A2, Lm7, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: verum end; end; theorem Th10: :: PRVECT_2:10 for G being RealNormSpace-Sequence for i being Element of dom G for x being Point of (product G) for y being Element of product (carr G) for xi being Point of (G . i) st y = x & xi = y . i holds ||.xi.|| <= ||.x.|| proof let G be RealNormSpace-Sequence; ::_thesis: for i being Element of dom G for x being Point of (product G) for y being Element of product (carr G) for xi being Point of (G . i) st y = x & xi = y . i holds ||.xi.|| <= ||.x.|| let i be Element of dom G; ::_thesis: for x being Point of (product G) for y being Element of product (carr G) for xi being Point of (G . i) st y = x & xi = y . i holds ||.xi.|| <= ||.x.|| let x be Point of (product G); ::_thesis: for y being Element of product (carr G) for xi being Point of (G . i) st y = x & xi = y . i holds ||.xi.|| <= ||.x.|| let y be Element of product (carr G); ::_thesis: for xi being Point of (G . i) st y = x & xi = y . i holds ||.xi.|| <= ||.x.|| let xi be Point of (G . i); ::_thesis: ( y = x & xi = y . i implies ||.xi.|| <= ||.x.|| ) reconsider n = len G as Element of NAT ; assume that A1: y = x and A2: xi = y . i ; ::_thesis: ||.xi.|| <= ||.x.|| A3: ((normsequence (G,y)) . i) ^2 = (sqr (normsequence (G,y))) . i by VALUED_1:11; A4: for i being Element of NAT st i in Seg n holds 0 <= (sqr (normsequence (G,y))) . i proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies 0 <= (sqr (normsequence (G,y))) . i ) assume i in Seg n ; ::_thesis: 0 <= (sqr (normsequence (G,y))) . i ((normsequence (G,y)) . i) ^2 >= 0 by XREAL_1:63; hence 0 <= (sqr (normsequence (G,y))) . i by VALUED_1:11; ::_thesis: verum end; dom G = Seg n by FINSEQ_1:def_3; then A5: ( 0 <= ((normsequence (G,y)) . i) ^2 & (sqr (normsequence (G,y))) . i <= Sum (sqr (normsequence (G,y))) ) by A4, REAL_NS1:7, XREAL_1:63; ||.xi.|| = (normsequence (G,y)) . i by A2, Def11; then sqrt ((sqr (normsequence (G,y))) . i) = (normsequence (G,y)) . i by A3, NORMSP_1:4, SQUARE_1:22; then A6: ||.xi.|| = sqrt ((sqr (normsequence (G,y))) . i) by A2, Def11; ||.x.|| = |.(normsequence (G,y)).| by A1, Th7; hence ||.xi.|| <= ||.x.|| by A3, A5, A6, SQUARE_1:26; ::_thesis: verum end; Lm8: for RNS being RealNormSpace for S being sequence of RNS for g being Point of RNS holds ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ) proof let RNS be RealNormSpace; ::_thesis: for S being sequence of RNS for g being Point of RNS holds ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ) let S be sequence of RNS; ::_thesis: for g being Point of RNS holds ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ) let g be Point of RNS; ::_thesis: ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ) now__::_thesis:_(_||.(S_-_g).||_is_convergent_&_lim_||.(S_-_g).||_=_0_implies_(_S_is_convergent_&_lim_S_=_g_)_) assume A1: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ; ::_thesis: ( S is convergent & lim S = g ) A2: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((S_._m)_-_g).||_<_r let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((S . m) - g).|| < r ) reconsider p = r as real number ; assume 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.((S . m) - g).|| < r then consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds abs ((||.(S - g).|| . m) - 0) < p by A1, SEQ_2:def_7; take n = n; ::_thesis: for m being Element of NAT st n <= m holds ||.((S . m) - g).|| < r now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.((S_._m)_-_g).||_<_p let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((S . m) - g).|| < p ) assume n <= m ; ::_thesis: ||.((S . m) - g).|| < p then abs ((||.(S - g).|| . m) - 0) < p by A3; then abs ||.((S - g) . m).|| < p by NORMSP_0:def_4; then A4: abs ||.((S . m) - g).|| < p by NORMSP_1:def_4; 0 <= ||.((S . m) - g).|| by NORMSP_1:4; hence ||.((S . m) - g).|| < p by A4, ABSVALUE:def_1; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds ||.((S . m) - g).|| < r ; ::_thesis: verum end; hence S is convergent by NORMSP_1:def_6; ::_thesis: lim S = g hence lim S = g by A2, NORMSP_1:def_7; ::_thesis: verum end; hence ( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) ) by NORMSP_1:24; ::_thesis: verum end; theorem Th11: :: PRVECT_2:11 for G being RealNormSpace-Sequence for i being Element of dom G for x, y being Point of (product G) for xi, yi being Point of (G . i) for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds ||.(yi - xi).|| <= ||.(y - x).|| proof let G be RealNormSpace-Sequence; ::_thesis: for i being Element of dom G for x, y being Point of (product G) for xi, yi being Point of (G . i) for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds ||.(yi - xi).|| <= ||.(y - x).|| let i be Element of dom G; ::_thesis: for x, y being Point of (product G) for xi, yi being Point of (G . i) for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds ||.(yi - xi).|| <= ||.(y - x).|| let x, y be Point of (product G); ::_thesis: for xi, yi being Point of (G . i) for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds ||.(yi - xi).|| <= ||.(y - x).|| let xi, yi be Point of (G . i); ::_thesis: for zx, zy being Element of product (carr G) st xi = zx . i & zx = x & yi = zy . i & zy = y holds ||.(yi - xi).|| <= ||.(y - x).|| let zx, zy be Element of product (carr G); ::_thesis: ( xi = zx . i & zx = x & yi = zy . i & zy = y implies ||.(yi - xi).|| <= ||.(y - x).|| ) assume that A1: xi = zx . i and A2: zx = x and A3: yi = zy . i and A4: zy = y ; ::_thesis: ||.(yi - xi).|| <= ||.(y - x).|| reconsider zyi = zy . i, zxi = zx . i as Element of (G . i) by A1, A3; A5: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6; then reconsider mzx = - x as Element of product (carr G) ; len G = len (carr G) by Def4; then A6: dom G = dom (carr G) by FINSEQ_3:29; - x = (- 1) * x by RLVECT_1:16; then A7: mzx . i = (- 1) * zxi by A2, A5, A6, Lm4; then reconsider mzxi = mzx . i as Element of (G . i) ; reconsider zyMm = y - x as Element of product (carr G) by A5; zyMm . i = zyi + mzxi by A4, A5, A6, Lm3; then zyMm . i = zyi + (- zxi) by A7, RLVECT_1:16; hence ||.(yi - xi).|| <= ||.(y - x).|| by A1, A3, Th10; ::_thesis: verum end; theorem :: PRVECT_2:12 for G being RealNormSpace-Sequence for seq being sequence of (product G) for x0 being Point of (product G) for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) proof let G be RealNormSpace-Sequence; ::_thesis: for seq being sequence of (product G) for x0 being Point of (product G) for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) let seq be sequence of (product G); ::_thesis: for x0 being Point of (product G) for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) let x0 be Point of (product G); ::_thesis: for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) let y0 be Element of product (carr G); ::_thesis: ( x0 = y0 & seq is convergent & lim seq = x0 implies for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ) assume that A1: x0 = y0 and A2: ( seq is convergent & lim seq = x0 ) ; ::_thesis: for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) let i be Element of dom G; ::_thesis: ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) defpred S1[ Element of NAT , Element of (G . i)] means ex seqm being Element of product (carr G) st ( seqm = seq . $1 & $2 = seqm . i ); len G = len (carr G) by Def4; then A3: dom G = dom (carr G) by FINSEQ_3:29; then y0 . i in (carr G) . i by CARD_3:9; then reconsider x0i = y0 . i as Point of (G . i) by Def4; A4: for x being Element of NAT ex y being Element of (G . i) st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of (G . i) st S1[x,y] product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6; then consider seqm being Element of product (carr G) such that A5: seqm = seq . x ; take seqm . i ; ::_thesis: ( seqm . i is Element of (G . i) & S1[x,seqm . i] ) (carr G) . i = the carrier of (G . i) by Def4; hence ( seqm . i is Element of (G . i) & S1[x,seqm . i] ) by A3, A5, CARD_3:9; ::_thesis: verum end; ex f being Function of NAT, the carrier of (G . i) st for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A4); then consider seqi being sequence of (G . i) such that A6: for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ; take seqi ; ::_thesis: ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) A7: 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 ||.((seqi . n) - x0i).|| < r proof 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 ||.((seqi . n) - x0i).|| < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((seqi . n) - x0i).|| < r then consider k being Element of NAT such that A8: for n being Element of NAT st k <= n holds ||.((seq . n) - x0).|| < r by A2, NORMSP_1:def_7; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_ ||.((seqi_._n)_-_x0i).||_<_r let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((seqi . n) - x0i).|| < r ) assume n >= k ; ::_thesis: ||.((seqi . n) - x0i).|| < r then A9: ||.((seq . n) - x0).|| < r by A8; ex seqn being Element of product (carr G) st ( seqn = seq . n & seqi . n = seqn . i ) by A6; then ||.((seqi . n) - x0i).|| <= ||.((seq . n) - x0).|| by A1, Th11; hence ||.((seqi . n) - x0i).|| < r by A9, XXREAL_0:2; ::_thesis: verum end; hence ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((seqi . n) - x0i).|| < r ; ::_thesis: verum end; then seqi is convergent by NORMSP_1:def_6; hence ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) by A6, A7, NORMSP_1:def_7; ::_thesis: verum end; theorem Th13: :: PRVECT_2:13 for G being RealNormSpace-Sequence for seq being sequence of (product G) for x0 being Point of (product G) for y0 being Element of product (carr G) st x0 = y0 & ( for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ) holds ( seq is convergent & lim seq = x0 ) proof let G be RealNormSpace-Sequence; ::_thesis: for seq being sequence of (product G) for x0 being Point of (product G) for y0 being Element of product (carr G) st x0 = y0 & ( for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ) holds ( seq is convergent & lim seq = x0 ) let seq be sequence of (product G); ::_thesis: for x0 being Point of (product G) for y0 being Element of product (carr G) st x0 = y0 & ( for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ) holds ( seq is convergent & lim seq = x0 ) let x0 be Point of (product G); ::_thesis: for y0 being Element of product (carr G) st x0 = y0 & ( for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ) holds ( seq is convergent & lim seq = x0 ) let y0 be Element of product (carr G); ::_thesis: ( x0 = y0 & ( for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ) implies ( seq is convergent & lim seq = x0 ) ) assume that A1: x0 = y0 and A2: for i being Element of dom G ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ; ::_thesis: ( seq is convergent & lim seq = x0 ) defpred S1[ Element of dom G, set ] means ex rseqi being Real_Sequence ex seqi being sequence of (G . $1) st ( rseqi = $2 & seqi is convergent & rseqi is convergent & lim rseqi = 0 & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . $1 ) ) ); A3: for i being Element of dom G ex yyseqi being Element of Funcs (NAT,REAL) st S1[i,yyseqi] proof let i be Element of dom G; ::_thesis: ex yyseqi being Element of Funcs (NAT,REAL) st S1[i,yyseqi] consider seqi being sequence of (G . i) such that A4: seqi is convergent and y0 . i = lim seqi and A5: for m being Element of NAT ex Sm being Element of product (carr G) st ( Sm = seq . m & seqi . m = Sm . i ) by A2; set rseqi = ||.(seqi - (lim seqi)).||; A6: ||.(seqi - (lim seqi)).|| is Element of Funcs (NAT,REAL) by FUNCT_2:8; ( ||.(seqi - (lim seqi)).|| is convergent & lim ||.(seqi - (lim seqi)).|| = 0 ) by A4, Lm8; hence ex yyseqi being Element of Funcs (NAT,REAL) st S1[i,yyseqi] by A4, A5, A6; ::_thesis: verum end; consider yyseq being Function of (dom G),(Funcs (NAT,REAL)) such that A7: for i being Element of dom G holds S1[i,yyseq . i] from FUNCT_2:sch_3(A3); reconsider I = len G as Element of NAT ; defpred S2[ Element of NAT , Element of REAL I] means for i being Element of dom G holds (yyseq . i) . $1 = $2 . i; A8: for k being Element of NAT ex yseqk being Element of REAL I st S2[k,yseqk] proof let k be Element of NAT ; ::_thesis: ex yseqk being Element of REAL I st S2[k,yseqk] defpred S3[ set , set ] means ex i being Element of dom G st ( i = $1 & $2 = (yyseq . i) . k ); A9: for k being Nat st k in Seg I holds ex x being set st S3[k,x] proof let j be Nat; ::_thesis: ( j in Seg I implies ex x being set st S3[j,x] ) assume j in Seg I ; ::_thesis: ex x being set st S3[j,x] then reconsider i = j as Element of dom G by FINSEQ_1:def_3; take (yyseq . i) . k ; ::_thesis: S3[j,(yyseq . i) . k] thus S3[j,(yyseq . i) . k] ; ::_thesis: verum end; consider yseqk being FinSequence such that A10: ( dom yseqk = Seg I & ( for j being Nat st j in Seg I holds S3[j,yseqk . j] ) ) from FINSEQ_1:sch_1(A9); now__::_thesis:_for_j_being_Nat_st_j_in_dom_yseqk_holds_ yseqk_._j_in_REAL let j be Nat; ::_thesis: ( j in dom yseqk implies yseqk . j in REAL ) assume j in dom yseqk ; ::_thesis: yseqk . j in REAL then consider i being Element of dom G such that i = j and A11: yseqk . j = (yyseq . i) . k by A10; yyseq . i is Function of NAT,REAL by FUNCT_2:66; hence yseqk . j in REAL by A11, FUNCT_2:5; ::_thesis: verum end; then reconsider yyy = yseqk as FinSequence of REAL by FINSEQ_2:12; yyy is Element of (len yyy) -tuples_on REAL by FINSEQ_2:92; then reconsider yseqk = yseqk as Element of REAL I by A10, FINSEQ_1:def_3; now__::_thesis:_for_j_being_Element_of_dom_G_holds_yseqk_._j_=_(yyseq_._j)_._k let j be Element of dom G; ::_thesis: yseqk . j = (yyseq . j) . k j in dom G ; then j in Seg I by FINSEQ_1:def_3; then ex i being Element of dom G st ( i = j & yseqk . j = (yyseq . i) . k ) by A10; hence yseqk . j = (yyseq . j) . k ; ::_thesis: verum end; hence ex yseqk being Element of REAL I st S2[k,yseqk] ; ::_thesis: verum end; consider yseq being Function of NAT,(REAL I) such that A12: for k being Element of NAT holds S2[k,yseq . k] from FUNCT_2:sch_3(A8); A13: now__::_thesis:_for_i0_being_Element_of_NAT_st_i0_in_Seg_I_holds_ ex_i_being_Element_of_dom_G_ex_rseqi_being_Real_Sequence_ex_seqi_being_sequence_of_(G_._i)_st_ (_(_for_k_being_Element_of_NAT_holds_rseqi_._k_=_(yseq_._k)_._i0_)_&_i_=_i0_&_seqi_is_convergent_&_rseqi_is_convergent_&_lim_rseqi_=_(0*_I)_._i_&_rseqi_=_||.(seqi_-_(lim_seqi)).||_&_(_for_m_being_Element_of_NAT_ex_seqm_being_Element_of_product_(carr_G)_st_ (_seqm_=_seq_._m_&_seqi_._m_=_seqm_._i_)_)_) let i0 be Element of NAT ; ::_thesis: ( i0 in Seg I implies ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ) assume i0 in Seg I ; ::_thesis: ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) then reconsider i = i0 as Element of dom G by FINSEQ_1:def_3; take i = i; ::_thesis: ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) consider rseqi being Real_Sequence, seqi being sequence of (G . i) such that A14: ( rseqi = yyseq . i & seqi is convergent & rseqi is convergent & lim rseqi = 0 & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) by A7; take rseqi = rseqi; ::_thesis: ex seqi being sequence of (G . i) st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) take seqi = seqi; ::_thesis: ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) thus ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) by A12, A14; ::_thesis: verum end; the carrier of (REAL-NS I) = REAL I by REAL_NS1:def_4; then reconsider xseq = yseq as sequence of (REAL-NS I) ; xseq = yseq ; then consider xseq being sequence of (REAL-NS I), yseq being Function of NAT,(REAL I) such that A15: xseq = yseq and A16: for i0 being Element of NAT st i0 in Seg I holds ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) by A13; A17: for i being Element of NAT st i in Seg I holds ex rseqi being Real_Sequence st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i ) & rseqi is convergent & (0* I) . i = lim rseqi ) proof let i0 be Element of NAT ; ::_thesis: ( i0 in Seg I implies ex rseqi being Real_Sequence st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi ) ) assume i0 in Seg I ; ::_thesis: ex rseqi being Real_Sequence st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi ) then ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) by A16; hence ex rseqi being Real_Sequence st ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi ) ; ::_thesis: verum end; A18: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6; now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ ||.(xseq_-_(0._(REAL-NS_I))).||_._x_=_||.(seq_-_x0).||_._x let x be set ; ::_thesis: ( x in NAT implies ||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x ) assume x in NAT ; ::_thesis: ||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x then reconsider i = x as Element of NAT ; reconsider seqimx0 = (seq . i) - x0 as Element of product (carr G) by A18; A19: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(normsequence_(G,seqimx0))_holds_ (normsequence_(G,seqimx0))_._k_=_(yseq_._i)_._k reconsider mx0 = - x0 as Element of product (carr G) by A18; let k be Nat; ::_thesis: ( k in dom (normsequence (G,seqimx0)) implies (normsequence (G,seqimx0)) . k = (yseq . i) . k ) assume A20: k in dom (normsequence (G,seqimx0)) ; ::_thesis: (normsequence (G,seqimx0)) . k = (yseq . i) . k A21: len G = len (normsequence (G,seqimx0)) by Def11; then reconsider k0 = k as Element of dom G by A20, FINSEQ_3:29; k in Seg I by A20, A21, FINSEQ_1:def_3; then consider k1 being Element of dom G, rseqk1i being Real_Sequence, seqk1i being sequence of (G . k1) such that A22: for j being Element of NAT holds rseqk1i . j = (yseq . j) . k and A23: k1 = k and seqk1i is convergent and rseqk1i is convergent and lim rseqk1i = (0* I) . k1 and A24: rseqk1i = ||.(seqk1i - (lim seqk1i)).|| and A25: for m being Element of NAT ex seqk1m being Element of product (carr G) st ( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) by A16; consider seqk0 being sequence of (G . k0) such that seqk0 is convergent and A26: y0 . k0 = lim seqk0 and A27: for m being Element of NAT ex seqm0 being Element of product (carr G) st ( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) by A2; A28: ex seqm0 being Element of product (carr G) st ( seqm0 = seq . i & seqk0 . i = seqm0 . k0 ) by A27; now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ seqk1i_._x_=_seqk0_._x let x be set ; ::_thesis: ( x in NAT implies seqk1i . x = seqk0 . x ) assume x in NAT ; ::_thesis: seqk1i . x = seqk0 . x then reconsider m = x as Element of NAT ; ( ex seqk1m being Element of product (carr G) st ( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) & ex seqm0 being Element of product (carr G) st ( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) ) by A27, A25; hence seqk1i . x = seqk0 . x by A23; ::_thesis: verum end; then A29: seqk1i = seqk0 by A23, FUNCT_2:12; len G = len (carr G) by Def4; then A30: dom G = dom (carr G) by FINSEQ_3:29; - x0 = (- 1) * x0 by RLVECT_1:16; then mx0 . k0 = (- 1) * (lim seqk0) by A1, A18, A26, A30, Lm4; then - (lim seqk0) = mx0 . k0 by RLVECT_1:16; then A31: seqimx0 . k0 = (seqk0 . i) - (lim seqk0) by A18, A28, A30, Lm3; thus (normsequence (G,seqimx0)) . k = the normF of (G . k0) . (seqimx0 . k0) by Def11 .= ||.((seqk0 - (lim seqk0)) . i).|| by A31, NORMSP_1:def_4 .= ||.(seqk1i - (lim seqk1i)).|| . i by A23, A29, NORMSP_0:def_4 .= (yseq . i) . k by A22, A24 ; ::_thesis: verum end; len (yseq . i) = I by CARD_1:def_7; then len (yseq . i) = len (normsequence (G,seqimx0)) by Def11; then dom (yseq . i) = dom (normsequence (G,seqimx0)) by FINSEQ_3:29; then A32: yseq . i = normsequence (G,seqimx0) by A19, FINSEQ_1:13; thus ||.(xseq - (0. (REAL-NS I))).|| . x = ||.((xseq - (0. (REAL-NS I))) . i).|| by NORMSP_0:def_4 .= ||.((xseq . i) - (0. (REAL-NS I))).|| by NORMSP_1:def_4 .= ||.(xseq . i).|| by RLVECT_1:13 .= |.(yseq . i).| by A15, REAL_NS1:1 .= ||.((seq . i) - x0).|| by A32, Th7 .= ||.((seq - x0) . i).|| by NORMSP_1:def_4 .= ||.(seq - x0).|| . x by NORMSP_0:def_4 ; ::_thesis: verum end; then A33: ||.(xseq - (0. (REAL-NS I))).|| = ||.(seq - x0).|| by FUNCT_2:12; 0* I = 0. (REAL-NS I) by REAL_NS1:def_4; then ( xseq is convergent & lim xseq = 0. (REAL-NS I) ) by A15, A17, REAL_NS1:11; then ( ||.(seq - x0).|| is convergent & lim ||.(seq - x0).|| = 0 ) by A33, Lm8; hence ( seq is convergent & lim seq = x0 ) by Lm8; ::_thesis: verum end; theorem :: PRVECT_2:14 for G being RealNormSpace-Sequence st ( for i being Element of dom G holds G . i is complete ) holds product G is complete proof let G be RealNormSpace-Sequence; ::_thesis: ( ( for i being Element of dom G holds G . i is complete ) implies product G is complete ) assume A1: for i being Element of dom G holds G . i is complete ; ::_thesis: product G is complete reconsider I = len G as Element of NAT ; A2: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6; for seq being sequence of (product G) st seq is Cauchy_sequence_by_Norm holds seq is convergent proof let seq be sequence of (product G); ::_thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent ) defpred S1[ Nat, set ] means ex i being Element of dom G st ( i = $1 & ex seqi being sequence of (G . i) st ( seqi is convergent & $2 = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) ); assume A3: seq is Cauchy_sequence_by_Norm ; ::_thesis: seq is convergent A4: for k being Nat st k in Seg I holds ex x being set st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg I implies ex x being set st S1[k,x] ) assume k in Seg I ; ::_thesis: ex x being set st S1[k,x] then reconsider i = k as Element of dom G by FINSEQ_1:def_3; defpred S2[ Element of NAT , Element of (G . i)] means ex seqm being Element of product (carr G) st ( seqm = seq . $1 & $2 = seqm . i ); A5: for x being Element of NAT ex y being Element of (G . i) st S2[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of (G . i) st S2[x,y] consider seqm being Element of product (carr G) such that A6: seqm = seq . x by A2; len G = len (carr G) by Def4; then A7: dom G = dom (carr G) by FINSEQ_3:29; take seqm . i ; ::_thesis: ( seqm . i is Element of (G . i) & S2[x,seqm . i] ) (carr G) . i = the carrier of (G . i) by Def4; hence ( seqm . i is Element of (G . i) & S2[x,seqm . i] ) by A6, A7, CARD_3:9; ::_thesis: verum end; ex f being Function of NAT, the carrier of (G . i) st for x being Element of NAT holds S2[x,f . x] from FUNCT_2:sch_3(A5); then consider seqi being sequence of (G . i) such that A8: for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ; take lim seqi ; ::_thesis: S1[k, lim seqi] now__::_thesis:_for_r1_being_Real_st_r1_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.((seqi_._n)_-_(seqi_._m)).||_<_r1 let r1 be Real; ::_thesis: ( r1 > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seqi . n) - (seqi . m)).|| < r1 ) assume A9: r1 > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seqi . n) - (seqi . m)).|| < r1 reconsider r = r1 as Element of REAL ; consider k being Element of NAT such that A10: for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r by A3, A9, RSSPACE3:8; now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ ||.((seqi_._n)_-_(seqi_._m)).||_<_r1 let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((seqi . n) - (seqi . m)).|| < r1 ) assume ( n >= k & m >= k ) ; ::_thesis: ||.((seqi . n) - (seqi . m)).|| < r1 then A11: ||.((seq . n) - (seq . m)).|| < r by A10; ( ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) & ex seqn being Element of product (carr G) st ( seqn = seq . n & seqi . n = seqn . i ) ) by A8; then ||.((seqi . n) - (seqi . m)).|| <= ||.((seq . n) - (seq . m)).|| by Th11; hence ||.((seqi . n) - (seqi . m)).|| < r1 by A11, XXREAL_0:2; ::_thesis: verum end; hence ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seqi . n) - (seqi . m)).|| < r1 ; ::_thesis: verum end; then A12: seqi is Cauchy_sequence_by_Norm by RSSPACE3:8; G . i is complete by A1; then seqi is convergent by A12, LOPBAN_1:def_15; hence S1[k, lim seqi] by A8; ::_thesis: verum end; consider yy0 being FinSequence such that A13: ( dom yy0 = Seg I & ( for j being Nat st j in Seg I holds S1[j,yy0 . j] ) ) from FINSEQ_1:sch_1(A4); A14: len yy0 = I by A13, FINSEQ_1:def_3; then A15: len yy0 = len (carr G) by Def4; A16: now__::_thesis:_for_i_being_set_st_i_in_dom_(carr_G)_holds_ yy0_._i_in_(carr_G)_._i let i be set ; ::_thesis: ( i in dom (carr G) implies yy0 . i in (carr G) . i ) assume i in dom (carr G) ; ::_thesis: yy0 . i in (carr G) . i then reconsider x = i as Element of dom (carr G) ; reconsider x = x as Element of dom G by A14, A15, FINSEQ_3:29; reconsider j = x as Element of NAT ; j in dom G ; then j in Seg I by FINSEQ_1:def_3; then ex i0 being Element of dom G st ( i0 = j & ex seqi being sequence of (G . i0) st ( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i0 ) ) ) ) by A13; then yy0 . x in the carrier of (G . x) ; hence yy0 . i in (carr G) . i by Def4; ::_thesis: verum end; ( dom (carr G) = Seg (len (carr G)) & len G = len (carr G) ) by Def4, FINSEQ_1:def_3; then reconsider y0 = yy0 as Element of product (carr G) by A13, A16, CARD_3:9; A17: now__::_thesis:_for_i_being_Element_of_dom_G_ex_seqi_being_sequence_of_(G_._i)_st_ (_seqi_is_convergent_&_y0_._i_=_lim_seqi_&_(_for_m_being_Element_of_NAT_ex_seqm_being_Element_of_product_(carr_G)_st_ (_seqm_=_seq_._m_&_seqi_._m_=_seqm_._i_)_)_) let i be Element of dom G; ::_thesis: ex seqi being sequence of (G . i) st ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) reconsider j = i as Element of NAT ; i in dom G ; then i in Seg I by FINSEQ_1:def_3; then consider i0 being Element of dom G such that A18: i0 = j and A19: ex seqi being sequence of (G . i0) st ( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A13; consider seqi being sequence of (G . i0) such that A20: ( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A19; reconsider seqi = seqi as sequence of (G . i) by A18; take seqi = seqi; ::_thesis: ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) thus ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st ( seqm = seq . m & seqi . m = seqm . i ) ) ) by A18, A20; ::_thesis: verum end; reconsider x0 = y0 as Point of (product G) by A2; x0 = y0 ; hence seq is convergent by A17, Th13; ::_thesis: verum end; hence product G is complete by LOPBAN_1:def_15; ::_thesis: verum end;