:: RLVECT_2 semantic presentation begin definition let S be 1-sorted ; let x be set ; assume A1: x in S ; func vector (S,x) -> Element of S equals :Def1: :: RLVECT_2:def 1 x; coherence x is Element of S by A1, STRUCT_0:def_5; end; :: deftheorem Def1 defines vector RLVECT_2:def_1_:_ for S being 1-sorted for x being set st x in S holds vector (S,x) = x; theorem :: RLVECT_2:1 for S being non empty 1-sorted for v being Element of S holds vector (S,v) = v by Def1, RLVECT_1:1; theorem Th2: :: RLVECT_2:2 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) holds Sum H = (Sum F) + (Sum G) proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) holds Sum H = (Sum F) + (Sum G) defpred S1[ Element of NAT ] means for F, G, H being FinSequence of the carrier of V st len F = $1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) holds Sum H = (Sum F) + (Sum G); now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_F,_G,_H_being_FinSequence_of_the_carrier_of_V_st_len_F_=_k_&_len_F_=_len_G_&_len_F_=_len_H_&_(_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_ H_._k_=_(F_/._k)_+_(G_/._k)_)_holds_ Sum_H_=_(Sum_F)_+_(Sum_G)_)_holds_ for_F,_G,_H_being_FinSequence_of_the_carrier_of_V_st_len_F_=_k_+_1_&_len_F_=_len_G_&_len_F_=_len_H_&_(_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_ H_._k_=_(F_/._k)_+_(G_/._k)_)_holds_ Sum_H_=_(Sum_F)_+_(Sum_G) let k be Element of NAT ; ::_thesis: ( ( for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) holds Sum H = (Sum F) + (Sum G) ) implies for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) holds Sum H = (Sum F) + (Sum G) ) assume A1: for F, G, H being FinSequence of the carrier of V st len F = k & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) holds Sum H = (Sum F) + (Sum G) ; ::_thesis: for F, G, H being FinSequence of the carrier of V st len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) holds Sum H = (Sum F) + (Sum G) let F, G, H be FinSequence of the carrier of V; ::_thesis: ( len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) ) assume that A2: len F = k + 1 and A3: len F = len G and A4: len F = len H and A5: for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ; ::_thesis: Sum H = (Sum F) + (Sum G) reconsider f = F | (Seg k), g = G | (Seg k), h = H | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18; A6: len h = k by A2, A4, FINSEQ_3:53; A7: k + 1 in Seg (k + 1) by FINSEQ_1:4; then A8: k + 1 in dom G by A2, A3, FINSEQ_1:def_3; then A9: G . (k + 1) in rng G by FUNCT_1:def_3; k + 1 in dom H by A2, A4, A7, FINSEQ_1:def_3; then A10: H . (k + 1) in rng H by FUNCT_1:def_3; A11: k + 1 in dom F by A2, A7, FINSEQ_1:def_3; then F . (k + 1) in rng F by FUNCT_1:def_3; then reconsider v = F . (k + 1), u = G . (k + 1), w = H . (k + 1) as Element of V by A9, A10; A12: w = (F /. (k + 1)) + (G /. (k + 1)) by A5, A11 .= v + (G /. (k + 1)) by A11, PARTFUN1:def_6 .= v + u by A8, PARTFUN1:def_6 ; G = g ^ <*u*> by A2, A3, FINSEQ_3:55; then A13: Sum G = (Sum g) + (Sum <*u*>) by RLVECT_1:41; A14: Sum <*v*> = v by RLVECT_1:44; A15: len f = k by A2, FINSEQ_3:53; A16: len g = k by A2, A3, FINSEQ_3:53; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_f_holds_ h_._i_=_(f_/._i)_+_(g_/._i) let i be Element of NAT ; ::_thesis: ( i in dom f implies h . i = (f /. i) + (g /. i) ) assume A17: i in dom f ; ::_thesis: h . i = (f /. i) + (g /. i) then A18: F . i = f . i by FUNCT_1:47; len f <= len F by A2, A15, NAT_1:12; then A19: dom f c= dom F by FINSEQ_3:30; then i in dom F by A17; then i in dom G by A3, FINSEQ_3:29; then A20: G /. i = G . i by PARTFUN1:def_6; i in dom h by A15, A6, A17, FINSEQ_3:29; then A21: H . i = h . i by FUNCT_1:47; F /. i = F . i by A17, A19, PARTFUN1:def_6; then A22: f /. i = F /. i by A17, A18, PARTFUN1:def_6; A23: i in dom g by A15, A16, A17, FINSEQ_3:29; then G . i = g . i by FUNCT_1:47; then g /. i = G /. i by A23, A20, PARTFUN1:def_6; hence h . i = (f /. i) + (g /. i) by A5, A17, A21, A19, A22; ::_thesis: verum end; then A24: Sum h = (Sum f) + (Sum g) by A1, A15, A16, A6; F = f ^ <*v*> by A2, FINSEQ_3:55; then A25: Sum F = (Sum f) + (Sum <*v*>) by RLVECT_1:41; A26: Sum <*u*> = u by RLVECT_1:44; H = h ^ <*w*> by A2, A4, FINSEQ_3:55; hence Sum H = (Sum h) + (Sum <*w*>) by RLVECT_1:41 .= ((Sum f) + (Sum g)) + (v + u) by A24, A12, RLVECT_1:44 .= (((Sum f) + (Sum g)) + v) + u by RLVECT_1:def_3 .= ((Sum F) + (Sum g)) + u by A25, A14, RLVECT_1:def_3 .= (Sum F) + (Sum G) by A13, A26, RLVECT_1:def_3 ; ::_thesis: verum end; then A27: for k being Element of NAT st S1[k] holds S1[k + 1] ; A28: S1[ 0 ] proof let F, G, H be FinSequence of the carrier of V; ::_thesis: ( len F = 0 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) ) assume that A29: len F = 0 and A30: len F = len G and A31: len F = len H ; ::_thesis: ( ex k being Element of NAT st ( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) ) A32: Sum H = 0. V by A29, A31, RLVECT_1:75; ( Sum F = 0. V & Sum G = 0. V ) by A29, A30, RLVECT_1:75; hence ( ex k being Element of NAT st ( k in dom F & not H . k = (F /. k) + (G /. k) ) or Sum H = (Sum F) + (Sum G) ) by A32, RLVECT_1:4; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A28, A27); hence for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) + (G /. k) ) holds Sum H = (Sum F) + (Sum G) ; ::_thesis: verum end; theorem :: RLVECT_2:3 for V being RealLinearSpace for a being Real for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) holds Sum G = a * (Sum F) proof let V be RealLinearSpace; ::_thesis: for a being Real for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) holds Sum G = a * (Sum F) let a be Real; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) holds Sum G = a * (Sum F) let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) implies Sum G = a * (Sum F) ) assume that A1: len F = len G and A2: for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ; ::_thesis: Sum G = a * (Sum F) A3: ( dom F = Seg (len F) & dom G = Seg (len G) ) by FINSEQ_1:def_3; now__::_thesis:_for_k_being_Element_of_NAT_ for_v_being_VECTOR_of_V_st_k_in_dom_G_&_v_=_F_._k_holds_ G_._k_=_a_*_v let k be Element of NAT ; ::_thesis: for v being VECTOR of V st k in dom G & v = F . k holds G . k = a * v let v be VECTOR of V; ::_thesis: ( k in dom G & v = F . k implies G . k = a * v ) assume that A4: k in dom G and A5: v = F . k ; ::_thesis: G . k = a * v v = F /. k by A1, A3, A4, A5, PARTFUN1:def_6; hence G . k = a * v by A1, A2, A3, A4; ::_thesis: verum end; hence Sum G = a * (Sum F) by A1, RLVECT_1:39; ::_thesis: verum end; theorem Th4: :: RLVECT_2:4 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = - (F /. k) ) holds Sum G = - (Sum F) proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = - (F /. k) ) holds Sum G = - (Sum F) let F, G be FinSequence of the carrier of V; ::_thesis: ( len F = len G & ( for k being Element of NAT st k in dom F holds G . k = - (F /. k) ) implies Sum G = - (Sum F) ) assume that A1: len F = len G and A2: for k being Element of NAT st k in dom F holds G . k = - (F /. k) ; ::_thesis: Sum G = - (Sum F) now__::_thesis:_for_k_being_Element_of_NAT_ for_v_being_Element_of_V_st_k_in_dom_G_&_v_=_F_._k_holds_ G_._k_=_-_v let k be Element of NAT ; ::_thesis: for v being Element of V st k in dom G & v = F . k holds G . k = - v let v be Element of V; ::_thesis: ( k in dom G & v = F . k implies G . k = - v ) assume that A3: k in dom G and A4: v = F . k ; ::_thesis: G . k = - v A5: ( dom G = Seg (len G) & dom F = Seg (len F) ) by FINSEQ_1:def_3; then v = F /. k by A1, A3, A4, PARTFUN1:def_6; hence G . k = - v by A1, A2, A3, A5; ::_thesis: verum end; hence Sum G = - (Sum F) by A1, RLVECT_1:40; ::_thesis: verum end; theorem :: RLVECT_2:5 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ) holds Sum H = (Sum F) - (Sum G) proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G, H being FinSequence of the carrier of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ) holds Sum H = (Sum F) - (Sum G) let F, G, H be FinSequence of the carrier of V; ::_thesis: ( len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ) implies Sum H = (Sum F) - (Sum G) ) assume that A1: len F = len G and A2: len F = len H and A3: for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ; ::_thesis: Sum H = (Sum F) - (Sum G) deffunc H1( set ) -> Element of the carrier of V = - (G /. $1); consider I being FinSequence such that A4: len I = len G and A5: for k being Nat st k in dom I holds I . k = H1(k) from FINSEQ_1:sch_2(); dom I = Seg (len G) by A4, FINSEQ_1:def_3; then A6: ( dom G = Seg (len G) & ( for k being Element of NAT st k in Seg (len G) holds I . k = H1(k) ) ) by A5, FINSEQ_1:def_3; rng I c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng I or x in the carrier of V ) assume x in rng I ; ::_thesis: x in the carrier of V then consider y being set such that A7: y in dom I and A8: I . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A7; x = - (G /. y) by A5, A7, A8; then reconsider v = x as Element of V ; v in V by RLVECT_1:1; hence x in the carrier of V ; ::_thesis: verum end; then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def_4; A9: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_ H_._k_=_(F_/._k)_+_(I_/._k) let k be Element of NAT ; ::_thesis: ( k in dom F implies H . k = (F /. k) + (I /. k) ) assume A10: k in dom F ; ::_thesis: H . k = (F /. k) + (I /. k) A11: ( dom F = Seg (len F) & dom I = Seg (len I) ) by FINSEQ_1:def_3; then A12: I . k = I /. k by A1, A4, A10, PARTFUN1:def_6; thus H . k = (F /. k) - (G /. k) by A3, A10 .= (F /. k) + (I /. k) by A1, A4, A5, A11, A10, A12 ; ::_thesis: verum end; Sum I = - (Sum G) by A4, A6, Th4; hence Sum H = (Sum F) - (Sum G) by A1, A2, A4, A9, Th2; ::_thesis: verum end; theorem Th6: :: RLVECT_2:6 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for F, G being FinSequence of the carrier of V for f being Permutation of (dom F) st len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) holds Sum F = Sum G proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of the carrier of V for f being Permutation of (dom F) st len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) holds Sum F = Sum G let F, G be FinSequence of the carrier of V; ::_thesis: for f being Permutation of (dom F) st len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) holds Sum F = Sum G let f be Permutation of (dom F); ::_thesis: ( len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) implies Sum F = Sum G ) defpred S1[ Element of NAT ] means for H1, H2 being FinSequence of the carrier of V st len H1 = $1 & len H1 = len H2 holds for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2; now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_H1,_H2_being_FinSequence_of_the_carrier_of_V_st_len_H1_=_k_&_len_H1_=_len_H2_holds_ for_f_being_Permutation_of_(dom_H1)_st_(_for_i_being_Element_of_NAT_st_i_in_dom_H2_holds_ H2_._i_=_H1_._(f_._i)_)_holds_ Sum_H1_=_Sum_H2_)_holds_ for_H1,_H2_being_FinSequence_of_the_carrier_of_V_st_len_H1_=_k_+_1_&_len_H1_=_len_H2_holds_ for_f_being_Permutation_of_(dom_H1)_st_(_for_i_being_Element_of_NAT_st_i_in_dom_H2_holds_ H2_._i_=_H1_._(f_._i)_)_holds_ Sum_H1_=_Sum_H2 let k be Element of NAT ; ::_thesis: ( ( for H1, H2 being FinSequence of the carrier of V st len H1 = k & len H1 = len H2 holds for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 ) implies for H1, H2 being FinSequence of the carrier of V st len H1 = k + 1 & len H1 = len H2 holds for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 ) assume A1: for H1, H2 being FinSequence of the carrier of V st len H1 = k & len H1 = len H2 holds for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 ; ::_thesis: for H1, H2 being FinSequence of the carrier of V st len H1 = k + 1 & len H1 = len H2 holds for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 let H1, H2 be FinSequence of the carrier of V; ::_thesis: ( len H1 = k + 1 & len H1 = len H2 implies for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 ) assume that A2: len H1 = k + 1 and A3: len H1 = len H2 ; ::_thesis: for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 reconsider p = H2 | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18; let f be Permutation of (dom H1); ::_thesis: ( ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) implies Sum H1 = Sum H2 ) A4: dom H1 = Seg (k + 1) by A2, FINSEQ_1:def_3; then A5: rng f = Seg (k + 1) by FUNCT_2:def_3; A6: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_f_holds_ f_._n_is_Element_of_NAT let n be Element of NAT ; ::_thesis: ( n in dom f implies f . n is Element of NAT ) assume n in dom f ; ::_thesis: f . n is Element of NAT then f . n in Seg (k + 1) by A5, FUNCT_1:def_3; hence f . n is Element of NAT ; ::_thesis: verum end; A7: dom H2 = Seg (k + 1) by A2, A3, FINSEQ_1:def_3; then reconsider v = H2 . (k + 1) as Element of V by FINSEQ_1:4, FUNCT_1:102; A8: dom p = Seg (len p) by FINSEQ_1:def_3; ( Seg (k + 1) = {} implies Seg (k + 1) = {} ) ; then A9: dom f = Seg (k + 1) by A4, FUNCT_2:def_1; A10: k + 1 in Seg (k + 1) by FINSEQ_1:4; then A11: f . (k + 1) in Seg (k + 1) by A9, A5, FUNCT_1:def_3; then reconsider n = f . (k + 1) as Element of NAT ; A12: n <= k + 1 by A11, FINSEQ_1:1; then consider m2 being Nat such that A13: n + m2 = k + 1 by NAT_1:10; defpred S2[ Nat, set ] means $2 = H1 . (n + $1); 1 <= n by A11, FINSEQ_1:1; then consider m1 being Nat such that A14: 1 + m1 = n by NAT_1:10; reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def_12; A15: for j being Nat st j in Seg m2 holds ex x being set st S2[j,x] ; consider q2 being FinSequence such that A16: dom q2 = Seg m2 and A17: for k being Nat st k in Seg m2 holds S2[k,q2 . k] from FINSEQ_1:sch_1(A15); rng q2 c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q2 or x in the carrier of V ) assume x in rng q2 ; ::_thesis: x in the carrier of V then consider y being set such that A18: y in dom q2 and A19: x = q2 . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A18; 1 <= y by A16, A18, FINSEQ_1:1; then A20: 1 <= n + y by NAT_1:12; y <= m2 by A16, A18, FINSEQ_1:1; then n + y <= len H1 by A2, A13, XREAL_1:7; then n + y in dom H1 by A20, FINSEQ_3:25; then reconsider xx = H1 . (n + y) as Element of V by FUNCT_1:102; xx in the carrier of V ; hence x in the carrier of V by A16, A17, A18, A19; ::_thesis: verum end; then reconsider q2 = q2 as FinSequence of the carrier of V by FINSEQ_1:def_4; reconsider q1 = H1 | (Seg m1) as FinSequence of the carrier of V by FINSEQ_1:18; defpred S3[ set , set ] means ( ( f . $1 in dom q1 implies $2 = f . $1 ) & ( not f . $1 in dom q1 implies for l being Element of NAT st l = f . $1 holds $2 = l - 1 ) ); A21: k <= k + 1 by NAT_1:12; then A22: Seg k c= Seg (k + 1) by FINSEQ_1:5; A23: for i being Nat st i in Seg k holds ex y being set st S3[i,y] proof let i be Nat; ::_thesis: ( i in Seg k implies ex y being set st S3[i,y] ) assume A24: i in Seg k ; ::_thesis: ex y being set st S3[i,y] now__::_thesis:_(_not_f_._i_in_dom_q1_implies_ex_y_being_Element_of_REAL_st_ (_(_f_._i_in_dom_q1_implies_y_=_f_._i_)_&_(_not_f_._i_in_dom_q1_implies_for_t_being_Element_of_NAT_st_t_=_f_._i_holds_ y_=_t_-_1_)_)_) f . i in Seg (k + 1) by A9, A5, A22, A24, FUNCT_1:def_3; then reconsider j = f . i as Element of NAT ; assume A25: not f . i in dom q1 ; ::_thesis: ex y being Element of REAL st ( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds y = t - 1 ) ) take y = j - 1; ::_thesis: ( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds y = t - 1 ) ) thus ( f . i in dom q1 implies y = f . i ) by A25; ::_thesis: ( not f . i in dom q1 implies for t being Element of NAT st t = f . i holds y = t - 1 ) assume not f . i in dom q1 ; ::_thesis: for t being Element of NAT st t = f . i holds y = t - 1 let t be Element of NAT ; ::_thesis: ( t = f . i implies y = t - 1 ) assume t = f . i ; ::_thesis: y = t - 1 hence y = t - 1 ; ::_thesis: verum end; hence ex y being set st S3[i,y] ; ::_thesis: verum end; consider g being FinSequence such that A26: dom g = Seg k and A27: for i being Nat st i in Seg k holds S3[i,g . i] from FINSEQ_1:sch_1(A23); A28: dom p = Seg k by A2, A3, A21, FINSEQ_1:17; m1 <= n by A14, NAT_1:11; then A29: m1 <= k + 1 by A12, XXREAL_0:2; then A30: dom q1 = Seg m1 by A2, FINSEQ_1:17; A31: now__::_thesis:_for_i,_l_being_Element_of_NAT_st_l_=_f_._i_&_not_f_._i_in_dom_q1_&_i_in_dom_g_holds_ m1_+_2_<=_l let i, l be Element of NAT ; ::_thesis: ( l = f . i & not f . i in dom q1 & i in dom g implies m1 + 2 <= l ) assume that A32: l = f . i and A33: not f . i in dom q1 and A34: i in dom g ; ::_thesis: m1 + 2 <= l A35: ( l < 1 or m1 < l ) by A30, A32, A33, FINSEQ_1:1; A36: now__::_thesis:_not_m1_+_1_=_l assume m1 + 1 = l ; ::_thesis: contradiction then k + 1 = i by A10, A9, A14, A22, A26, A32, A34, FUNCT_1:def_4; then k + 1 <= k + 0 by A26, A34, FINSEQ_1:1; hence contradiction by XREAL_1:6; ::_thesis: verum end; f . i in rng f by A9, A22, A26, A34, FUNCT_1:def_3; then m1 + 1 <= l by A4, A32, A35, FINSEQ_1:1, NAT_1:13; then m1 + 1 < l by A36, XXREAL_0:1; then (m1 + 1) + 1 <= l by NAT_1:13; hence m1 + 2 <= l ; ::_thesis: verum end; A37: len q1 = m1 by A2, A29, FINSEQ_1:17; A38: now__::_thesis:_for_j_being_Nat_st_j_in_dom_q2_holds_ H1_._((len_(q1_^_<*v*>))_+_j)_=_q2_._j let j be Nat; ::_thesis: ( j in dom q2 implies H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j ) assume A39: j in dom q2 ; ::_thesis: H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j len (q1 ^ <*v*>) = m1 + (len <*v*>) by A37, FINSEQ_1:22 .= n by A14, FINSEQ_1:39 ; hence H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j by A16, A17, A39; ::_thesis: verum end; 1 + k = 1 + (m1 + m2) by A14, A13; then A40: m1 <= k by NAT_1:11; A41: rng g c= dom p proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in dom p ) assume y in rng g ; ::_thesis: y in dom p then consider x being set such that A42: x in dom g and A43: g . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A42; now__::_thesis:_y_in_dom_p percases ( f . x in dom q1 or not f . x in dom q1 ) ; supposeA44: f . x in dom q1 ; ::_thesis: y in dom p A45: dom q1 c= dom p by A40, A30, A28, FINSEQ_1:5; f . x = g . x by A26, A27, A42, A44; hence y in dom p by A43, A44, A45; ::_thesis: verum end; supposeA46: not f . x in dom q1 ; ::_thesis: y in dom p reconsider j = f . x as Element of NAT by A9, A22, A6, A26, A42; A47: f . x in Seg (k + 1) by A9, A5, A22, A26, A42, FUNCT_1:def_3; ( j < 1 or m1 < j ) by A30, A46, FINSEQ_1:1; then reconsider l = j - 1 as Element of NAT by A47, FINSEQ_1:1, NAT_1:20; j <= k + 1 by A47, FINSEQ_1:1; then A48: l <= (k + 1) - 1 by XREAL_1:9; m1 + 2 <= j by A31, A42, A46; then A49: (m1 + 2) - 1 <= l by XREAL_1:9; 1 <= m1 + 1 by NAT_1:12; then A50: 1 <= l by A49, XXREAL_0:2; g . x = j - 1 by A26, A27, A42, A46; hence y in dom p by A28, A43, A50, A48, FINSEQ_1:1; ::_thesis: verum end; end; end; hence y in dom p ; ::_thesis: verum end; set q = q1 ^ q2; A51: len q2 = m2 by A16, FINSEQ_1:def_3; then A52: len (q1 ^ q2) = m1 + m2 by A37, FINSEQ_1:22; then A53: dom (q1 ^ q2) = Seg k by A14, A13, FINSEQ_1:def_3; then reconsider g = g as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by A28, A26, A41, FUNCT_2:2; A54: len p = k by A2, A3, A21, FINSEQ_1:17; A55: rng g = dom (q1 ^ q2) proof thus rng g c= dom (q1 ^ q2) ; :: according to XBOOLE_0:def_10 ::_thesis: dom (q1 ^ q2) c= rng g let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (q1 ^ q2) or y in rng g ) assume A56: y in dom (q1 ^ q2) ; ::_thesis: y in rng g then reconsider j = y as Element of NAT ; consider x being set such that A57: x in dom f and A58: f . x = y by A5, A22, A53, A56, FUNCT_1:def_3; reconsider x = x as Element of NAT by A9, A57; now__::_thesis:_y_in_rng_g percases ( x in dom g or not x in dom g ) ; supposeA59: x in dom g ; ::_thesis: y in rng g now__::_thesis:_y_in_rng_g percases ( f . x in dom q1 or not f . x in dom q1 ) ; suppose f . x in dom q1 ; ::_thesis: y in rng g then g . x = f . x by A26, A27, A59; hence y in rng g by A58, A59, FUNCT_1:def_3; ::_thesis: verum end; supposeA60: not f . x in dom q1 ; ::_thesis: y in rng g j <= k by A53, A56, FINSEQ_1:1; then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7; then j + 1 in rng f by A5, FINSEQ_1:1; then consider x1 being set such that A61: x1 in dom f and A62: f . x1 = j + 1 by FUNCT_1:def_3; A63: now__::_thesis:_x1_in_dom_g assume not x1 in dom g ; ::_thesis: contradiction then x1 in (Seg (k + 1)) \ (Seg k) by A4, A26, A61, XBOOLE_0:def_5; then x1 in {(k + 1)} by FINSEQ_3:15; then A64: j + 1 = m1 + 1 by A14, A62, TARSKI:def_1; 1 <= j by A53, A56, FINSEQ_1:1; hence contradiction by A30, A58, A60, A64, FINSEQ_1:1; ::_thesis: verum end; ( j < 1 or m1 < j ) by A30, A58, A60, FINSEQ_1:1; then not j + 1 <= m1 by A53, A56, FINSEQ_1:1, NAT_1:13; then not f . x1 in dom q1 by A30, A62, FINSEQ_1:1; then g . x1 = (j + 1) - 1 by A26, A27, A62, A63 .= y ; hence y in rng g by A63, FUNCT_1:def_3; ::_thesis: verum end; end; end; hence y in rng g ; ::_thesis: verum end; supposeA65: not x in dom g ; ::_thesis: y in rng g j <= k by A53, A56, FINSEQ_1:1; then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:7; then j + 1 in rng f by A5, FINSEQ_1:1; then consider x1 being set such that A66: x1 in dom f and A67: f . x1 = j + 1 by FUNCT_1:def_3; x in (Seg (k + 1)) \ (Seg k) by A4, A26, A57, A65, XBOOLE_0:def_5; then x in {(k + 1)} by FINSEQ_3:15; then A68: x = k + 1 by TARSKI:def_1; A69: now__::_thesis:_x1_in_dom_g assume not x1 in dom g ; ::_thesis: contradiction then x1 in (Seg (k + 1)) \ (Seg k) by A4, A26, A66, XBOOLE_0:def_5; then x1 in {(k + 1)} by FINSEQ_3:15; then j + 1 = j + 0 by A58, A68, A67, TARSKI:def_1; hence contradiction ; ::_thesis: verum end; m1 <= j by A14, A58, A68, XREAL_1:29; then not j + 1 <= m1 by NAT_1:13; then not f . x1 in dom q1 by A30, A67, FINSEQ_1:1; then g . x1 = (j + 1) - 1 by A26, A27, A67, A69 .= y ; hence y in rng g by A69, FUNCT_1:def_3; ::_thesis: verum end; end; end; hence y in rng g ; ::_thesis: verum end; assume A70: for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ; ::_thesis: Sum H1 = Sum H2 then A71: H2 . (k + 1) = H1 . (f . (k + 1)) by A7, FINSEQ_1:4; A72: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(q1_^_<*v*>)_holds_ H1_._j_=_(q1_^_<*v*>)_._j let j be Nat; ::_thesis: ( j in dom (q1 ^ <*v*>) implies H1 . j = (q1 ^ <*v*>) . j ) assume A73: j in dom (q1 ^ <*v*>) ; ::_thesis: H1 . j = (q1 ^ <*v*>) . j A74: now__::_thesis:_(_j_in_Seg_m1_implies_H1_._j_=_(q1_^_<*v*>)_._j_) assume j in Seg m1 ; ::_thesis: H1 . j = (q1 ^ <*v*>) . j then A75: j in dom q1 by A2, A29, FINSEQ_1:17; then q1 . j = H1 . j by FUNCT_1:47; hence H1 . j = (q1 ^ <*v*>) . j by A75, FINSEQ_1:def_7; ::_thesis: verum end; A76: now__::_thesis:_(_j_in_{n}_implies_(q1_^_<*v*>)_._j_=_H1_._j_) ( 1 in Seg 1 & len <*v*> = 1 ) by FINSEQ_1:1, FINSEQ_1:39; then 1 in dom <*v*> by FINSEQ_1:def_3; then A77: (q1 ^ <*v*>) . ((len q1) + 1) = <*v*> . 1 by FINSEQ_1:def_7; assume j in {n} ; ::_thesis: (q1 ^ <*v*>) . j = H1 . j then j = n by TARSKI:def_1; hence (q1 ^ <*v*>) . j = H1 . j by A71, A14, A37, A77, FINSEQ_1:40; ::_thesis: verum end; len (q1 ^ <*v*>) = m1 + (len <*v*>) by A37, FINSEQ_1:22 .= m1 + 1 by FINSEQ_1:40 ; then j in Seg (m1 + 1) by A73, FINSEQ_1:def_3; then j in (Seg m1) \/ {n} by A14, FINSEQ_1:9; hence H1 . j = (q1 ^ <*v*>) . j by A74, A76, XBOOLE_0:def_3; ::_thesis: verum end; g is one-to-one proof let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not y1 in dom g or not b1 in dom g or not g . y1 = g . b1 or y1 = b1 ) let y2 be set ; ::_thesis: ( not y1 in dom g or not y2 in dom g or not g . y1 = g . y2 or y1 = y2 ) assume that A78: y1 in dom g and A79: y2 in dom g and A80: g . y1 = g . y2 ; ::_thesis: y1 = y2 reconsider j1 = y1, j2 = y2 as Element of NAT by A26, A78, A79; A81: f . y2 in Seg (k + 1) by A9, A5, A22, A26, A79, FUNCT_1:def_3; A82: f . y1 in Seg (k + 1) by A9, A5, A22, A26, A78, FUNCT_1:def_3; then reconsider a = f . y1, b = f . y2 as Element of NAT by A81; now__::_thesis:_y1_=_y2 percases ( ( f . y1 in dom q1 & f . y2 in dom q1 ) or ( f . y1 in dom q1 & not f . y2 in dom q1 ) or ( not f . y1 in dom q1 & f . y2 in dom q1 ) or ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ) ; suppose ( f . y1 in dom q1 & f . y2 in dom q1 ) ; ::_thesis: y1 = y2 then ( g . j1 = f . y1 & g . j2 = f . y2 ) by A26, A27, A78, A79; hence y1 = y2 by A9, A22, A26, A78, A79, A80, FUNCT_1:def_4; ::_thesis: verum end; supposeA83: ( f . y1 in dom q1 & not f . y2 in dom q1 ) ; ::_thesis: y1 = y2 then A84: a <= m1 by A30, FINSEQ_1:1; ( g . j1 = a & g . j2 = b - 1 ) by A26, A27, A78, A79, A83; then A85: (b - 1) + 1 <= m1 + 1 by A80, A84, XREAL_1:6; 1 <= b by A81, FINSEQ_1:1; then A86: b in Seg (m1 + 1) by A85, FINSEQ_1:1; not b in Seg m1 by A2, A29, A83, FINSEQ_1:17; then b in (Seg (m1 + 1)) \ (Seg m1) by A86, XBOOLE_0:def_5; then b in {(m1 + 1)} by FINSEQ_3:15; then b = m1 + 1 by TARSKI:def_1; then y2 = k + 1 by A10, A9, A14, A22, A26, A79, FUNCT_1:def_4; hence y1 = y2 by A26, A79, FINSEQ_3:8; ::_thesis: verum end; supposeA87: ( not f . y1 in dom q1 & f . y2 in dom q1 ) ; ::_thesis: y1 = y2 then A88: b <= m1 by A30, FINSEQ_1:1; ( g . j1 = a - 1 & g . j2 = b ) by A26, A27, A78, A79, A87; then A89: (a - 1) + 1 <= m1 + 1 by A80, A88, XREAL_1:6; 1 <= a by A82, FINSEQ_1:1; then A90: a in Seg (m1 + 1) by A89, FINSEQ_1:1; not a in Seg m1 by A2, A29, A87, FINSEQ_1:17; then a in (Seg (m1 + 1)) \ (Seg m1) by A90, XBOOLE_0:def_5; then a in {(m1 + 1)} by FINSEQ_3:15; then a = m1 + 1 by TARSKI:def_1; then y1 = k + 1 by A10, A9, A14, A22, A26, A78, FUNCT_1:def_4; hence y1 = y2 by A26, A78, FINSEQ_3:8; ::_thesis: verum end; supposeA91: ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ; ::_thesis: y1 = y2 then g . j2 = b - 1 by A26, A27, A79; then A92: g . y2 = b + (- 1) ; g . j1 = a - 1 by A26, A27, A78, A91; then g . j1 = a + (- 1) ; then a = b by A80, A92, XCMPLX_1:2; hence y1 = y2 by A9, A22, A26, A78, A79, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence y1 = y2 ; ::_thesis: verum end; then reconsider g = g as Permutation of (dom (q1 ^ q2)) by A55, FUNCT_2:57; (len (q1 ^ <*v*>)) + (len q2) = ((len q1) + (len <*v*>)) + m2 by A51, FINSEQ_1:22 .= k + 1 by A14, A13, A37, FINSEQ_1:40 ; then dom H1 = Seg ((len (q1 ^ <*v*>)) + (len q2)) by A2, FINSEQ_1:def_3; then A93: H1 = (q1 ^ <*v*>) ^ q2 by A72, A38, FINSEQ_1:def_7; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_p_holds_ p_._i_=_(q1_^_q2)_._(g_._i) let i be Element of NAT ; ::_thesis: ( i in dom p implies p . i = (q1 ^ q2) . (g . i) ) assume A94: i in dom p ; ::_thesis: p . i = (q1 ^ q2) . (g . i) then f . i in rng f by A9, A22, A28, FUNCT_1:def_3; then reconsider j = f . i as Element of NAT by A5; now__::_thesis:_p_._i_=_(q1_^_q2)_._(g_._i) percases ( f . i in dom q1 or not f . i in dom q1 ) ; supposeA95: f . i in dom q1 ; ::_thesis: p . i = (q1 ^ q2) . (g . i) then A96: ( f . i = g . i & H1 . j = q1 . j ) by A28, A27, A94, FUNCT_1:47; ( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A70, A7, A22, A28, A94, FUNCT_1:47; hence p . i = (q1 ^ q2) . (g . i) by A95, A96, FINSEQ_1:def_7; ::_thesis: verum end; supposeA97: not f . i in dom q1 ; ::_thesis: p . i = (q1 ^ q2) . (g . i) then m1 + 2 <= j by A28, A26, A31, A94; then A98: (m1 + 2) - 1 <= j - 1 by XREAL_1:9; m1 < m1 + 1 by XREAL_1:29; then A99: m1 < j - 1 by A98, XXREAL_0:2; then m1 < j by XREAL_1:146, XXREAL_0:2; then reconsider j1 = j - 1 as Element of NAT by NAT_1:20; A100: not j1 in dom q1 by A30, A99, FINSEQ_1:1; A101: g . i = j - 1 by A28, A27, A94, A97; then j - 1 in dom (q1 ^ q2) by A28, A26, A55, A94, FUNCT_1:def_3; then consider a being Nat such that A102: a in dom q2 and A103: j1 = (len q1) + a by A100, FINSEQ_1:25; A104: len <*v*> = 1 by FINSEQ_1:39; A105: ( H2 . i = p . i & H2 . i = H1 . (f . i) ) by A70, A7, A22, A28, A94, FUNCT_1:47; A106: H1 = q1 ^ (<*v*> ^ q2) by A93, FINSEQ_1:32; j in dom H1 by A4, A9, A5, A22, A28, A94, FUNCT_1:def_3; then consider b being Nat such that A107: b in dom (<*v*> ^ q2) and A108: j = (len q1) + b by A97, A106, FINSEQ_1:25; A109: H1 . j = (<*v*> ^ q2) . b by A106, A107, A108, FINSEQ_1:def_7; A110: b = 1 + a by A103, A108; (q1 ^ q2) . (j - 1) = q2 . a by A102, A103, FINSEQ_1:def_7; hence p . i = (q1 ^ q2) . (g . i) by A101, A105, A102, A109, A110, A104, FINSEQ_1:def_7; ::_thesis: verum end; end; end; hence p . i = (q1 ^ q2) . (g . i) ; ::_thesis: verum end; then Sum p = Sum (q1 ^ q2) by A1, A14, A13, A54, A52; then Sum H2 = (Sum (q1 ^ q2)) + (Sum <*v*>) by A2, A3, A54, A8, RLVECT_1:38, RLVECT_1:44 .= ((Sum q1) + (Sum q2)) + (Sum <*v*>) by RLVECT_1:41 .= (Sum q1) + ((Sum <*v*>) + (Sum q2)) by RLVECT_1:def_3 .= (Sum q1) + (Sum (<*v*> ^ q2)) by RLVECT_1:41 .= Sum (q1 ^ (<*v*> ^ q2)) by RLVECT_1:41 .= Sum H1 by A93, FINSEQ_1:32 ; hence Sum H1 = Sum H2 ; ::_thesis: verum end; then A111: for k being Element of NAT st S1[k] holds S1[k + 1] ; A112: S1[ 0 ] proof let H1, H2 be FinSequence of the carrier of V; ::_thesis: ( len H1 = 0 & len H1 = len H2 implies for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 ) assume that A113: len H1 = 0 and A114: len H1 = len H2 ; ::_thesis: for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 Sum H1 = 0. V by A113, RLVECT_1:75; hence for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds H2 . i = H1 . (f . i) ) holds Sum H1 = Sum H2 by A113, A114, RLVECT_1:75; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A112, A111); hence ( len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) implies Sum F = Sum G ) ; ::_thesis: verum end; theorem :: RLVECT_2:7 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for F, G being FinSequence of the carrier of V for f being Permutation of (dom F) st G = F * f holds Sum F = Sum G proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for F, G being FinSequence of the carrier of V for f being Permutation of (dom F) st G = F * f holds Sum F = Sum G let F, G be FinSequence of the carrier of V; ::_thesis: for f being Permutation of (dom F) st G = F * f holds Sum F = Sum G let f be Permutation of (dom F); ::_thesis: ( G = F * f implies Sum F = Sum G ) assume G = F * f ; ::_thesis: Sum F = Sum G then ( len F = len G & ( for i being Element of NAT st i in dom G holds G . i = F . (f . i) ) ) by FINSEQ_2:44, FUNCT_1:12; hence Sum F = Sum G by Th6; ::_thesis: verum end; definition let V be non empty addLoopStr ; let T be finite Subset of V; assume A1: ( V is Abelian & V is add-associative & V is right_zeroed ) ; func Sum T -> Element of V means :Def2: :: RLVECT_2:def 2 ex F being FinSequence of the carrier of V st ( rng F = T & F is one-to-one & it = Sum F ); existence ex b1 being Element of V ex F being FinSequence of the carrier of V st ( rng F = T & F is one-to-one & b1 = Sum F ) proof consider p being FinSequence such that A2: rng p = T and A3: p is one-to-one by FINSEQ_4:58; reconsider p = p as FinSequence of the carrier of V by A2, FINSEQ_1:def_4; take Sum p ; ::_thesis: ex F being FinSequence of the carrier of V st ( rng F = T & F is one-to-one & Sum p = Sum F ) take p ; ::_thesis: ( rng p = T & p is one-to-one & Sum p = Sum p ) thus ( rng p = T & p is one-to-one & Sum p = Sum p ) by A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being Element of V st ex F being FinSequence of the carrier of V st ( rng F = T & F is one-to-one & b1 = Sum F ) & ex F being FinSequence of the carrier of V st ( rng F = T & F is one-to-one & b2 = Sum F ) holds b1 = b2 by A1, RLVECT_1:42; end; :: deftheorem Def2 defines Sum RLVECT_2:def_2_:_ for V being non empty addLoopStr for T being finite Subset of V st V is Abelian & V is add-associative & V is right_zeroed holds for b3 being Element of V holds ( b3 = Sum T iff ex F being FinSequence of the carrier of V st ( rng F = T & F is one-to-one & b3 = Sum F ) ); theorem Th8: :: RLVECT_2:8 for V being non empty Abelian add-associative right_zeroed addLoopStr holds Sum ({} V) = 0. V proof let V be non empty Abelian add-associative right_zeroed addLoopStr ; ::_thesis: Sum ({} V) = 0. V Sum (<*> the carrier of V) = 0. V by RLVECT_1:43; hence Sum ({} V) = 0. V by Def2, RELAT_1:38; ::_thesis: verum end; theorem :: RLVECT_2:9 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for v being Element of V holds Sum {v} = v proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v being Element of V holds Sum {v} = v let v be Element of V; ::_thesis: Sum {v} = v A1: Sum <*v*> = v by RLVECT_1:44; ( rng <*v*> = {v} & <*v*> is one-to-one ) by FINSEQ_1:39, FINSEQ_3:93; hence Sum {v} = v by A1, Def2; ::_thesis: verum end; theorem :: RLVECT_2:10 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for v1, v2 being Element of V st v1 <> v2 holds Sum {v1,v2} = v1 + v2 proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v1, v2 being Element of V st v1 <> v2 holds Sum {v1,v2} = v1 + v2 let v1, v2 be Element of V; ::_thesis: ( v1 <> v2 implies Sum {v1,v2} = v1 + v2 ) assume v1 <> v2 ; ::_thesis: Sum {v1,v2} = v1 + v2 then A1: <*v1,v2*> is one-to-one by FINSEQ_3:94; ( rng <*v1,v2*> = {v1,v2} & Sum <*v1,v2*> = v1 + v2 ) by FINSEQ_2:127, RLVECT_1:45; hence Sum {v1,v2} = v1 + v2 by A1, Def2; ::_thesis: verum end; theorem :: RLVECT_2:11 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for v1, v2, v3 being Element of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds Sum {v1,v2,v3} = (v1 + v2) + v3 proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for v1, v2, v3 being Element of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds Sum {v1,v2,v3} = (v1 + v2) + v3 let v1, v2, v3 be Element of V; ::_thesis: ( v1 <> v2 & v2 <> v3 & v1 <> v3 implies Sum {v1,v2,v3} = (v1 + v2) + v3 ) assume ( v1 <> v2 & v2 <> v3 & v1 <> v3 ) ; ::_thesis: Sum {v1,v2,v3} = (v1 + v2) + v3 then A1: <*v1,v2,v3*> is one-to-one by FINSEQ_3:95; ( rng <*v1,v2,v3*> = {v1,v2,v3} & Sum <*v1,v2,v3*> = (v1 + v2) + v3 ) by FINSEQ_2:128, RLVECT_1:46; hence Sum {v1,v2,v3} = (v1 + v2) + v3 by A1, Def2; ::_thesis: verum end; theorem Th12: :: RLVECT_2:12 for V being non empty Abelian add-associative right_zeroed addLoopStr for S, T being finite Subset of V st T misses S holds Sum (T \/ S) = (Sum T) + (Sum S) proof let V be non empty Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V st T misses S holds Sum (T \/ S) = (Sum T) + (Sum S) let S, T be finite Subset of V; ::_thesis: ( T misses S implies Sum (T \/ S) = (Sum T) + (Sum S) ) consider F being FinSequence of the carrier of V such that A1: rng F = T \/ S and A2: ( F is one-to-one & Sum (T \/ S) = Sum F ) by Def2; consider G being FinSequence of the carrier of V such that A3: rng G = T and A4: G is one-to-one and A5: Sum T = Sum G by Def2; consider H being FinSequence of the carrier of V such that A6: rng H = S and A7: H is one-to-one and A8: Sum S = Sum H by Def2; set I = G ^ H; assume T misses S ; ::_thesis: Sum (T \/ S) = (Sum T) + (Sum S) then A9: G ^ H is one-to-one by A3, A4, A6, A7, FINSEQ_3:91; rng (G ^ H) = rng F by A1, A3, A6, FINSEQ_1:31; hence Sum (T \/ S) = Sum (G ^ H) by A2, A9, RLVECT_1:42 .= (Sum T) + (Sum S) by A5, A8, RLVECT_1:41 ; ::_thesis: verum end; theorem Th13: :: RLVECT_2:13 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) let S, T be finite Subset of V; ::_thesis: Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) set A = S \ T; set B = T \ S; set Z = (S \ T) \/ (T \ S); set I = T /\ S; A1: (S \ T) \/ (T /\ S) = S by XBOOLE_1:51; A2: (T \ S) \/ (T /\ S) = T by XBOOLE_1:51; A3: (S \ T) \/ (T \ S) = T \+\ S ; then ((S \ T) \/ (T \ S)) \/ (T /\ S) = T \/ S by XBOOLE_1:93; then (Sum (T \/ S)) + (Sum (T /\ S)) = ((Sum ((S \ T) \/ (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by A3, Th12, XBOOLE_1:103 .= (((Sum (S \ T)) + (Sum (T \ S))) + (Sum (T /\ S))) + (Sum (T /\ S)) by Th12, XBOOLE_1:82 .= ((Sum (S \ T)) + ((Sum (T /\ S)) + (Sum (T \ S)))) + (Sum (T /\ S)) by RLVECT_1:def_3 .= ((Sum (S \ T)) + (Sum (T /\ S))) + ((Sum (T \ S)) + (Sum (T /\ S))) by RLVECT_1:def_3 .= (Sum S) + ((Sum (T \ S)) + (Sum (T /\ S))) by A1, Th12, XBOOLE_1:89 .= (Sum T) + (Sum S) by A2, Th12, XBOOLE_1:89 ; hence Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by RLSUB_2:61; ::_thesis: verum end; theorem :: RLVECT_2:14 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) let S, T be finite Subset of V; ::_thesis: Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S)) by Th13; then (Sum T) + (Sum S) = (Sum (T /\ S)) + (Sum (T \/ S)) by RLSUB_2:61; hence Sum (T /\ S) = ((Sum T) + (Sum S)) - (Sum (T \/ S)) by RLSUB_2:61; ::_thesis: verum end; theorem Th15: :: RLVECT_2:15 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S) proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T \ S) = (Sum (T \/ S)) - (Sum S) let S, T be finite Subset of V; ::_thesis: Sum (T \ S) = (Sum (T \/ S)) - (Sum S) T \ S misses S by XBOOLE_1:79; then A1: (T \ S) /\ S = {} V by XBOOLE_0:def_7; (T \ S) \/ S = T \/ S by XBOOLE_1:39; then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (Sum ((T \ S) /\ S)) by Th13; then Sum (T \/ S) = ((Sum (T \ S)) + (Sum S)) - (0. V) by A1, Th8 .= (Sum (T \ S)) + (Sum S) by RLVECT_1:13 ; hence Sum (T \ S) = (Sum (T \/ S)) - (Sum S) by RLSUB_2:61; ::_thesis: verum end; theorem Th16: :: RLVECT_2:16 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S)) proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T \ S) = (Sum T) - (Sum (T /\ S)) let S, T be finite Subset of V; ::_thesis: Sum (T \ S) = (Sum T) - (Sum (T /\ S)) T \ (T /\ S) = T \ S by XBOOLE_1:47; then Sum (T \ S) = (Sum (T \/ (T /\ S))) - (Sum (T /\ S)) by Th15; hence Sum (T \ S) = (Sum T) - (Sum (T /\ S)) by XBOOLE_1:22; ::_thesis: verum end; theorem :: RLVECT_2:17 for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S)) proof let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S)) let S, T be finite Subset of V; ::_thesis: Sum (T \+\ S) = (Sum (T \/ S)) - (Sum (T /\ S)) T \+\ S = (T \/ S) \ (T /\ S) by XBOOLE_1:101; hence Sum (T \+\ S) = (Sum (T \/ S)) - (Sum ((T \/ S) /\ (T /\ S))) by Th16 .= (Sum (T \/ S)) - (Sum (((T \/ S) /\ T) /\ S)) by XBOOLE_1:16 .= (Sum (T \/ S)) - (Sum (T /\ S)) by XBOOLE_1:21 ; ::_thesis: verum end; theorem :: RLVECT_2:18 for V being non empty Abelian add-associative right_zeroed addLoopStr for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th12, XBOOLE_1:82; definition let V be non empty ZeroStr ; mode Linear_Combination of V -> Element of Funcs ( the carrier of V,REAL) means :Def3: :: RLVECT_2:def 3 ex T being finite Subset of V st for v being Element of V st not v in T holds it . v = 0 ; existence ex b1 being Element of Funcs ( the carrier of V,REAL) ex T being finite Subset of V st for v being Element of V st not v in T holds b1 . v = 0 proof reconsider f = the carrier of V --> 0 as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; take f ; ::_thesis: ex T being finite Subset of V st for v being Element of V st not v in T holds f . v = 0 take {} V ; ::_thesis: for v being Element of V st not v in {} V holds f . v = 0 thus for v being Element of V st not v in {} V holds f . v = 0 by FUNCOP_1:7; ::_thesis: verum end; end; :: deftheorem Def3 defines Linear_Combination RLVECT_2:def_3_:_ for V being non empty ZeroStr for b2 being Element of Funcs ( the carrier of V,REAL) holds ( b2 is Linear_Combination of V iff ex T being finite Subset of V st for v being Element of V st not v in T holds b2 . v = 0 ); notation let V be non empty addLoopStr ; let L be Element of Funcs ( the carrier of V,REAL); synonym Carrier L for support V; end; Lm1: now__::_thesis:_for_V_being_non_empty_addLoopStr_ for_L_being_Element_of_Funcs_(_the_carrier_of_V,REAL)_holds_Carrier_c=_the_carrier_of_V let V be non empty addLoopStr ; ::_thesis: for L being Element of Funcs ( the carrier of V,REAL) holds Carrier c= the carrier of V let L be Element of Funcs ( the carrier of V,REAL); ::_thesis: Carrier c= the carrier of V A1: support L c= dom L by PRE_POLY:37; thus Carrier c= the carrier of V ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier or x in the carrier of V ) assume x in support L ; ::_thesis: x in the carrier of V then x in dom L by A1; hence x in the carrier of V ; ::_thesis: verum end; end; definition let V be non empty addLoopStr ; let L be Element of Funcs ( the carrier of V,REAL); :: original: Carrier redefine func Carrier L -> Subset of V equals :: RLVECT_2:def 4 { v where v is Element of V : L . v <> 0 } ; coherence Carrier is Subset of V by Lm1; compatibility for b1 being Subset of V holds ( b1 = Carrier iff b1 = { v where v is Element of V : L . v <> 0 } ) proof let X be Subset of V; ::_thesis: ( X = Carrier iff X = { v where v is Element of V : L . v <> 0 } ) set A = Carrier ; set B = { v where v is Element of V : L . v <> 0 } ; thus ( X = Carrier implies X = { v where v is Element of V : L . v <> 0 } ) ::_thesis: ( X = { v where v is Element of V : L . v <> 0 } implies X = Carrier ) proof assume A1: X = Carrier ; ::_thesis: X = { v where v is Element of V : L . v <> 0 } thus X c= { v where v is Element of V : L . v <> 0 } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is Element of V : L . v <> 0 } c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in { v where v is Element of V : L . v <> 0 } ) assume A2: x in X ; ::_thesis: x in { v where v is Element of V : L . v <> 0 } then L . x <> 0 by A1, PRE_POLY:def_7; hence x in { v where v is Element of V : L . v <> 0 } by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of V : L . v <> 0 } or x in X ) assume x in { v where v is Element of V : L . v <> 0 } ; ::_thesis: x in X then ex v being Element of V st ( x = v & L . v <> 0 ) ; hence x in X by A1, PRE_POLY:def_7; ::_thesis: verum end; assume A3: X = { v where v is Element of V : L . v <> 0 } ; ::_thesis: X = Carrier thus X c= Carrier :: according to XBOOLE_0:def_10 ::_thesis: Carrier c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Carrier ) assume x in X ; ::_thesis: x in Carrier then ex v being Element of V st ( x = v & L . v <> 0 ) by A3; hence x in Carrier by PRE_POLY:def_7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier or x in X ) assume A4: x in Carrier ; ::_thesis: x in X then A5: L . x <> 0 by PRE_POLY:def_7; Carrier c= the carrier of V by Lm1; hence x in X by A3, A4, A5; ::_thesis: verum end; end; :: deftheorem defines Carrier RLVECT_2:def_4_:_ for V being non empty addLoopStr for L being Element of Funcs ( the carrier of V,REAL) holds Carrier L = { v where v is Element of V : L . v <> 0 } ; registration let V be non empty addLoopStr ; let L be Linear_Combination of V; cluster Carrier -> finite ; coherence Carrier L is finite proof set A = Carrier L; consider T being finite Subset of V such that A1: for v being Element of V st not v in T holds L . v = 0 by Def3; Carrier L c= T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier L or x in T ) assume x in Carrier L ; ::_thesis: x in T then ex v being Element of V st ( x = v & L . v <> 0 ) ; hence x in T by A1; ::_thesis: verum end; hence Carrier L is finite ; ::_thesis: verum end; end; theorem :: RLVECT_2:19 for V being non empty addLoopStr for L being Linear_Combination of V for v being Element of V holds ( L . v = 0 iff not v in Carrier L ) proof let V be non empty addLoopStr ; ::_thesis: for L being Linear_Combination of V for v being Element of V holds ( L . v = 0 iff not v in Carrier L ) let L be Linear_Combination of V; ::_thesis: for v being Element of V holds ( L . v = 0 iff not v in Carrier L ) let v be Element of V; ::_thesis: ( L . v = 0 iff not v in Carrier L ) thus ( L . v = 0 implies not v in Carrier L ) ::_thesis: ( not v in Carrier L implies L . v = 0 ) proof assume A1: L . v = 0 ; ::_thesis: not v in Carrier L assume v in Carrier L ; ::_thesis: contradiction then ex u being Element of V st ( u = v & L . u <> 0 ) ; hence contradiction by A1; ::_thesis: verum end; thus ( not v in Carrier L implies L . v = 0 ) ; ::_thesis: verum end; definition let V be non empty addLoopStr ; func ZeroLC V -> Linear_Combination of V means :Def5: :: RLVECT_2:def 5 Carrier it = {} ; existence ex b1 being Linear_Combination of V st Carrier b1 = {} proof reconsider f = the carrier of V --> 0 as Function of the carrier of V,REAL ; reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; f is Linear_Combination of V proof reconsider T = {} V as empty finite Subset of V ; take T ; :: according to RLVECT_2:def_3 ::_thesis: for v being Element of V st not v in T holds f . v = 0 thus for v being Element of V st not v in T holds f . v = 0 by FUNCOP_1:7; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V ; take f ; ::_thesis: Carrier f = {} set C = { v where v is Element of V : f . v <> 0 } ; now__::_thesis:_not__{__v_where_v_is_Element_of_V_:_f_._v_<>_0__}__<>_{} set x = the Element of { v where v is Element of V : f . v <> 0 } ; assume { v where v is Element of V : f . v <> 0 } <> {} ; ::_thesis: contradiction then the Element of { v where v is Element of V : f . v <> 0 } in { v where v is Element of V : f . v <> 0 } ; then ex v being Element of V st ( the Element of { v where v is Element of V : f . v <> 0 } = v & f . v <> 0 ) ; hence contradiction by FUNCOP_1:7; ::_thesis: verum end; hence Carrier f = {} ; ::_thesis: verum end; uniqueness for b1, b2 being Linear_Combination of V st Carrier b1 = {} & Carrier b2 = {} holds b1 = b2 proof let L, L9 be Linear_Combination of V; ::_thesis: ( Carrier L = {} & Carrier L9 = {} implies L = L9 ) assume that A1: Carrier L = {} and A2: Carrier L9 = {} ; ::_thesis: L = L9 now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_ L_._x_=_L9_._x let x be set ; ::_thesis: ( x in the carrier of V implies L . x = L9 . x ) assume x in the carrier of V ; ::_thesis: L . x = L9 . x then reconsider v = x as Element of V ; A3: now__::_thesis:_not_L9_._v_<>_0 assume L9 . v <> 0 ; ::_thesis: contradiction then v in { u where u is Element of V : L9 . u <> 0 } ; hence contradiction by A2; ::_thesis: verum end; now__::_thesis:_not_L_._v_<>_0 assume L . v <> 0 ; ::_thesis: contradiction then v in { u where u is Element of V : L . u <> 0 } ; hence contradiction by A1; ::_thesis: verum end; hence L . x = L9 . x by A3; ::_thesis: verum end; hence L = L9 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def5 defines ZeroLC RLVECT_2:def_5_:_ for V being non empty addLoopStr for b2 being Linear_Combination of V holds ( b2 = ZeroLC V iff Carrier b2 = {} ); theorem Th20: :: RLVECT_2:20 for V being non empty addLoopStr for v being Element of V holds (ZeroLC V) . v = 0 proof let V be non empty addLoopStr ; ::_thesis: for v being Element of V holds (ZeroLC V) . v = 0 let v be Element of V; ::_thesis: (ZeroLC V) . v = 0 ( Carrier (ZeroLC V) = {} & not v in {} ) by Def5; hence (ZeroLC V) . v = 0 ; ::_thesis: verum end; definition let V be non empty addLoopStr ; let A be Subset of V; mode Linear_Combination of A -> Linear_Combination of V means :Def6: :: RLVECT_2:def 6 Carrier it c= A; existence ex b1 being Linear_Combination of V st Carrier b1 c= A proof take L = ZeroLC V; ::_thesis: Carrier L c= A Carrier L = {} by Def5; hence Carrier L c= A by XBOOLE_1:2; ::_thesis: verum end; end; :: deftheorem Def6 defines Linear_Combination RLVECT_2:def_6_:_ for V being non empty addLoopStr for A being Subset of V for b3 being Linear_Combination of V holds ( b3 is Linear_Combination of A iff Carrier b3 c= A ); theorem :: RLVECT_2:21 for V being RealLinearSpace for A, B being Subset of V for l being Linear_Combination of A st A c= B holds l is Linear_Combination of B proof let V be RealLinearSpace; ::_thesis: for A, B being Subset of V for l being Linear_Combination of A st A c= B holds l is Linear_Combination of B let A, B be Subset of V; ::_thesis: for l being Linear_Combination of A st A c= B holds l is Linear_Combination of B let l be Linear_Combination of A; ::_thesis: ( A c= B implies l is Linear_Combination of B ) assume A1: A c= B ; ::_thesis: l is Linear_Combination of B Carrier l c= A by Def6; then Carrier l c= B by A1, XBOOLE_1:1; hence l is Linear_Combination of B by Def6; ::_thesis: verum end; theorem Th22: :: RLVECT_2:22 for V being RealLinearSpace for A being Subset of V holds ZeroLC V is Linear_Combination of A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V holds ZeroLC V is Linear_Combination of A let A be Subset of V; ::_thesis: ZeroLC V is Linear_Combination of A ( Carrier (ZeroLC V) = {} & {} c= A ) by Def5, XBOOLE_1:2; hence ZeroLC V is Linear_Combination of A by Def6; ::_thesis: verum end; theorem Th23: :: RLVECT_2:23 for V being RealLinearSpace for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V proof let V be RealLinearSpace; ::_thesis: for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V let l be Linear_Combination of {} the carrier of V; ::_thesis: l = ZeroLC V Carrier l c= {} by Def6; then Carrier l = {} ; hence l = ZeroLC V by Def5; ::_thesis: verum end; definition let V be RealLinearSpace; let F be FinSequence of V; let f be Function of the carrier of V,REAL; funcf (#) F -> FinSequence of the carrier of V means :Def7: :: RLVECT_2:def 7 ( len it = len F & ( for i being Element of NAT st i in dom it holds it . i = (f . (F /. i)) * (F /. i) ) ); existence ex b1 being FinSequence of the carrier of V st ( len b1 = len F & ( for i being Element of NAT st i in dom b1 holds b1 . i = (f . (F /. i)) * (F /. i) ) ) proof deffunc H1( set ) -> Element of the carrier of V = (f . (F /. $1)) * (F /. $1); consider G being FinSequence such that A1: len G = len F and A2: for n being Nat st n in dom G holds G . n = H1(n) from FINSEQ_1:sch_2(); rng G c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in the carrier of V ) assume x in rng G ; ::_thesis: x in the carrier of V then consider y being set such that A3: y in dom G and A4: G . y = x by FUNCT_1:def_3; y in Seg (len F) by A1, A3, FINSEQ_1:def_3; then reconsider y = y as Element of NAT ; G . y = (f . (F /. y)) * (F /. y) by A2, A3; hence x in the carrier of V by A4; ::_thesis: verum end; then reconsider G = G as FinSequence of the carrier of V by FINSEQ_1:def_4; take G ; ::_thesis: ( len G = len F & ( for i being Element of NAT st i in dom G holds G . i = (f . (F /. i)) * (F /. i) ) ) thus ( len G = len F & ( for i being Element of NAT st i in dom G holds G . i = (f . (F /. i)) * (F /. i) ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of the carrier of V st len b1 = len F & ( for i being Element of NAT st i in dom b1 holds b1 . i = (f . (F /. i)) * (F /. i) ) & len b2 = len F & ( for i being Element of NAT st i in dom b2 holds b2 . i = (f . (F /. i)) * (F /. i) ) holds b1 = b2 proof let H1, H2 be FinSequence of V; ::_thesis: ( len H1 = len F & ( for i being Element of NAT st i in dom H1 holds H1 . i = (f . (F /. i)) * (F /. i) ) & len H2 = len F & ( for i being Element of NAT st i in dom H2 holds H2 . i = (f . (F /. i)) * (F /. i) ) implies H1 = H2 ) assume that A5: len H1 = len F and A6: for i being Element of NAT st i in dom H1 holds H1 . i = (f . (F /. i)) * (F /. i) and A7: len H2 = len F and A8: for i being Element of NAT st i in dom H2 holds H2 . i = (f . (F /. i)) * (F /. i) ; ::_thesis: H1 = H2 now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_H1_holds_ H1_._k_=_H2_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len H1 implies H1 . k = H2 . k ) assume ( 1 <= k & k <= len H1 ) ; ::_thesis: H1 . k = H2 . k then A9: k in Seg (len H1) by FINSEQ_1:1; then k in dom H1 by FINSEQ_1:def_3; then A10: H1 . k = (f . (F /. k)) * (F /. k) by A6; k in dom H2 by A5, A7, A9, FINSEQ_1:def_3; hence H1 . k = H2 . k by A8, A10; ::_thesis: verum end; hence H1 = H2 by A5, A7, FINSEQ_1:14; ::_thesis: verum end; end; :: deftheorem Def7 defines (#) RLVECT_2:def_7_:_ for V being RealLinearSpace for F being FinSequence of V for f being Function of the carrier of V,REAL for b4 being FinSequence of the carrier of V holds ( b4 = f (#) F iff ( len b4 = len F & ( for i being Element of NAT st i in dom b4 holds b4 . i = (f . (F /. i)) * (F /. i) ) ) ); theorem Th24: :: RLVECT_2:24 for i being Element of NAT for V being RealLinearSpace for v being VECTOR of V for F being FinSequence of V for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v proof let i be Element of NAT ; ::_thesis: for V being RealLinearSpace for v being VECTOR of V for F being FinSequence of V for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for F being FinSequence of V for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v let v be VECTOR of V; ::_thesis: for F being FinSequence of V for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v let F be FinSequence of V; ::_thesis: for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v let f be Function of the carrier of V,REAL; ::_thesis: ( i in dom F & v = F . i implies (f (#) F) . i = (f . v) * v ) assume that A1: i in dom F and A2: v = F . i ; ::_thesis: (f (#) F) . i = (f . v) * v A3: F /. i = F . i by A1, PARTFUN1:def_6; len (f (#) F) = len F by Def7; then i in dom (f (#) F) by A1, FINSEQ_3:29; hence (f (#) F) . i = (f . v) * v by A2, A3, Def7; ::_thesis: verum end; theorem :: RLVECT_2:25 for V being RealLinearSpace for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V proof let V be RealLinearSpace; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V let f be Function of the carrier of V,REAL; ::_thesis: f (#) (<*> the carrier of V) = <*> the carrier of V len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def7 .= 0 ; hence f (#) (<*> the carrier of V) = <*> the carrier of V ; ::_thesis: verum end; theorem Th26: :: RLVECT_2:26 for V being RealLinearSpace for v being VECTOR of V for f being Function of the carrier of V,REAL holds f (#) <*v*> = <*((f . v) * v)*> proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for f being Function of the carrier of V,REAL holds f (#) <*v*> = <*((f . v) * v)*> let v be VECTOR of V; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) <*v*> = <*((f . v) * v)*> let f be Function of the carrier of V,REAL; ::_thesis: f (#) <*v*> = <*((f . v) * v)*> A1: 1 in {1} by TARSKI:def_1; A2: len (f (#) <*v*>) = len <*v*> by Def7 .= 1 by FINSEQ_1:40 ; then dom (f (#) <*v*>) = {1} by FINSEQ_1:2, FINSEQ_1:def_3; then (f (#) <*v*>) . 1 = (f . (<*v*> /. 1)) * (<*v*> /. 1) by A1, Def7 .= (f . (<*v*> /. 1)) * v by FINSEQ_4:16 .= (f . v) * v by FINSEQ_4:16 ; hence f (#) <*v*> = <*((f . v) * v)*> by A2, FINSEQ_1:40; ::_thesis: verum end; theorem Th27: :: RLVECT_2:27 for V being RealLinearSpace for v1, v2 being VECTOR of V for f being Function of the carrier of V,REAL holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> proof let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V for f being Function of the carrier of V,REAL holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> let v1, v2 be VECTOR of V; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> let f be Function of the carrier of V,REAL; ::_thesis: f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> A1: len (f (#) <*v1,v2*>) = len <*v1,v2*> by Def7 .= 2 by FINSEQ_1:44 ; then A2: dom (f (#) <*v1,v2*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3; 2 in {1,2} by TARSKI:def_2; then A3: (f (#) <*v1,v2*>) . 2 = (f . (<*v1,v2*> /. 2)) * (<*v1,v2*> /. 2) by A2, Def7 .= (f . (<*v1,v2*> /. 2)) * v2 by FINSEQ_4:17 .= (f . v2) * v2 by FINSEQ_4:17 ; 1 in {1,2} by TARSKI:def_2; then (f (#) <*v1,v2*>) . 1 = (f . (<*v1,v2*> /. 1)) * (<*v1,v2*> /. 1) by A2, Def7 .= (f . (<*v1,v2*> /. 1)) * v1 by FINSEQ_4:17 .= (f . v1) * v1 by FINSEQ_4:17 ; hence f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> by A1, A3, FINSEQ_1:44; ::_thesis: verum end; theorem :: RLVECT_2:28 for V being RealLinearSpace for v1, v2, v3 being VECTOR of V for f being Function of the carrier of V,REAL holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> proof let V be RealLinearSpace; ::_thesis: for v1, v2, v3 being VECTOR of V for f being Function of the carrier of V,REAL holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> let v1, v2, v3 be VECTOR of V; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> let f be Function of the carrier of V,REAL; ::_thesis: f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> A1: len (f (#) <*v1,v2,v3*>) = len <*v1,v2,v3*> by Def7 .= 3 by FINSEQ_1:45 ; then A2: dom (f (#) <*v1,v2,v3*>) = {1,2,3} by FINSEQ_1:def_3, FINSEQ_3:1; 3 in {1,2,3} by ENUMSET1:def_1; then A3: (f (#) <*v1,v2,v3*>) . 3 = (f . (<*v1,v2,v3*> /. 3)) * (<*v1,v2,v3*> /. 3) by A2, Def7 .= (f . (<*v1,v2,v3*> /. 3)) * v3 by FINSEQ_4:18 .= (f . v3) * v3 by FINSEQ_4:18 ; 2 in {1,2,3} by ENUMSET1:def_1; then A4: (f (#) <*v1,v2,v3*>) . 2 = (f . (<*v1,v2,v3*> /. 2)) * (<*v1,v2,v3*> /. 2) by A2, Def7 .= (f . (<*v1,v2,v3*> /. 2)) * v2 by FINSEQ_4:18 .= (f . v2) * v2 by FINSEQ_4:18 ; 1 in {1,2,3} by ENUMSET1:def_1; then (f (#) <*v1,v2,v3*>) . 1 = (f . (<*v1,v2,v3*> /. 1)) * (<*v1,v2,v3*> /. 1) by A2, Def7 .= (f . (<*v1,v2,v3*> /. 1)) * v1 by FINSEQ_4:18 .= (f . v1) * v1 by FINSEQ_4:18 ; hence f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> by A1, A4, A3, FINSEQ_1:45; ::_thesis: verum end; definition let V be RealLinearSpace; let L be Linear_Combination of V; func Sum L -> Element of V means :Def8: :: RLVECT_2:def 8 ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) ); existence ex b1 being Element of V ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) proof consider F being FinSequence such that A1: rng F = Carrier L and A2: F is one-to-one by FINSEQ_4:58; reconsider F = F as FinSequence of the carrier of V by A1, FINSEQ_1:def_4; take Sum (L (#) F) ; ::_thesis: ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) ) take F ; ::_thesis: ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) ) thus ( F is one-to-one & rng F = Carrier L ) by A1, A2; ::_thesis: Sum (L (#) F) = Sum (L (#) F) thus Sum (L (#) F) = Sum (L (#) F) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of V st ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) & ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & b2 = Sum (L (#) F) ) holds b1 = b2 proof let v1, v2 be Element of V; ::_thesis: ( ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & v1 = Sum (L (#) F) ) & ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & v2 = Sum (L (#) F) ) implies v1 = v2 ) given F1 being FinSequence of the carrier of V such that A3: F1 is one-to-one and A4: rng F1 = Carrier L and A5: v1 = Sum (L (#) F1) ; ::_thesis: ( for F being FinSequence of V holds ( not F is one-to-one or not rng F = Carrier L or not v2 = Sum (L (#) F) ) or v1 = v2 ) given F2 being FinSequence of the carrier of V such that A6: F2 is one-to-one and A7: rng F2 = Carrier L and A8: v2 = Sum (L (#) F2) ; ::_thesis: v1 = v2 defpred S1[ set , set ] means {$2} = F1 " {(F2 . $1)}; A9: dom F2 = Seg (len F2) by FINSEQ_1:def_3; A10: dom F1 = Seg (len F1) by FINSEQ_1:def_3; A11: len F1 = len F2 by A3, A4, A6, A7, FINSEQ_1:48; A12: for x being set st x in dom F1 holds ex y being set st ( y in dom F1 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in dom F1 implies ex y being set st ( y in dom F1 & S1[x,y] ) ) assume x in dom F1 ; ::_thesis: ex y being set st ( y in dom F1 & S1[x,y] ) then F2 . x in rng F1 by A4, A7, A11, A10, A9, FUNCT_1:def_3; then consider y being set such that A13: F1 " {(F2 . x)} = {y} by A3, FUNCT_1:74; take y ; ::_thesis: ( y in dom F1 & S1[x,y] ) y in F1 " {(F2 . x)} by A13, TARSKI:def_1; hence y in dom F1 by FUNCT_1:def_7; ::_thesis: S1[x,y] thus S1[x,y] by A13; ::_thesis: verum end; consider f being Function of (dom F1),(dom F1) such that A14: for x being set st x in dom F1 holds S1[x,f . x] from FUNCT_2:sch_1(A12); A15: f is one-to-one proof let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not y1 in dom f or not b1 in dom f or not f . y1 = f . b1 or y1 = b1 ) let y2 be set ; ::_thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 ) assume that A16: y1 in dom f and A17: y2 in dom f and A18: f . y1 = f . y2 ; ::_thesis: y1 = y2 F2 . y1 in rng F1 by A4, A7, A11, A10, A9, A16, FUNCT_1:def_3; then A19: {(F2 . y1)} c= rng F1 by ZFMISC_1:31; F2 . y2 in rng F1 by A4, A7, A11, A10, A9, A17, FUNCT_1:def_3; then A20: {(F2 . y2)} c= rng F1 by ZFMISC_1:31; ( F1 " {(F2 . y1)} = {(f . y1)} & F1 " {(F2 . y2)} = {(f . y2)} ) by A14, A16, A17; then {(F2 . y1)} = {(F2 . y2)} by A18, A19, A20, FUNCT_1:91; then F2 . y1 = F2 . y2 by ZFMISC_1:3; hence y1 = y2 by A6, A11, A10, A9, A16, A17, FUNCT_1:def_4; ::_thesis: verum end; set G1 = L (#) F1; A21: len (L (#) F1) = len F1 by Def7; A22: rng f = dom F1 proof thus rng f c= dom F1 ; :: according to XBOOLE_0:def_10 ::_thesis: dom F1 c= rng f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom F1 or y in rng f ) assume A23: y in dom F1 ; ::_thesis: y in rng f then F1 . y in rng F2 by A4, A7, FUNCT_1:def_3; then consider x being set such that A24: x in dom F2 and A25: F2 . x = F1 . y by FUNCT_1:def_3; F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A23, A25, FUNCT_1:59; then F1 " {(F2 . x)} c= {y} by A3, FUNCT_1:82; then {(f . x)} c= {y} by A11, A10, A9, A14, A24; then A26: f . x = y by ZFMISC_1:18; x in dom f by A11, A10, A9, A24, FUNCT_2:def_1; hence y in rng f by A26, FUNCT_1:def_3; ::_thesis: verum end; then reconsider f = f as Permutation of (dom F1) by A15, FUNCT_2:57; ( dom F1 = Seg (len F1) & dom (L (#) F1) = Seg (len (L (#) F1)) ) by FINSEQ_1:def_3; then reconsider f = f as Permutation of (dom (L (#) F1)) by A21; set G2 = L (#) F2; A27: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def_3; A28: len (L (#) F2) = len F2 by Def7; A29: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def_3; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(L_(#)_F2)_holds_ (L_(#)_F2)_._i_=_(L_(#)_F1)_._(f_._i) let i be Element of NAT ; ::_thesis: ( i in dom (L (#) F2) implies (L (#) F2) . i = (L (#) F1) . (f . i) ) assume A30: i in dom (L (#) F2) ; ::_thesis: (L (#) F2) . i = (L (#) F1) . (f . i) then reconsider u = F2 . i as VECTOR of V by A28, A9, A27, FUNCT_1:102; A31: ( (L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) & F2 . i = F2 /. i ) by A28, A9, A27, A30, Def7, PARTFUN1:def_6; i in dom f by A11, A21, A28, A29, A27, A30, FUNCT_2:def_1; then A32: f . i in dom F1 by A22, FUNCT_1:def_3; then reconsider m = f . i as Element of NAT ; reconsider v = F1 . m as VECTOR of V by A32, FUNCT_1:102; {(F1 . (f . i))} = Im (F1,(f . i)) by A32, FUNCT_1:59 .= F1 .: (F1 " {(F2 . i)}) by A11, A28, A10, A27, A14, A30 ; then A33: u = v by FUNCT_1:75, ZFMISC_1:18; F1 . m = F1 /. m by A32, PARTFUN1:def_6; hence (L (#) F2) . i = (L (#) F1) . (f . i) by A21, A10, A29, A32, A33, A31, Def7; ::_thesis: verum end; hence v1 = v2 by A3, A4, A5, A6, A7, A8, A21, A28, Th6, FINSEQ_1:48; ::_thesis: verum end; end; :: deftheorem Def8 defines Sum RLVECT_2:def_8_:_ for V being RealLinearSpace for L being Linear_Combination of V for b3 being Element of V holds ( b3 = Sum L iff ex F being FinSequence of V st ( F is one-to-one & rng F = Carrier L & b3 = Sum (L (#) F) ) ); Lm2: for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V proof let V be RealLinearSpace; ::_thesis: Sum (ZeroLC V) = 0. V consider F being FinSequence of V such that F is one-to-one and A1: rng F = Carrier (ZeroLC V) and A2: Sum (ZeroLC V) = Sum ((ZeroLC V) (#) F) by Def8; Carrier (ZeroLC V) = {} by Def5; then F = {} by A1, RELAT_1:41; then len F = 0 ; then len ((ZeroLC V) (#) F) = 0 by Def7; hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; ::_thesis: verum end; theorem :: RLVECT_2:29 for V being RealLinearSpace for A being Subset of V holds ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) proof let V be RealLinearSpace; ::_thesis: for A being Subset of V holds ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) let A be Subset of V; ::_thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) thus ( A <> {} & A is linearly-closed implies for l being Linear_Combination of A holds Sum l in A ) ::_thesis: ( ( for l being Linear_Combination of A holds Sum l in A ) implies ( A <> {} & A is linearly-closed ) ) proof defpred S1[ Element of NAT ] means for l being Linear_Combination of A st card (Carrier l) = $1 holds Sum l in A; assume that A1: A <> {} and A2: A is linearly-closed ; ::_thesis: for l being Linear_Combination of A holds Sum l in A now__::_thesis:_for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_0_holds_ Sum_l_in_A let l be Linear_Combination of A; ::_thesis: ( card (Carrier l) = 0 implies Sum l in A ) assume card (Carrier l) = 0 ; ::_thesis: Sum l in A then Carrier l = {} ; then l = ZeroLC V by Def5; then Sum l = 0. V by Lm2; hence Sum l in A by A1, A2, RLSUB_1:1; ::_thesis: verum end; then A3: S1[ 0 ] ; now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_k_holds_ Sum_l_in_A_)_holds_ for_l_being_Linear_Combination_of_A_st_card_(Carrier_l)_=_k_+_1_holds_ Sum_l_in_A let k be Element of NAT ; ::_thesis: ( ( for l being Linear_Combination of A st card (Carrier l) = k holds Sum l in A ) implies for l being Linear_Combination of A st card (Carrier l) = k + 1 holds Sum l in A ) assume A4: for l being Linear_Combination of A st card (Carrier l) = k holds Sum l in A ; ::_thesis: for l being Linear_Combination of A st card (Carrier l) = k + 1 holds Sum l in A let l be Linear_Combination of A; ::_thesis: ( card (Carrier l) = k + 1 implies Sum l in A ) deffunc H1( Element of V) -> Element of REAL = l . $1; consider F being FinSequence of V such that A5: F is one-to-one and A6: rng F = Carrier l and A7: Sum l = Sum (l (#) F) by Def8; reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18; assume A8: card (Carrier l) = k + 1 ; ::_thesis: Sum l in A then A9: len F = k + 1 by A5, A6, FINSEQ_4:62; then A10: len (l (#) F) = k + 1 by Def7; A11: k + 1 in Seg (k + 1) by FINSEQ_1:4; then A12: k + 1 in dom F by A9, FINSEQ_1:def_3; k + 1 in dom F by A9, A11, FINSEQ_1:def_3; then reconsider v = F . (k + 1) as VECTOR of V by FUNCT_1:102; consider f being Function of the carrier of V,REAL such that A13: f . v = 0 and A14: for u being Element of V st u <> v holds f . u = H1(u) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; A15: v in Carrier l by A6, A12, FUNCT_1:def_3; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_Carrier_l_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in Carrier l implies f . u = 0 ) assume A16: not u in Carrier l ; ::_thesis: f . u = 0 hence f . u = l . u by A15, A14 .= 0 by A16 ; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def3; A17: A \ {v} c= A by XBOOLE_1:36; A18: Carrier l c= A by Def6; then A19: (l . v) * v in A by A2, A15, RLSUB_1:def_1; A20: Carrier f = (Carrier l) \ {v} proof thus Carrier f c= (Carrier l) \ {v} :: according to XBOOLE_0:def_10 ::_thesis: (Carrier l) \ {v} c= Carrier f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in (Carrier l) \ {v} ) assume x in Carrier f ; ::_thesis: x in (Carrier l) \ {v} then consider u being VECTOR of V such that A21: u = x and A22: f . u <> 0 ; f . u = l . u by A13, A14, A22; then A23: x in Carrier l by A21, A22; not x in {v} by A13, A21, A22, TARSKI:def_1; hence x in (Carrier l) \ {v} by A23, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Carrier l) \ {v} or x in Carrier f ) assume A24: x in (Carrier l) \ {v} ; ::_thesis: x in Carrier f then x in Carrier l by XBOOLE_0:def_5; then consider u being VECTOR of V such that A25: x = u and A26: l . u <> 0 ; not x in {v} by A24, XBOOLE_0:def_5; then x <> v by TARSKI:def_1; then l . u = f . u by A14, A25; hence x in Carrier f by A25, A26; ::_thesis: verum end; then Carrier f c= A \ {v} by A18, XBOOLE_1:33; then Carrier f c= A by A17, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by Def6; A27: len G = k by A9, FINSEQ_3:53; then A28: len (f (#) G) = k by Def7; A29: rng G = Carrier f proof thus rng G c= Carrier f :: according to XBOOLE_0:def_10 ::_thesis: Carrier f c= rng G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in Carrier f ) assume x in rng G ; ::_thesis: x in Carrier f then consider y being set such that A30: y in dom G and A31: G . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A30; A32: ( dom G c= dom F & G . y = F . y ) by A30, FUNCT_1:47, RELAT_1:60; now__::_thesis:_not_x_=_v assume x = v ; ::_thesis: contradiction then A33: k + 1 = y by A5, A12, A30, A31, A32, FUNCT_1:def_4; y <= k by A27, A30, FINSEQ_3:25; hence contradiction by A33, XREAL_1:29; ::_thesis: verum end; then A34: not x in {v} by TARSKI:def_1; x in rng F by A30, A31, A32, FUNCT_1:def_3; hence x in Carrier f by A6, A20, A34, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in rng G ) assume A35: x in Carrier f ; ::_thesis: x in rng G then x in rng F by A6, A20, XBOOLE_0:def_5; then consider y being set such that A36: y in dom F and A37: F . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A36; now__::_thesis:_y_in_Seg_k assume not y in Seg k ; ::_thesis: contradiction then y in (dom F) \ (Seg k) by A36, XBOOLE_0:def_5; then y in (Seg (k + 1)) \ (Seg k) by A9, FINSEQ_1:def_3; then y in {(k + 1)} by FINSEQ_3:15; then y = k + 1 by TARSKI:def_1; then not v in {v} by A20, A35, A37, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then y in (dom F) /\ (Seg k) by A36, XBOOLE_0:def_4; then A38: y in dom G by RELAT_1:61; then G . y = F . y by FUNCT_1:47; hence x in rng G by A37, A38, FUNCT_1:def_3; ::_thesis: verum end; (Seg (k + 1)) /\ (Seg k) = Seg k by FINSEQ_1:7, NAT_1:12 .= dom (f (#) G) by A28, FINSEQ_1:def_3 ; then A39: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A10, FINSEQ_1:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_(f_(#)_G)_holds_ (f_(#)_G)_._x_=_(l_(#)_F)_._x let x be set ; ::_thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x ) assume A40: x in dom (f (#) G) ; ::_thesis: (f (#) G) . x = (l (#) F) . x then reconsider n = x as Element of NAT ; n in dom (l (#) F) by A39, A40, XBOOLE_0:def_4; then A41: n in dom F by A9, A10, FINSEQ_3:29; then F . n in rng F by FUNCT_1:def_3; then reconsider w = F . n as VECTOR of V ; A42: n in dom G by A27, A28, A40, FINSEQ_3:29; then A43: G . n in rng G by FUNCT_1:def_3; then reconsider u = G . n as VECTOR of V ; not u in {v} by A20, A29, A43, XBOOLE_0:def_5; then A44: u <> v by TARSKI:def_1; A45: (f (#) G) . n = (f . u) * u by A42, Th24 .= (l . u) * u by A14, A44 ; w = u by A42, FUNCT_1:47; hence (f (#) G) . x = (l (#) F) . x by A45, A41, Th24; ::_thesis: verum end; then A46: f (#) G = (l (#) F) | (Seg k) by A39, FUNCT_1:46; v in rng F by A12, FUNCT_1:def_3; then {v} c= Carrier l by A6, ZFMISC_1:31; then card (Carrier f) = (k + 1) - (card {v}) by A8, A20, CARD_2:44 .= (k + 1) - 1 by CARD_1:30 .= k ; then A47: Sum f in A by A4; G is one-to-one by A5, FUNCT_1:52; then A48: Sum (f (#) G) = Sum f by A29, Def8; ( dom (f (#) G) = Seg (len (f (#) G)) & (l (#) F) . (len F) = (l . v) * v ) by A9, A12, Th24, FINSEQ_1:def_3; then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by A9, A10, A28, A46, RLVECT_1:38; hence Sum l in A by A2, A7, A19, A48, A47, RLSUB_1:def_1; ::_thesis: verum end; then A49: for k being Element of NAT st S1[k] holds S1[k + 1] ; let l be Linear_Combination of A; ::_thesis: Sum l in A A50: card (Carrier l) = card (Carrier l) ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A49); hence Sum l in A by A50; ::_thesis: verum end; assume A51: for l being Linear_Combination of A holds Sum l in A ; ::_thesis: ( A <> {} & A is linearly-closed ) hence A <> {} ; ::_thesis: A is linearly-closed ( ZeroLC V is Linear_Combination of A & Sum (ZeroLC V) = 0. V ) by Lm2, Th22; then A52: 0. V in A by A51; A53: for a being Real for v being VECTOR of V st v in A holds a * v in A proof let a be Real; ::_thesis: for v being VECTOR of V st v in A holds a * v in A let v be VECTOR of V; ::_thesis: ( v in A implies a * v in A ) assume A54: v in A ; ::_thesis: a * v in A now__::_thesis:_a_*_v_in_A percases ( a = 0 or a <> 0 ) ; suppose a = 0 ; ::_thesis: a * v in A hence a * v in A by A52, RLVECT_1:10; ::_thesis: verum end; supposeA55: a <> 0 ; ::_thesis: a * v in A deffunc H1( Element of V) -> Element of NAT = 0 ; consider f being Function of the carrier of V,REAL such that A56: f . v = a and A57: for u being Element of V st u <> v holds f . u = H1(u) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {v} implies f . u = 0 ) assume not u in {v} ; ::_thesis: f . u = 0 then u <> v by TARSKI:def_1; hence f . u = 0 by A57; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def3; A58: Carrier f = {v} proof thus Carrier f c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= Carrier f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} ) assume x in Carrier f ; ::_thesis: x in {v} then consider u being VECTOR of V such that A59: x = u and A60: f . u <> 0 ; u = v by A57, A60; hence x in {v} by A59, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in Carrier f ) assume x in {v} ; ::_thesis: x in Carrier f then x = v by TARSKI:def_1; hence x in Carrier f by A55, A56; ::_thesis: verum end; {v} c= A by A54, ZFMISC_1:31; then reconsider f = f as Linear_Combination of A by A58, Def6; consider F being FinSequence of V such that A61: ( F is one-to-one & rng F = Carrier f ) and A62: Sum (f (#) F) = Sum f by Def8; F = <*v*> by A58, A61, FINSEQ_3:97; then f (#) F = <*((f . v) * v)*> by Th26; then Sum f = a * v by A56, A62, RLVECT_1:44; hence a * v in A by A51; ::_thesis: verum end; end; end; hence a * v in A ; ::_thesis: verum end; thus for v, u being VECTOR of V st v in A & u in A holds v + u in A :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of REAL for b2 being Element of the carrier of V holds ( not b2 in A or b1 * b2 in A ) proof let v, u be VECTOR of V; ::_thesis: ( v in A & u in A implies v + u in A ) assume that A63: v in A and A64: u in A ; ::_thesis: v + u in A now__::_thesis:_v_+_u_in_A percases ( u = v or v <> u ) ; suppose u = v ; ::_thesis: v + u in A then v + u = (1 * v) + v by RLVECT_1:def_8 .= (1 * v) + (1 * v) by RLVECT_1:def_8 .= (1 + 1) * v by RLVECT_1:def_6 .= 2 * v ; hence v + u in A by A53, A63; ::_thesis: verum end; supposeA65: v <> u ; ::_thesis: v + u in A deffunc H1( Element of V) -> Element of NAT = 0 ; consider f being Function of the carrier of V,REAL such that A66: ( f . v = 1 & f . u = 1 ) and A67: for w being Element of V st w <> v & w <> u holds f . w = H1(w) from FUNCT_2:sch_7(A65); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_w_being_VECTOR_of_V_st_not_w_in_{v,u}_holds_ f_._w_=_0 let w be VECTOR of V; ::_thesis: ( not w in {v,u} implies f . w = 0 ) assume not w in {v,u} ; ::_thesis: f . w = 0 then ( w <> v & w <> u ) by TARSKI:def_2; hence f . w = 0 by A67; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def3; A68: Carrier f = {v,u} proof thus Carrier f c= {v,u} :: according to XBOOLE_0:def_10 ::_thesis: {v,u} c= Carrier f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v,u} ) assume x in Carrier f ; ::_thesis: x in {v,u} then ex w being VECTOR of V st ( x = w & f . w <> 0 ) ; then ( x = v or x = u ) by A67; hence x in {v,u} by TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v,u} or x in Carrier f ) assume x in {v,u} ; ::_thesis: x in Carrier f then ( x = v or x = u ) by TARSKI:def_2; hence x in Carrier f by A66; ::_thesis: verum end; then A69: Carrier f c= A by A63, A64, ZFMISC_1:32; A70: ( 1 * u = u & 1 * v = v ) by RLVECT_1:def_8; reconsider f = f as Linear_Combination of A by A69, Def6; consider F being FinSequence of V such that A71: ( F is one-to-one & rng F = Carrier f ) and A72: Sum (f (#) F) = Sum f by Def8; ( F = <*v,u*> or F = <*u,v*> ) by A65, A68, A71, FINSEQ_3:99; then ( f (#) F = <*(1 * v),(1 * u)*> or f (#) F = <*(1 * u),(1 * v)*> ) by A66, Th27; then Sum f = v + u by A72, A70, RLVECT_1:45; hence v + u in A by A51; ::_thesis: verum end; end; end; hence v + u in A ; ::_thesis: verum end; thus for b1 being Element of REAL for b2 being Element of the carrier of V holds ( not b2 in A or b1 * b2 in A ) by A53; ::_thesis: verum end; theorem :: RLVECT_2:30 for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V by Lm2; theorem :: RLVECT_2:31 for V being RealLinearSpace for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V proof let V be RealLinearSpace; ::_thesis: for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V let l be Linear_Combination of {} the carrier of V; ::_thesis: Sum l = 0. V l = ZeroLC V by Th23; hence Sum l = 0. V by Lm2; ::_thesis: verum end; theorem Th32: :: RLVECT_2:32 for V being RealLinearSpace for v being VECTOR of V for l being Linear_Combination of {v} holds Sum l = (l . v) * v proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for l being Linear_Combination of {v} holds Sum l = (l . v) * v let v be VECTOR of V; ::_thesis: for l being Linear_Combination of {v} holds Sum l = (l . v) * v let l be Linear_Combination of {v}; ::_thesis: Sum l = (l . v) * v A1: Carrier l c= {v} by Def6; now__::_thesis:_Sum_l_=_(l_._v)_*_v percases ( Carrier l = {} or Carrier l = {v} ) by A1, ZFMISC_1:33; suppose Carrier l = {} ; ::_thesis: Sum l = (l . v) * v then A2: l = ZeroLC V by Def5; hence Sum l = 0. V by Lm2 .= 0 * v by RLVECT_1:10 .= (l . v) * v by A2, Th20 ; ::_thesis: verum end; suppose Carrier l = {v} ; ::_thesis: Sum l = (l . v) * v then consider F being FinSequence of V such that A3: ( F is one-to-one & rng F = {v} ) and A4: Sum l = Sum (l (#) F) by Def8; F = <*v*> by A3, FINSEQ_3:97; then l (#) F = <*((l . v) * v)*> by Th26; hence Sum l = (l . v) * v by A4, RLVECT_1:44; ::_thesis: verum end; end; end; hence Sum l = (l . v) * v ; ::_thesis: verum end; theorem Th33: :: RLVECT_2:33 for V being RealLinearSpace for v1, v2 being VECTOR of V st v1 <> v2 holds for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) proof let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V st v1 <> v2 holds for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) let v1, v2 be VECTOR of V; ::_thesis: ( v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) ) assume A1: v1 <> v2 ; ::_thesis: for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) let l be Linear_Combination of {v1,v2}; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) A2: Carrier l c= {v1,v2} by Def6; now__::_thesis:_Sum_l_=_((l_._v1)_*_v1)_+_((l_._v2)_*_v2) percases ( Carrier l = {} or Carrier l = {v1} or Carrier l = {v2} or Carrier l = {v1,v2} ) by A2, ZFMISC_1:36; suppose Carrier l = {} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) then A3: l = ZeroLC V by Def5; hence Sum l = 0. V by Lm2 .= (0. V) + (0. V) by RLVECT_1:4 .= (0 * v1) + (0. V) by RLVECT_1:10 .= (0 * v1) + (0 * v2) by RLVECT_1:10 .= ((l . v1) * v1) + (0 * v2) by A3, Th20 .= ((l . v1) * v1) + ((l . v2) * v2) by A3, Th20 ; ::_thesis: verum end; supposeA4: Carrier l = {v1} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) then reconsider L = l as Linear_Combination of {v1} by Def6; A5: not v2 in Carrier l by A1, A4, TARSKI:def_1; thus Sum l = Sum L .= (l . v1) * v1 by Th32 .= ((l . v1) * v1) + (0. V) by RLVECT_1:4 .= ((l . v1) * v1) + (0 * v2) by RLVECT_1:10 .= ((l . v1) * v1) + ((l . v2) * v2) by A5 ; ::_thesis: verum end; supposeA6: Carrier l = {v2} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) then reconsider L = l as Linear_Combination of {v2} by Def6; A7: not v1 in Carrier l by A1, A6, TARSKI:def_1; thus Sum l = Sum L .= (l . v2) * v2 by Th32 .= (0. V) + ((l . v2) * v2) by RLVECT_1:4 .= (0 * v1) + ((l . v2) * v2) by RLVECT_1:10 .= ((l . v1) * v1) + ((l . v2) * v2) by A7 ; ::_thesis: verum end; suppose Carrier l = {v1,v2} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2) then consider F being FinSequence of V such that A8: ( F is one-to-one & rng F = {v1,v2} ) and A9: Sum l = Sum (l (#) F) by Def8; ( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A8, FINSEQ_3:99; then ( l (#) F = <*((l . v1) * v1),((l . v2) * v2)*> or l (#) F = <*((l . v2) * v2),((l . v1) * v1)*> ) by Th27; hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A9, RLVECT_1:45; ::_thesis: verum end; end; end; hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) ; ::_thesis: verum end; theorem :: RLVECT_2:34 for V being RealLinearSpace for L being Linear_Combination of V st Carrier L = {} holds Sum L = 0. V proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st Carrier L = {} holds Sum L = 0. V let L be Linear_Combination of V; ::_thesis: ( Carrier L = {} implies Sum L = 0. V ) assume Carrier L = {} ; ::_thesis: Sum L = 0. V then L = ZeroLC V by Def5; hence Sum L = 0. V by Lm2; ::_thesis: verum end; theorem :: RLVECT_2:35 for V being RealLinearSpace for v being VECTOR of V for L being Linear_Combination of V st Carrier L = {v} holds Sum L = (L . v) * v proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for L being Linear_Combination of V st Carrier L = {v} holds Sum L = (L . v) * v let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v} holds Sum L = (L . v) * v let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v} implies Sum L = (L . v) * v ) assume Carrier L = {v} ; ::_thesis: Sum L = (L . v) * v then L is Linear_Combination of {v} by Def6; hence Sum L = (L . v) * v by Th32; ::_thesis: verum end; theorem :: RLVECT_2:36 for V being RealLinearSpace for v1, v2 being VECTOR of V for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = ((L . v1) * v1) + ((L . v2) * v2) proof let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = ((L . v1) * v1) + ((L . v2) * v2) let v1, v2 be VECTOR of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds Sum L = ((L . v1) * v1) + ((L . v2) * v2) let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v1,v2} & v1 <> v2 implies Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) assume that A1: Carrier L = {v1,v2} and A2: v1 <> v2 ; ::_thesis: Sum L = ((L . v1) * v1) + ((L . v2) * v2) L is Linear_Combination of {v1,v2} by A1, Def6; hence Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A2, Th33; ::_thesis: verum end; definition let V be non empty addLoopStr ; let L1, L2 be Linear_Combination of V; :: original: = redefine predL1 = L2 means :: RLVECT_2:def 9 for v being Element of V holds L1 . v = L2 . v; compatibility ( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63; end; :: deftheorem defines = RLVECT_2:def_9_:_ for V being non empty addLoopStr for L1, L2 being Linear_Combination of V holds ( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ); definition let V be non empty addLoopStr ; let L1, L2 be Linear_Combination of V; :: original: + redefine funcL1 + L2 -> Linear_Combination of V means :Def10: :: RLVECT_2:def 10 for v being Element of V holds it . v = (L1 . v) + (L2 . v); coherence L1 + L2 is Linear_Combination of V proof reconsider f = L1 + L2 as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_(Carrier_L1)_\/_(Carrier_L2)_holds_ f_._v_=_0 let v be Element of V; ::_thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies f . v = 0 ) assume A1: not v in (Carrier L1) \/ (Carrier L2) ; ::_thesis: f . v = 0 then not v in Carrier L2 by XBOOLE_0:def_3; then A2: L2 . v = 0 ; not v in Carrier L1 by A1, XBOOLE_0:def_3; then L1 . v = 0 ; hence f . v = 0 + 0 by A2, VALUED_1:1 .= 0 ; ::_thesis: verum end; hence L1 + L2 is Linear_Combination of V by Def3; ::_thesis: verum end; compatibility for b1 being Linear_Combination of V holds ( b1 = L1 + L2 iff for v being Element of V holds b1 . v = (L1 . v) + (L2 . v) ) proof let f be Linear_Combination of V; ::_thesis: ( f = L1 + L2 iff for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) thus ( f = L1 + L2 implies for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) by VALUED_1:1; ::_thesis: ( ( for v being Element of V holds f . v = (L1 . v) + (L2 . v) ) implies f = L1 + L2 ) assume A3: for v being Element of V holds f . v = (L1 . v) + (L2 . v) ; ::_thesis: f = L1 + L2 thus f = L1 + L2 ::_thesis: verum proof let v be Element of the carrier of V; :: according to FUNCT_2:def_8 ::_thesis: f . v = (L1 + L2) . v thus f . v = (L1 . v) + (L2 . v) by A3 .= (L1 + L2) . v by VALUED_1:1 ; ::_thesis: verum end; end; end; :: deftheorem Def10 defines + RLVECT_2:def_10_:_ for V being non empty addLoopStr for L1, L2, b4 being Linear_Combination of V holds ( b4 = L1 + L2 iff for v being Element of V holds b4 . v = (L1 . v) + (L2 . v) ); theorem Th37: :: RLVECT_2:37 for V being RealLinearSpace for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) proof let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) let L1, L2 be Linear_Combination of V; ::_thesis: Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (L1 + L2) or x in (Carrier L1) \/ (Carrier L2) ) assume x in Carrier (L1 + L2) ; ::_thesis: x in (Carrier L1) \/ (Carrier L2) then consider u being VECTOR of V such that A1: x = u and A2: (L1 + L2) . u <> 0 ; (L1 + L2) . u = (L1 . u) + (L2 . u) by Def10; then ( L1 . u <> 0 or L2 . u <> 0 ) by A2; then ( x in { v1 where v1 is VECTOR of V : L1 . v1 <> 0 } or x in { v2 where v2 is VECTOR of V : L2 . v2 <> 0 } ) by A1; hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th38: :: RLVECT_2:38 for V being RealLinearSpace for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 + L2 is Linear_Combination of A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 + L2 is Linear_Combination of A let A be Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 + L2 is Linear_Combination of A let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 + L2 is Linear_Combination of A ) assume ( L1 is Linear_Combination of A & L2 is Linear_Combination of A ) ; ::_thesis: L1 + L2 is Linear_Combination of A then ( Carrier L1 c= A & Carrier L2 c= A ) by Def6; then A1: (Carrier L1) \/ (Carrier L2) c= A by XBOOLE_1:8; Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by Th37; hence Carrier (L1 + L2) c= A by A1, XBOOLE_1:1; :: according to RLVECT_2:def_6 ::_thesis: verum end; theorem :: RLVECT_2:39 for V being non empty addLoopStr for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 ; theorem Th40: :: RLVECT_2:40 for V being RealLinearSpace for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 proof let V be RealLinearSpace; ::_thesis: for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 let L1, L2, L3 be Linear_Combination of V; ::_thesis: L1 + (L2 + L3) = (L1 + L2) + L3 let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (L1 + (L2 + L3)) . v = ((L1 + L2) + L3) . v thus (L1 + (L2 + L3)) . v = (L1 . v) + ((L2 + L3) . v) by Def10 .= (L1 . v) + ((L2 . v) + (L3 . v)) by Def10 .= ((L1 . v) + (L2 . v)) + (L3 . v) .= ((L1 + L2) . v) + (L3 . v) by Def10 .= ((L1 + L2) + L3) . v by Def10 ; ::_thesis: verum end; theorem Th41: :: RLVECT_2:41 for V being RealLinearSpace for L being Linear_Combination of V holds ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) let L be Linear_Combination of V; ::_thesis: ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) thus L + (ZeroLC V) = L ::_thesis: (ZeroLC V) + L = L proof let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (L + (ZeroLC V)) . v = L . v thus (L + (ZeroLC V)) . v = (L . v) + ((ZeroLC V) . v) by Def10 .= (L . v) + 0 by Th20 .= L . v ; ::_thesis: verum end; hence (ZeroLC V) + L = L ; ::_thesis: verum end; definition let V be RealLinearSpace; let a be Real; let L be Linear_Combination of V; funca * L -> Linear_Combination of V means :Def11: :: RLVECT_2:def 11 for v being VECTOR of V holds it . v = a * (L . v); existence ex b1 being Linear_Combination of V st for v being VECTOR of V holds b1 . v = a * (L . v) proof deffunc H1( Element of V) -> Element of REAL = a * (L . $1); consider f being Function of the carrier of V,REAL such that A1: for v being Element of V holds f . v = H1(v) from FUNCT_2:sch_4(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_Carrier_L_holds_ f_._v_=_0 let v be VECTOR of V; ::_thesis: ( not v in Carrier L implies f . v = 0 ) assume not v in Carrier L ; ::_thesis: f . v = 0 then L . v = 0 ; hence f . v = a * 0 by A1 .= 0 ; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def3; take f ; ::_thesis: for v being VECTOR of V holds f . v = a * (L . v) let v be VECTOR of V; ::_thesis: f . v = a * (L . v) thus f . v = a * (L . v) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Linear_Combination of V st ( for v being VECTOR of V holds b1 . v = a * (L . v) ) & ( for v being VECTOR of V holds b2 . v = a * (L . v) ) holds b1 = b2 proof let L1, L2 be Linear_Combination of V; ::_thesis: ( ( for v being VECTOR of V holds L1 . v = a * (L . v) ) & ( for v being VECTOR of V holds L2 . v = a * (L . v) ) implies L1 = L2 ) assume A2: for v being VECTOR of V holds L1 . v = a * (L . v) ; ::_thesis: ( ex v being VECTOR of V st not L2 . v = a * (L . v) or L1 = L2 ) assume A3: for v being VECTOR of V holds L2 . v = a * (L . v) ; ::_thesis: L1 = L2 let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: L1 . v = L2 . v thus L1 . v = a * (L . v) by A2 .= L2 . v by A3 ; ::_thesis: verum end; end; :: deftheorem Def11 defines * RLVECT_2:def_11_:_ for V being RealLinearSpace for a being Real for L, b4 being Linear_Combination of V holds ( b4 = a * L iff for v being VECTOR of V holds b4 . v = a * (L . v) ); theorem Th42: :: RLVECT_2:42 for V being RealLinearSpace for a being Real for L being Linear_Combination of V st a <> 0 holds Carrier (a * L) = Carrier L proof let V be RealLinearSpace; ::_thesis: for a being Real for L being Linear_Combination of V st a <> 0 holds Carrier (a * L) = Carrier L let a be Real; ::_thesis: for L being Linear_Combination of V st a <> 0 holds Carrier (a * L) = Carrier L let L be Linear_Combination of V; ::_thesis: ( a <> 0 implies Carrier (a * L) = Carrier L ) set T = { u where u is VECTOR of V : (a * L) . u <> 0 } ; set S = { v where v is VECTOR of V : L . v <> 0 } ; assume A1: a <> 0 ; ::_thesis: Carrier (a * L) = Carrier L { u where u is VECTOR of V : (a * L) . u <> 0 } = { v where v is VECTOR of V : L . v <> 0 } proof thus { u where u is VECTOR of V : (a * L) . u <> 0 } c= { v where v is VECTOR of V : L . v <> 0 } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is VECTOR of V : L . v <> 0 } c= { u where u is VECTOR of V : (a * L) . u <> 0 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is VECTOR of V : (a * L) . u <> 0 } or x in { v where v is VECTOR of V : L . v <> 0 } ) assume x in { u where u is VECTOR of V : (a * L) . u <> 0 } ; ::_thesis: x in { v where v is VECTOR of V : L . v <> 0 } then consider u being VECTOR of V such that A2: x = u and A3: (a * L) . u <> 0 ; (a * L) . u = a * (L . u) by Def11; then L . u <> 0 by A3; hence x in { v where v is VECTOR of V : L . v <> 0 } by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is VECTOR of V : L . v <> 0 } or x in { u where u is VECTOR of V : (a * L) . u <> 0 } ) assume x in { v where v is VECTOR of V : L . v <> 0 } ; ::_thesis: x in { u where u is VECTOR of V : (a * L) . u <> 0 } then consider v being VECTOR of V such that A4: x = v and A5: L . v <> 0 ; (a * L) . v = a * (L . v) by Def11; then (a * L) . v <> 0 by A1, A5, XCMPLX_1:6; hence x in { u where u is VECTOR of V : (a * L) . u <> 0 } by A4; ::_thesis: verum end; hence Carrier (a * L) = Carrier L ; ::_thesis: verum end; theorem Th43: :: RLVECT_2:43 for V being RealLinearSpace for L being Linear_Combination of V holds 0 * L = ZeroLC V proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds 0 * L = ZeroLC V let L be Linear_Combination of V; ::_thesis: 0 * L = ZeroLC V let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (0 * L) . v = (ZeroLC V) . v thus (0 * L) . v = 0 * (L . v) by Def11 .= (ZeroLC V) . v by Th20 ; ::_thesis: verum end; theorem Th44: :: RLVECT_2:44 for V being RealLinearSpace for a being Real for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds a * L is Linear_Combination of A proof let V be RealLinearSpace; ::_thesis: for a being Real for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds a * L is Linear_Combination of A let a be Real; ::_thesis: for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds a * L is Linear_Combination of A let A be Subset of V; ::_thesis: for L being Linear_Combination of V st L is Linear_Combination of A holds a * L is Linear_Combination of A let L be Linear_Combination of V; ::_thesis: ( L is Linear_Combination of A implies a * L is Linear_Combination of A ) assume A1: L is Linear_Combination of A ; ::_thesis: a * L is Linear_Combination of A now__::_thesis:_a_*_L_is_Linear_Combination_of_A percases ( a = 0 or a <> 0 ) ; suppose a = 0 ; ::_thesis: a * L is Linear_Combination of A then a * L = ZeroLC V by Th43; hence a * L is Linear_Combination of A by Th22; ::_thesis: verum end; suppose a <> 0 ; ::_thesis: a * L is Linear_Combination of A then Carrier (a * L) = Carrier L by Th42; hence a * L is Linear_Combination of A by A1, Def6; ::_thesis: verum end; end; end; hence a * L is Linear_Combination of A ; ::_thesis: verum end; theorem Th45: :: RLVECT_2:45 for V being RealLinearSpace for a, b being Real for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) proof let V be RealLinearSpace; ::_thesis: for a, b being Real for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) let a, b be Real; ::_thesis: for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) let L be Linear_Combination of V; ::_thesis: (a + b) * L = (a * L) + (b * L) let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: ((a + b) * L) . v = ((a * L) + (b * L)) . v thus ((a + b) * L) . v = (a + b) * (L . v) by Def11 .= (a * (L . v)) + (b * (L . v)) .= ((a * L) . v) + (b * (L . v)) by Def11 .= ((a * L) . v) + ((b * L) . v) by Def11 .= ((a * L) + (b * L)) . v by Def10 ; ::_thesis: verum end; theorem Th46: :: RLVECT_2:46 for V being RealLinearSpace for a being Real for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) proof let V be RealLinearSpace; ::_thesis: for a being Real for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) let a be Real; ::_thesis: for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) let L1, L2 be Linear_Combination of V; ::_thesis: a * (L1 + L2) = (a * L1) + (a * L2) let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (a * (L1 + L2)) . v = ((a * L1) + (a * L2)) . v thus (a * (L1 + L2)) . v = a * ((L1 + L2) . v) by Def11 .= a * ((L1 . v) + (L2 . v)) by Def10 .= (a * (L1 . v)) + (a * (L2 . v)) .= ((a * L1) . v) + (a * (L2 . v)) by Def11 .= ((a * L1) . v) + ((a * L2) . v) by Def11 .= ((a * L1) + (a * L2)) . v by Def10 ; ::_thesis: verum end; theorem Th47: :: RLVECT_2:47 for V being RealLinearSpace for a, b being Real for L being Linear_Combination of V holds a * (b * L) = (a * b) * L proof let V be RealLinearSpace; ::_thesis: for a, b being Real for L being Linear_Combination of V holds a * (b * L) = (a * b) * L let a, b be Real; ::_thesis: for L being Linear_Combination of V holds a * (b * L) = (a * b) * L let L be Linear_Combination of V; ::_thesis: a * (b * L) = (a * b) * L let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (a * (b * L)) . v = ((a * b) * L) . v thus (a * (b * L)) . v = a * ((b * L) . v) by Def11 .= a * (b * (L . v)) by Def11 .= (a * b) * (L . v) .= ((a * b) * L) . v by Def11 ; ::_thesis: verum end; theorem Th48: :: RLVECT_2:48 for V being RealLinearSpace for L being Linear_Combination of V holds 1 * L = L proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds 1 * L = L let L be Linear_Combination of V; ::_thesis: 1 * L = L let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (1 * L) . v = L . v thus (1 * L) . v = 1 * (L . v) by Def11 .= L . v ; ::_thesis: verum end; definition let V be RealLinearSpace; let L be Linear_Combination of V; func - L -> Linear_Combination of V equals :: RLVECT_2:def 12 (- 1) * L; correctness coherence (- 1) * L is Linear_Combination of V; ; end; :: deftheorem defines - RLVECT_2:def_12_:_ for V being RealLinearSpace for L being Linear_Combination of V holds - L = (- 1) * L; theorem Th49: :: RLVECT_2:49 for V being RealLinearSpace for v being VECTOR of V for L being Linear_Combination of V holds (- L) . v = - (L . v) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for L being Linear_Combination of V holds (- L) . v = - (L . v) let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V holds (- L) . v = - (L . v) let L be Linear_Combination of V; ::_thesis: (- L) . v = - (L . v) thus (- L) . v = (- 1) * (L . v) by Def11 .= - (L . v) ; ::_thesis: verum end; theorem :: RLVECT_2:50 for V being RealLinearSpace for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds L2 = - L1 proof let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds L2 = - L1 let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 + L2 = ZeroLC V implies L2 = - L1 ) assume A1: L1 + L2 = ZeroLC V ; ::_thesis: L2 = - L1 let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: L2 . v = (- L1) . v (L1 . v) + (L2 . v) = (ZeroLC V) . v by A1, Def10 .= 0 by Th20 ; hence L2 . v = - (L1 . v) .= (- L1) . v by Th49 ; ::_thesis: verum end; theorem :: RLVECT_2:51 for V being RealLinearSpace for L being Linear_Combination of V holds Carrier (- L) = Carrier L by Th42; theorem :: RLVECT_2:52 for V being RealLinearSpace for A being Subset of V for L being Linear_Combination of V st L is Linear_Combination of A holds - L is Linear_Combination of A by Th44; theorem :: RLVECT_2:53 for V being RealLinearSpace for L being Linear_Combination of V holds - (- L) = L proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds - (- L) = L let L be Linear_Combination of V; ::_thesis: - (- L) = L let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (- (- L)) . v = L . v thus (- (- L)) . v = (((- 1) * (- 1)) * L) . v by Th47 .= 1 * (L . v) by Def11 .= L . v ; ::_thesis: verum end; definition let V be RealLinearSpace; let L1, L2 be Linear_Combination of V; funcL1 - L2 -> Linear_Combination of V equals :: RLVECT_2:def 13 L1 + (- L2); correctness coherence L1 + (- L2) is Linear_Combination of V; ; end; :: deftheorem defines - RLVECT_2:def_13_:_ for V being RealLinearSpace for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2); theorem Th54: :: RLVECT_2:54 for V being RealLinearSpace for v being VECTOR of V for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let v be VECTOR of V; ::_thesis: for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let L1, L2 be Linear_Combination of V; ::_thesis: (L1 - L2) . v = (L1 . v) - (L2 . v) thus (L1 - L2) . v = (L1 . v) + ((- L2) . v) by Def10 .= (L1 . v) + (- (L2 . v)) by Th49 .= (L1 . v) - (L2 . v) ; ::_thesis: verum end; theorem :: RLVECT_2:55 for V being RealLinearSpace for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) proof let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) let L1, L2 be Linear_Combination of V; ::_thesis: Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier (- L2)) by Th37; hence Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by Th42; ::_thesis: verum end; theorem :: RLVECT_2:56 for V being RealLinearSpace for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 - L2 is Linear_Combination of A proof let V be RealLinearSpace; ::_thesis: for A being Subset of V for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 - L2 is Linear_Combination of A let A be Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds L1 - L2 is Linear_Combination of A let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 - L2 is Linear_Combination of A ) assume that A1: L1 is Linear_Combination of A and A2: L2 is Linear_Combination of A ; ::_thesis: L1 - L2 is Linear_Combination of A - L2 is Linear_Combination of A by A2, Th44; hence L1 - L2 is Linear_Combination of A by A1, Th38; ::_thesis: verum end; theorem Th57: :: RLVECT_2:57 for V being RealLinearSpace for L being Linear_Combination of V holds L - L = ZeroLC V proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds L - L = ZeroLC V let L be Linear_Combination of V; ::_thesis: L - L = ZeroLC V let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (L - L) . v = (ZeroLC V) . v thus (L - L) . v = (L . v) - (L . v) by Th54 .= (ZeroLC V) . v by Th20 ; ::_thesis: verum end; definition let V be RealLinearSpace; func LinComb V -> set means :Def14: :: RLVECT_2:def 14 for x being set holds ( x in it iff x is Linear_Combination of V ); existence ex b1 being set st for x being set holds ( x in b1 iff x is Linear_Combination of V ) proof defpred S1[ set ] means $1 is Linear_Combination of V; consider A being set such that A1: for x being set holds ( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for x being set holds ( x in A iff x is Linear_Combination of V ) let x be set ; ::_thesis: ( x in A iff x is Linear_Combination of V ) thus ( x in A implies x is Linear_Combination of V ) by A1; ::_thesis: ( x is Linear_Combination of V implies x in A ) assume x is Linear_Combination of V ; ::_thesis: x in A hence x in A by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is Linear_Combination of V ) ) & ( for x being set holds ( x in b2 iff x is Linear_Combination of V ) ) holds b1 = b2 proof let D1, D2 be set ; ::_thesis: ( ( for x being set holds ( x in D1 iff x is Linear_Combination of V ) ) & ( for x being set holds ( x in D2 iff x is Linear_Combination of V ) ) implies D1 = D2 ) assume A2: for x being set holds ( x in D1 iff x is Linear_Combination of V ) ; ::_thesis: ( ex x being set st ( ( x in D2 implies x is Linear_Combination of V ) implies ( x is Linear_Combination of V & not x in D2 ) ) or D1 = D2 ) assume A3: for x being set holds ( x in D2 iff x is Linear_Combination of V ) ; ::_thesis: D1 = D2 thus D1 c= D2 :: according to XBOOLE_0:def_10 ::_thesis: D2 c= D1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in D2 ) assume x in D1 ; ::_thesis: x in D2 then x is Linear_Combination of V by A2; hence x in D2 by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in D1 ) assume x in D2 ; ::_thesis: x in D1 then x is Linear_Combination of V by A3; hence x in D1 by A2; ::_thesis: verum end; end; :: deftheorem Def14 defines LinComb RLVECT_2:def_14_:_ for V being RealLinearSpace for b2 being set holds ( b2 = LinComb V iff for x being set holds ( x in b2 iff x is Linear_Combination of V ) ); registration let V be RealLinearSpace; cluster LinComb V -> non empty ; coherence not LinComb V is empty proof set x = the Linear_Combination of V; the Linear_Combination of V in LinComb V by Def14; hence not LinComb V is empty ; ::_thesis: verum end; end; definition let V be RealLinearSpace; let e be Element of LinComb V; func @ e -> Linear_Combination of V equals :: RLVECT_2:def 15 e; coherence e is Linear_Combination of V by Def14; end; :: deftheorem defines @ RLVECT_2:def_15_:_ for V being RealLinearSpace for e being Element of LinComb V holds @ e = e; definition let V be RealLinearSpace; let L be Linear_Combination of V; func @ L -> Element of LinComb V equals :: RLVECT_2:def 16 L; coherence L is Element of LinComb V by Def14; end; :: deftheorem defines @ RLVECT_2:def_16_:_ for V being RealLinearSpace for L being Linear_Combination of V holds @ L = L; definition let V be RealLinearSpace; func LCAdd V -> BinOp of (LinComb V) means :Def17: :: RLVECT_2:def 17 for e1, e2 being Element of LinComb V holds it . (e1,e2) = (@ e1) + (@ e2); existence ex b1 being BinOp of (LinComb V) st for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2) proof deffunc H1( Element of LinComb V, Element of LinComb V) -> Element of LinComb V = @ ((@ $1) + (@ $2)); consider o being BinOp of (LinComb V) such that A1: for e1, e2 being Element of LinComb V holds o . (e1,e2) = H1(e1,e2) from BINOP_1:sch_4(); take o ; ::_thesis: for e1, e2 being Element of LinComb V holds o . (e1,e2) = (@ e1) + (@ e2) let e1, e2 be Element of LinComb V; ::_thesis: o . (e1,e2) = (@ e1) + (@ e2) thus o . (e1,e2) = @ ((@ e1) + (@ e2)) by A1 .= (@ e1) + (@ e2) ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (LinComb V) st ( for e1, e2 being Element of LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) ) holds b1 = b2 proof let o1, o2 be BinOp of (LinComb V); ::_thesis: ( ( for e1, e2 being Element of LinComb V holds o1 . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of LinComb V holds o2 . (e1,e2) = (@ e1) + (@ e2) ) implies o1 = o2 ) assume A2: for e1, e2 being Element of LinComb V holds o1 . (e1,e2) = (@ e1) + (@ e2) ; ::_thesis: ( ex e1, e2 being Element of LinComb V st not o2 . (e1,e2) = (@ e1) + (@ e2) or o1 = o2 ) assume A3: for e1, e2 being Element of LinComb V holds o2 . (e1,e2) = (@ e1) + (@ e2) ; ::_thesis: o1 = o2 now__::_thesis:_for_e1,_e2_being_Element_of_LinComb_V_holds_o1_._(e1,e2)_=_o2_._(e1,e2) let e1, e2 be Element of LinComb V; ::_thesis: o1 . (e1,e2) = o2 . (e1,e2) thus o1 . (e1,e2) = (@ e1) + (@ e2) by A2 .= o2 . (e1,e2) by A3 ; ::_thesis: verum end; hence o1 = o2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def17 defines LCAdd RLVECT_2:def_17_:_ for V being RealLinearSpace for b2 being BinOp of (LinComb V) holds ( b2 = LCAdd V iff for e1, e2 being Element of LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) ); definition let V be RealLinearSpace; func LCMult V -> Function of [:REAL,(LinComb V):],(LinComb V) means :Def18: :: RLVECT_2:def 18 for a being Real for e being Element of LinComb V holds it . [a,e] = a * (@ e); existence ex b1 being Function of [:REAL,(LinComb V):],(LinComb V) st for a being Real for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) proof defpred S1[ Element of REAL , Element of LinComb V, set ] means ex a being Real st ( a = $1 & $3 = a * (@ $2) ); A1: for x being Element of REAL for e1 being Element of LinComb V ex e2 being Element of LinComb V st S1[x,e1,e2] proof let x be Element of REAL ; ::_thesis: for e1 being Element of LinComb V ex e2 being Element of LinComb V st S1[x,e1,e2] let e1 be Element of LinComb V; ::_thesis: ex e2 being Element of LinComb V st S1[x,e1,e2] take @ (x * (@ e1)) ; ::_thesis: S1[x,e1, @ (x * (@ e1))] take x ; ::_thesis: ( x = x & @ (x * (@ e1)) = x * (@ e1) ) thus ( x = x & @ (x * (@ e1)) = x * (@ e1) ) ; ::_thesis: verum end; consider g being Function of [:REAL,(LinComb V):],(LinComb V) such that A2: for x being Element of REAL for e being Element of LinComb V holds S1[x,e,g . (x,e)] from BINOP_1:sch_3(A1); take g ; ::_thesis: for a being Real for e being Element of LinComb V holds g . [a,e] = a * (@ e) let a be Real; ::_thesis: for e being Element of LinComb V holds g . [a,e] = a * (@ e) let e be Element of LinComb V; ::_thesis: g . [a,e] = a * (@ e) ex b being Real st ( b = a & g . (a,e) = b * (@ e) ) by A2; hence g . [a,e] = a * (@ e) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:REAL,(LinComb V):],(LinComb V) st ( for a being Real for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) ) & ( for a being Real for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) ) holds b1 = b2 proof let g1, g2 be Function of [:REAL,(LinComb V):],(LinComb V); ::_thesis: ( ( for a being Real for e being Element of LinComb V holds g1 . [a,e] = a * (@ e) ) & ( for a being Real for e being Element of LinComb V holds g2 . [a,e] = a * (@ e) ) implies g1 = g2 ) assume A3: for a being Real for e being Element of LinComb V holds g1 . [a,e] = a * (@ e) ; ::_thesis: ( ex a being Real ex e being Element of LinComb V st not g2 . [a,e] = a * (@ e) or g1 = g2 ) assume A4: for a being Real for e being Element of LinComb V holds g2 . [a,e] = a * (@ e) ; ::_thesis: g1 = g2 now__::_thesis:_for_x_being_Element_of_REAL_ for_e_being_Element_of_LinComb_V_holds_g1_._(x,e)_=_g2_._(x,e) let x be Element of REAL ; ::_thesis: for e being Element of LinComb V holds g1 . (x,e) = g2 . (x,e) let e be Element of LinComb V; ::_thesis: g1 . (x,e) = g2 . (x,e) thus g1 . (x,e) = x * (@ e) by A3 .= g2 . (x,e) by A4 ; ::_thesis: verum end; hence g1 = g2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def18 defines LCMult RLVECT_2:def_18_:_ for V being RealLinearSpace for b2 being Function of [:REAL,(LinComb V):],(LinComb V) holds ( b2 = LCMult V iff for a being Real for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) ); definition let V be RealLinearSpace; func LC_RLSpace V -> RLSStruct equals :: RLVECT_2:def 19 RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #); coherence RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #) is RLSStruct ; end; :: deftheorem defines LC_RLSpace RLVECT_2:def_19_:_ for V being RealLinearSpace holds LC_RLSpace V = RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #); registration let V be RealLinearSpace; cluster LC_RLSpace V -> non empty strict ; coherence ( LC_RLSpace V is strict & not LC_RLSpace V is empty ) ; end; registration let V be RealLinearSpace; cluster LC_RLSpace V -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( LC_RLSpace V is Abelian & LC_RLSpace V is add-associative & LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital ) proof set S = LC_RLSpace V; A1: now__::_thesis:_for_v,_u_being_VECTOR_of_(LC_RLSpace_V) for_K,_L_being_Linear_Combination_of_V_st_v_=_K_&_u_=_L_holds_ v_+_u_=_K_+_L let v, u be VECTOR of (LC_RLSpace V); ::_thesis: for K, L being Linear_Combination of V st v = K & u = L holds v + u = K + L let K, L be Linear_Combination of V; ::_thesis: ( v = K & u = L implies v + u = K + L ) A2: ( @ (@ K) = K & @ (@ L) = L ) ; assume ( v = K & u = L ) ; ::_thesis: v + u = K + L hence v + u = K + L by A2, Def17; ::_thesis: verum end; thus LC_RLSpace V is Abelian ::_thesis: ( LC_RLSpace V is add-associative & LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital ) proof let u, v be Element of (LC_RLSpace V); :: according to RLVECT_1:def_2 ::_thesis: u + v = v + u reconsider K = u, L = v as Linear_Combination of V by Def14; thus u + v = L + K by A1 .= v + u by A1 ; ::_thesis: verum end; thus LC_RLSpace V is add-associative ::_thesis: ( LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital ) proof let u, v, w be Element of (LC_RLSpace V); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w) reconsider L = u, K = v, M = w as Linear_Combination of V by Def14; A3: v + w = K + M by A1; u + v = L + K by A1; hence (u + v) + w = (L + K) + M by A1 .= L + (K + M) by Th40 .= u + (v + w) by A1, A3 ; ::_thesis: verum end; thus LC_RLSpace V is right_zeroed ::_thesis: ( LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital ) proof let v be Element of (LC_RLSpace V); :: according to RLVECT_1:def_4 ::_thesis: v + (0. (LC_RLSpace V)) = v reconsider K = v as Linear_Combination of V by Def14; thus v + (0. (LC_RLSpace V)) = K + (ZeroLC V) by A1 .= v by Th41 ; ::_thesis: verum end; thus LC_RLSpace V is right_complementable ::_thesis: ( LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital ) proof let v be Element of (LC_RLSpace V); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable reconsider K = v as Linear_Combination of V by Def14; - K in the carrier of (LC_RLSpace V) by Def14; then - K in LC_RLSpace V by STRUCT_0:def_5; then - K = vector ((LC_RLSpace V),(- K)) by Def1; then v + (vector ((LC_RLSpace V),(- K))) = K - K by A1 .= 0. (LC_RLSpace V) by Th57 ; hence ex w being VECTOR of (LC_RLSpace V) st v + w = 0. (LC_RLSpace V) ; :: according to ALGSTR_0:def_11 ::_thesis: verum end; A4: now__::_thesis:_for_v_being_VECTOR_of_(LC_RLSpace_V) for_L_being_Linear_Combination_of_V for_a_being_Real_st_v_=_L_holds_ a_*_v_=_a_*_L let v be VECTOR of (LC_RLSpace V); ::_thesis: for L being Linear_Combination of V for a being Real st v = L holds a * v = a * L let L be Linear_Combination of V; ::_thesis: for a being Real st v = L holds a * v = a * L let a be Real; ::_thesis: ( v = L implies a * v = a * L ) A5: @ (@ L) = L ; assume v = L ; ::_thesis: a * v = a * L hence a * v = a * L by A5, Def18; ::_thesis: verum end; thus for a being real number for v, w being VECTOR of (LC_RLSpace V) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital ) proof let a be real number ; ::_thesis: for v, w being VECTOR of (LC_RLSpace V) holds a * (v + w) = (a * v) + (a * w) let v, w be VECTOR of (LC_RLSpace V); ::_thesis: a * (v + w) = (a * v) + (a * w) reconsider K = v, M = w as Linear_Combination of V by Def14; reconsider a = a as Real by XREAL_0:def_1; A6: ( a * v = a * K & a * w = a * M ) by A4; v + w = K + M by A1; then a * (v + w) = a * (K + M) by A4 .= (a * K) + (a * M) by Th46 .= (a * v) + (a * w) by A1, A6 ; hence a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum end; thus for a, b being real number for v being VECTOR of (LC_RLSpace V) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital ) proof let a, b be real number ; ::_thesis: for v being VECTOR of (LC_RLSpace V) holds (a + b) * v = (a * v) + (b * v) let v be VECTOR of (LC_RLSpace V); ::_thesis: (a + b) * v = (a * v) + (b * v) reconsider K = v as Linear_Combination of V by Def14; reconsider a = a, b = b as Real by XREAL_0:def_1; A7: ( a * v = a * K & b * v = b * K ) by A4; (a + b) * v = (a + b) * K by A4 .= (a * K) + (b * K) by Th45 .= (a * v) + (b * v) by A1, A7 ; hence (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum end; thus for a, b being real number for v being VECTOR of (LC_RLSpace V) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: LC_RLSpace V is scalar-unital proof let a, b be real number ; ::_thesis: for v being VECTOR of (LC_RLSpace V) holds (a * b) * v = a * (b * v) let v be VECTOR of (LC_RLSpace V); ::_thesis: (a * b) * v = a * (b * v) reconsider K = v as Linear_Combination of V by Def14; reconsider a = a, b = b as Real by XREAL_0:def_1; A8: b * v = b * K by A4; (a * b) * v = (a * b) * K by A4 .= a * (b * K) by Th47 .= a * (b * v) by A4, A8 ; hence (a * b) * v = a * (b * v) ; ::_thesis: verum end; let v be VECTOR of (LC_RLSpace V); :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v reconsider K = v as Linear_Combination of V by Def14; thus 1 * v = 1 * K by A4 .= v by Th48 ; ::_thesis: verum end; end; theorem :: RLVECT_2:58 for V being RealLinearSpace holds the carrier of (LC_RLSpace V) = LinComb V ; theorem :: RLVECT_2:59 for V being RealLinearSpace holds 0. (LC_RLSpace V) = ZeroLC V ; theorem :: RLVECT_2:60 for V being RealLinearSpace holds the addF of (LC_RLSpace V) = LCAdd V ; theorem :: RLVECT_2:61 for V being RealLinearSpace holds the Mult of (LC_RLSpace V) = LCMult V ; theorem Th62: :: RLVECT_2:62 for V being RealLinearSpace for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = L1 + L2 proof let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = L1 + L2 let L1, L2 be Linear_Combination of V; ::_thesis: (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = L1 + L2 set v2 = vector ((LC_RLSpace V),L2); A1: ( L1 = @ (@ L1) & L2 = @ (@ L2) ) ; L2 in the carrier of (LC_RLSpace V) by Def14; then A2: L2 in LC_RLSpace V by STRUCT_0:def_5; L1 in the carrier of (LC_RLSpace V) by Def14; then L1 in LC_RLSpace V by STRUCT_0:def_5; hence (vector ((LC_RLSpace V),L1)) + (vector ((LC_RLSpace V),L2)) = (LCAdd V) . [L1,(vector ((LC_RLSpace V),L2))] by Def1 .= (LCAdd V) . ((@ L1),(@ L2)) by A2, Def1 .= L1 + L2 by A1, Def17 ; ::_thesis: verum end; theorem Th63: :: RLVECT_2:63 for V being RealLinearSpace for a being Real for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L proof let V be RealLinearSpace; ::_thesis: for a being Real for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L let a be Real; ::_thesis: for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L let L be Linear_Combination of V; ::_thesis: a * (vector ((LC_RLSpace V),L)) = a * L A1: @ (@ L) = L ; L in the carrier of (LC_RLSpace V) by Def14; then L in LC_RLSpace V by STRUCT_0:def_5; hence a * (vector ((LC_RLSpace V),L)) = (LCMult V) . [a,(@ L)] by Def1 .= a * L by A1, Def18 ; ::_thesis: verum end; theorem Th64: :: RLVECT_2:64 for V being RealLinearSpace for L being Linear_Combination of V holds - (vector ((LC_RLSpace V),L)) = - L proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds - (vector ((LC_RLSpace V),L)) = - L let L be Linear_Combination of V; ::_thesis: - (vector ((LC_RLSpace V),L)) = - L thus - (vector ((LC_RLSpace V),L)) = (- 1) * (vector ((LC_RLSpace V),L)) by RLVECT_1:16 .= - L by Th63 ; ::_thesis: verum end; theorem :: RLVECT_2:65 for V being RealLinearSpace for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2 proof let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2 let L1, L2 be Linear_Combination of V; ::_thesis: (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2 - L2 in LinComb V by Def14; then A1: - L2 in LC_RLSpace V by STRUCT_0:def_5; - (vector ((LC_RLSpace V),L2)) = - L2 by Th64 .= vector ((LC_RLSpace V),(- L2)) by A1, Def1 ; hence (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2 by Th62; ::_thesis: verum end; definition let V be RealLinearSpace; let A be Subset of V; func LC_RLSpace A -> strict Subspace of LC_RLSpace V means :: RLVECT_2:def 20 the carrier of it = { l where l is Linear_Combination of A : verum } ; existence ex b1 being strict Subspace of LC_RLSpace V st the carrier of b1 = { l where l is Linear_Combination of A : verum } proof set X = { l where l is Linear_Combination of A : verum } ; { l where l is Linear_Combination of A : verum } c= the carrier of (LC_RLSpace V) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { l where l is Linear_Combination of A : verum } or x in the carrier of (LC_RLSpace V) ) assume x in { l where l is Linear_Combination of A : verum } ; ::_thesis: x in the carrier of (LC_RLSpace V) then ex l being Linear_Combination of A st x = l ; hence x in the carrier of (LC_RLSpace V) by Def14; ::_thesis: verum end; then reconsider X = { l where l is Linear_Combination of A : verum } as Subset of (LC_RLSpace V) ; A1: X is linearly-closed proof thus for v, u being VECTOR of (LC_RLSpace V) st v in X & u in X holds v + u in X :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of REAL for b2 being Element of the carrier of (LC_RLSpace V) holds ( not b2 in X or b1 * b2 in X ) proof let v, u be VECTOR of (LC_RLSpace V); ::_thesis: ( v in X & u in X implies v + u in X ) assume that A2: v in X and A3: u in X ; ::_thesis: v + u in X consider l1 being Linear_Combination of A such that A4: v = l1 by A2; consider l2 being Linear_Combination of A such that A5: u = l2 by A3; A6: u = vector ((LC_RLSpace V),l2) by A5, Def1, RLVECT_1:1; v = vector ((LC_RLSpace V),l1) by A4, Def1, RLVECT_1:1; then v + u = l1 + l2 by A6, Th62; then v + u is Linear_Combination of A by Th38; hence v + u in X ; ::_thesis: verum end; let a be Real; ::_thesis: for b1 being Element of the carrier of (LC_RLSpace V) holds ( not b1 in X or a * b1 in X ) let v be VECTOR of (LC_RLSpace V); ::_thesis: ( not v in X or a * v in X ) assume v in X ; ::_thesis: a * v in X then consider l being Linear_Combination of A such that A7: v = l ; a * v = a * (vector ((LC_RLSpace V),l)) by A7, Def1, RLVECT_1:1 .= a * l by Th63 ; then a * v is Linear_Combination of A by Th44; hence a * v in X ; ::_thesis: verum end; ZeroLC V is Linear_Combination of A by Th22; then ZeroLC V in X ; hence ex b1 being strict Subspace of LC_RLSpace V st the carrier of b1 = { l where l is Linear_Combination of A : verum } by A1, RLSUB_1:35; ::_thesis: verum end; uniqueness for b1, b2 being strict Subspace of LC_RLSpace V st the carrier of b1 = { l where l is Linear_Combination of A : verum } & the carrier of b2 = { l where l is Linear_Combination of A : verum } holds b1 = b2 by RLSUB_1:30; end; :: deftheorem defines LC_RLSpace RLVECT_2:def_20_:_ for V being RealLinearSpace for A being Subset of V for b3 being strict Subspace of LC_RLSpace V holds ( b3 = LC_RLSpace A iff the carrier of b3 = { l where l is Linear_Combination of A : verum } ); theorem Th66: :: RLVECT_2:66 for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT for v being Element of V st k in dom F & v = G . k holds F . k = a * v ) holds Sum F = a * (Sum G) proof let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT for v being Element of V st k in dom F & v = G . k holds F . k = a * v ) holds Sum F = a * (Sum G) let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT for v being Element of V st k in dom F & v = G . k holds F . k = a * v ) holds Sum F = a * (Sum G) let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT for v being Element of V st k in dom F & v = G . k holds F . k = a * v ) holds Sum F = a * (Sum G) let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Element of NAT for v being Element of V st k in dom F & v = G . k holds F . k = a * v ) implies Sum F = a * (Sum G) ) defpred S1[ Element of NAT ] means for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Element of NAT for v being Element of V st k in dom H & v = I . k holds H . k = a * v ) holds Sum H = a * (Sum I); A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Element of NAT for v being Element of V st k in dom H & v = I . k holds H . k = a * v ) holds Sum H = a * (Sum I) ; ::_thesis: S1[n + 1] let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = n + 1 & ( for k being Element of NAT for v being Element of V st k in dom H & v = I . k holds H . k = a * v ) implies Sum H = a * (Sum I) ) assume that A3: len H = len I and A4: len H = n + 1 and A5: for k being Element of NAT for v being Element of V st k in dom H & v = I . k holds H . k = a * v ; ::_thesis: Sum H = a * (Sum I) reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of V by FINSEQ_1:18; A6: n <= n + 1 by NAT_1:12; then A7: q = I | (dom q) by A3, A4, FINSEQ_1:17; A8: len p = n by A4, A6, FINSEQ_1:17; A9: len q = n by A3, A4, A6, FINSEQ_1:17; A10: now__::_thesis:_for_k_being_Element_of_NAT_ for_v_being_Element_of_V_st_k_in_dom_p_&_v_=_q_._k_holds_ p_._k_=_a_*_v A11: dom p c= dom H by A4, A6, A8, FINSEQ_3:30; let k be Element of NAT ; ::_thesis: for v being Element of V st k in dom p & v = q . k holds p . k = a * v let v be Element of V; ::_thesis: ( k in dom p & v = q . k implies p . k = a * v ) assume that A12: k in dom p and A13: v = q . k ; ::_thesis: p . k = a * v dom q = dom p by A8, A9, FINSEQ_3:29; then I . k = q . k by A12, FUNCT_1:47; then H . k = a * v by A5, A12, A13, A11; hence p . k = a * v by A12, FUNCT_1:47; ::_thesis: verum end; n + 1 in Seg (n + 1) by FINSEQ_1:4; then A14: n + 1 in dom H by A4, FINSEQ_1:def_3; dom H = dom I by A3, FINSEQ_3:29; then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Element of V by A14, FINSEQ_2:11; A15: v1 = a * v2 by A5, A14; p = H | (dom p) by A4, A6, FINSEQ_1:17; hence Sum H = (Sum p) + v1 by A4, A8, RLVECT_1:38 .= (a * (Sum q)) + (a * v2) by A2, A8, A9, A10, A15 .= a * ((Sum q) + v2) by VECTSP_1:def_14 .= a * (Sum I) by A3, A4, A9, A7, RLVECT_1:38 ; ::_thesis: verum end; A16: S1[ 0 ] proof let H, I be FinSequence of V; ::_thesis: ( len H = len I & len H = 0 & ( for k being Element of NAT for v being Element of V st k in dom H & v = I . k holds H . k = a * v ) implies Sum H = a * (Sum I) ) assume that A17: len H = len I and A18: len H = 0 and for k being Element of NAT for v being Element of V st k in dom H & v = I . k holds H . k = a * v ; ::_thesis: Sum H = a * (Sum I) H = <*> the carrier of V by A18; then A19: Sum H = 0. V by RLVECT_1:43; I = <*> the carrier of V by A17, A18; then Sum I = 0. V by RLVECT_1:43; hence Sum H = a * (Sum I) by A19, VECTSP_1:14; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A1); hence ( len F = len G & ( for k being Element of NAT for v being Element of V st k in dom F & v = G . k holds F . k = a * v ) implies Sum F = a * (Sum G) ) ; ::_thesis: verum end; theorem :: RLVECT_2:67 for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) holds Sum G = a * (Sum F) proof let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) holds Sum G = a * (Sum F) let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) holds Sum G = a * (Sum F) let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: for F, G being FinSequence of V st len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) holds Sum G = a * (Sum F) let F, G be FinSequence of V; ::_thesis: ( len F = len G & ( for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ) implies Sum G = a * (Sum F) ) assume that A1: len F = len G and A2: for k being Element of NAT st k in dom F holds G . k = a * (F /. k) ; ::_thesis: Sum G = a * (Sum F) now__::_thesis:_for_k_being_Element_of_NAT_ for_v_being_Element_of_V_st_k_in_dom_G_&_v_=_F_._k_holds_ G_._k_=_a_*_v let k be Element of NAT ; ::_thesis: for v being Element of V st k in dom G & v = F . k holds G . k = a * v let v be Element of V; ::_thesis: ( k in dom G & v = F . k implies G . k = a * v ) assume that A3: k in dom G and A4: v = F . k ; ::_thesis: G . k = a * v A5: k in dom F by A1, A3, FINSEQ_3:29; then v = F /. k by A4, PARTFUN1:def_6; hence G . k = a * v by A2, A5; ::_thesis: verum end; hence Sum G = a * (Sum F) by A1, Th66; ::_thesis: verum end; theorem :: RLVECT_2:68 for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr for V being non empty right_complementable Abelian add-associative right_zeroed VectSpStr over R for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ) holds Sum H = (Sum F) - (Sum G) proof let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed VectSpStr over R for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ) holds Sum H = (Sum F) - (Sum G) let V be non empty right_complementable Abelian add-associative right_zeroed VectSpStr over R; ::_thesis: for F, G, H being FinSequence of V st len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ) holds Sum H = (Sum F) - (Sum G) let F, G, H be FinSequence of V; ::_thesis: ( len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ) implies Sum H = (Sum F) - (Sum G) ) assume that A1: len F = len G and A2: len F = len H and A3: for k being Element of NAT st k in dom F holds H . k = (F /. k) - (G /. k) ; ::_thesis: Sum H = (Sum F) - (Sum G) deffunc H1( Nat) -> Element of the carrier of V = - (G /. $1); consider I being FinSequence such that A4: len I = len G and A5: for k being Nat st k in dom I holds I . k = H1(k) from FINSEQ_1:sch_2(); A6: dom I = Seg (len G) by A4, FINSEQ_1:def_3; then A7: for k being Element of NAT st k in Seg (len G) holds I . k = H1(k) by A5; rng I c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng I or x in the carrier of V ) assume x in rng I ; ::_thesis: x in the carrier of V then consider y being set such that A8: y in dom I and A9: I . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A8; x = - (G /. y) by A5, A8, A9; then reconsider v = x as Element of V ; v in V by RLVECT_1:1; hence x in the carrier of V ; ::_thesis: verum end; then reconsider I = I as FinSequence of V by FINSEQ_1:def_4; A10: Seg (len G) = dom G by FINSEQ_1:def_3; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_ H_._k_=_(F_/._k)_+_(I_/._k) let k be Element of NAT ; ::_thesis: ( k in dom F implies H . k = (F /. k) + (I /. k) ) A11: dom F = dom G by A1, FINSEQ_3:29; assume A12: k in dom F ; ::_thesis: H . k = (F /. k) + (I /. k) then k in dom I by A1, A4, FINSEQ_3:29; then A13: I . k = I /. k by PARTFUN1:def_6; thus H . k = (F /. k) - (G /. k) by A3, A12 .= (F /. k) + (- (G /. k)) .= (F /. k) + (I /. k) by A5, A6, A10, A12, A13, A11 ; ::_thesis: verum end; then A14: Sum H = (Sum F) + (Sum I) by A1, A2, A4, Th2; Sum I = - (Sum G) by A4, A7, A10, Th4; hence Sum H = (Sum F) - (Sum G) by A14; ::_thesis: verum end; theorem :: RLVECT_2:69 for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R holds a * (Sum (<*> the carrier of V)) = 0. V proof let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R holds a * (Sum (<*> the carrier of V)) = 0. V let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R holds a * (Sum (<*> the carrier of V)) = 0. V let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: a * (Sum (<*> the carrier of V)) = 0. V thus a * (Sum (<*> the carrier of V)) = a * (0. V) by RLVECT_1:43 .= 0. V by VECTSP_1:14 ; ::_thesis: verum end; theorem :: RLVECT_2:70 for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u) proof let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u) let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u) let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: for v, u being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u) let v, u be Element of V; ::_thesis: a * (Sum <*v,u*>) = (a * v) + (a * u) thus a * (Sum <*v,u*>) = a * (v + u) by RLVECT_1:45 .= (a * v) + (a * u) by VECTSP_1:def_14 ; ::_thesis: verum end; theorem :: RLVECT_2:71 for R being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w) proof let R be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of R for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w) let a be Element of R; ::_thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w) let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R; ::_thesis: for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w) let v, u, w be Element of V; ::_thesis: a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w) thus a * (Sum <*v,u,w*>) = a * ((v + u) + w) by RLVECT_1:46 .= (a * (v + u)) + (a * w) by VECTSP_1:def_14 .= ((a * v) + (a * u)) + (a * w) by VECTSP_1:def_14 ; ::_thesis: verum end;