:: VECTSP_6 semantic presentation begin definition let GF be non empty ZeroStr ; let V be non empty VectSpStr over GF; mode Linear_Combination of V -> Element of Funcs ( the carrier of V, the carrier of GF) means :Def1: :: VECTSP_6:def 1 ex T being finite Subset of V st for v being Element of V st not v in T holds it . v = 0. GF; existence ex b1 being Element of Funcs ( the carrier of V, the carrier of GF) ex T being finite Subset of V st for v being Element of V st not v in T holds b1 . v = 0. GF proof reconsider f = the carrier of V --> (0. GF) as Function of the carrier of V, the carrier of GF ; reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) 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. GF take {} V ; ::_thesis: for v being Element of V st not v in {} V holds f . v = 0. GF thus for v being Element of V st not v in {} V holds f . v = 0. GF by FUNCOP_1:7; ::_thesis: verum end; end; :: deftheorem Def1 defines Linear_Combination VECTSP_6:def_1_:_ for GF being non empty ZeroStr for V being non empty VectSpStr over GF for b3 being Element of Funcs ( the carrier of V, the carrier of GF) holds ( b3 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 b3 . v = 0. GF ); definition let GF be non empty ZeroStr ; let V be non empty VectSpStr over GF; let L be Linear_Combination of V; func Carrier L -> finite Subset of V equals :: VECTSP_6:def 2 { v where v is Element of V : L . v <> 0. GF } ; coherence { v where v is Element of V : L . v <> 0. GF } is finite Subset of V proof set A = { v where v is Element of V : L . v <> 0. GF } ; 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. GF by Def1; { v where v is Element of V : L . v <> 0. GF } c= T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of V : L . v <> 0. GF } or x in T ) assume x in { v where v is Element of V : L . v <> 0. GF } ; ::_thesis: x in T then ex v being Element of V st ( x = v & L . v <> 0. GF ) ; hence x in T by A1; ::_thesis: verum end; hence { v where v is Element of V : L . v <> 0. GF } is finite Subset of V by XBOOLE_1:1; ::_thesis: verum end; end; :: deftheorem defines Carrier VECTSP_6:def_2_:_ for GF being non empty ZeroStr for V being non empty VectSpStr over GF for L being Linear_Combination of V holds Carrier L = { v where v is Element of V : L . v <> 0. GF } ; theorem :: VECTSP_6:1 for x being set for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds ( x in Carrier L iff ex v being Element of V st ( x = v & L . v <> 0. GF ) ) ; theorem :: VECTSP_6:2 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L being Linear_Combination of V holds ( L . v = 0. GF iff not v in Carrier L ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L being Linear_Combination of V holds ( L . v = 0. GF iff not v in Carrier L ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for L being Linear_Combination of V holds ( L . v = 0. GF iff not v in Carrier L ) let v be Element of V; ::_thesis: for L being Linear_Combination of V holds ( L . v = 0. GF iff not v in Carrier L ) let L be Linear_Combination of V; ::_thesis: ( L . v = 0. GF iff not v in Carrier L ) thus ( L . v = 0. GF implies not v in Carrier L ) ::_thesis: ( not v in Carrier L implies L . v = 0. GF ) proof assume A1: L . v = 0. GF ; ::_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. GF ) ; hence contradiction by A1; ::_thesis: verum end; assume not v in Carrier L ; ::_thesis: L . v = 0. GF hence L . v = 0. GF ; ::_thesis: verum end; definition let GF be non empty ZeroStr ; let V be non empty VectSpStr over GF; func ZeroLC V -> Linear_Combination of V means :Def3: :: VECTSP_6:def 3 Carrier it = {} ; existence ex b1 being Linear_Combination of V st Carrier b1 = {} proof reconsider f = the carrier of V --> (0. GF) as Function of the carrier of V, the carrier of GF ; reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8; f is Linear_Combination of V proof reconsider T = {} V as empty finite Subset of V ; take T ; :: according to VECTSP_6:def_1 ::_thesis: for v being Element of V st not v in T holds f . v = 0. GF thus for v being Element of V st not v in T holds f . v = 0. GF 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. GF } ; now__::_thesis:_not__{__v_where_v_is_Element_of_V_:_f_._v_<>_0._GF__}__<>_{} set x = the Element of { v where v is Element of V : f . v <> 0. GF } ; assume { v where v is Element of V : f . v <> 0. GF } <> {} ; ::_thesis: contradiction then the Element of { v where v is Element of V : f . v <> 0. GF } in { v where v is Element of V : f . v <> 0. GF } ; then ex v being Element of V st ( the Element of { v where v is Element of V : f . v <> 0. GF } = v & f . v <> 0. GF ) ; 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 ) reconsider K = L, K9 = L9 as Function of the carrier of V, the carrier of GF ; 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_ K_._x_=_K9_._x let x be set ; ::_thesis: ( x in the carrier of V implies K . x = K9 . x ) assume x in the carrier of V ; ::_thesis: K . x = K9 . x then reconsider v = x as Element of V ; A3: now__::_thesis:_not_L9_._v_<>_0._GF assume L9 . v <> 0. GF ; ::_thesis: contradiction then v in { u where u is Element of V : L9 . u <> 0. GF } ; hence contradiction by A2; ::_thesis: verum end; now__::_thesis:_not_L_._v_<>_0._GF assume L . v <> 0. GF ; ::_thesis: contradiction then v in { u where u is Element of V : L . u <> 0. GF } ; hence contradiction by A1; ::_thesis: verum end; hence K . x = K9 . x by A3; ::_thesis: verum end; hence L = L9 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def3 defines ZeroLC VECTSP_6:def_3_:_ for GF being non empty ZeroStr for V being non empty VectSpStr over GF for b3 being Linear_Combination of V holds ( b3 = ZeroLC V iff Carrier b3 = {} ); theorem Th3: :: VECTSP_6:3 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V holds (ZeroLC V) . v = 0. GF proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V holds (ZeroLC V) . v = 0. GF let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V holds (ZeroLC V) . v = 0. GF let v be Element of V; ::_thesis: (ZeroLC V) . v = 0. GF ( Carrier (ZeroLC V) = {} & not v in {} ) by Def3; hence (ZeroLC V) . v = 0. GF ; ::_thesis: verum end; definition let GF be non empty ZeroStr ; let V be non empty VectSpStr over GF; let A be Subset of V; mode Linear_Combination of A -> Linear_Combination of V means :Def4: :: VECTSP_6:def 4 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 Def3; hence Carrier L c= A by XBOOLE_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines Linear_Combination VECTSP_6:def_4_:_ for GF being non empty ZeroStr for V being non empty VectSpStr over GF for A being Subset of V for b4 being Linear_Combination of V holds ( b4 is Linear_Combination of A iff Carrier b4 c= A ); theorem :: VECTSP_6:4 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF 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 GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF 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 V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Def4; then Carrier l c= B by A1, XBOOLE_1:1; hence l is Linear_Combination of B by Def4; ::_thesis: verum end; theorem Th5: :: VECTSP_6:5 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for A being Subset of V holds ZeroLC V is Linear_Combination of A proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for A being Subset of V holds ZeroLC V is Linear_Combination of A let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Def3, XBOOLE_1:2; hence ZeroLC V is Linear_Combination of A by Def4; ::_thesis: verum end; theorem Th6: :: VECTSP_6:6 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Def4; then Carrier l = {} ; hence l = ZeroLC V by Def3; ::_thesis: verum end; theorem :: VECTSP_6:7 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def4; definition let GF be non empty addLoopStr ; let V be non empty VectSpStr over GF; let F be FinSequence of the carrier of V; let f be Function of V,GF; funcf (#) F -> FinSequence of V means :Def5: :: VECTSP_6:def 5 ( len it = len F & ( for i being Nat st i in dom it holds it . i = (f . (F /. i)) * (F /. i) ) ); existence ex b1 being FinSequence of V st ( len b1 = len F & ( for i being Nat st i in dom b1 holds b1 . i = (f . (F /. i)) * (F /. i) ) ) proof deffunc H1( Nat) -> 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 Nat st i in dom G holds G . i = (f . (F /. i)) * (F /. i) ) ) thus ( len G = len F & ( for i being 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 V st len b1 = len F & ( for i being Nat st i in dom b1 holds b1 . i = (f . (F /. i)) * (F /. i) ) & len b2 = len F & ( for i being Nat st i in dom b2 holds b2 . i = (f . (F /. i)) * (F /. i) ) holds b1 = b2 proof let H1, H2 be FinSequence of the carrier of V; ::_thesis: ( len H1 = len F & ( for i being Nat st i in dom H1 holds H1 . i = (f . (F /. i)) * (F /. i) ) & len H2 = len F & ( for i being 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 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 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 Def5 defines (#) VECTSP_6:def_5_:_ for GF being non empty addLoopStr for V being non empty VectSpStr over GF for F being FinSequence of the carrier of V for f being Function of V,GF for b5 being FinSequence of V holds ( b5 = f (#) F iff ( len b5 = len F & ( for i being Nat st i in dom b5 holds b5 . i = (f . (F /. i)) * (F /. i) ) ) ); theorem Th8: :: VECTSP_6:8 for i being Element of NAT for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for F being FinSequence of V for f being Function of V,GF st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v proof let i be Element of NAT ; ::_thesis: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for F being FinSequence of V for f being Function of V,GF st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for F being FinSequence of V for f being Function of V,GF st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for F being FinSequence of V for f being Function of V,GF st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v let v be Element of V; ::_thesis: for F being FinSequence of V for f being Function of V,GF 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 V,GF st i in dom F & v = F . i holds (f (#) F) . i = (f . v) * v let f be Function of V,GF; ::_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 Def5; then i in dom (f (#) F) by A1, FINSEQ_3:29; hence (f (#) F) . i = (f . v) * v by A2, A3, Def5; ::_thesis: verum end; theorem :: VECTSP_6:9 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V let f be Function of V,GF; ::_thesis: f (#) (<*> the carrier of V) = <*> the carrier of V len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def5 .= 0 ; hence f (#) (<*> the carrier of V) = <*> the carrier of V ; ::_thesis: verum end; theorem Th10: :: VECTSP_6:10 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*> proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*> let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*> let v be Element of V; ::_thesis: for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*> let f be Function of V,GF; ::_thesis: f (#) <*v*> = <*((f . v) * v)*> A1: 1 in {1} by TARSKI:def_1; A2: len (f (#) <*v*>) = len <*v*> by Def5 .= 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, Def5 .= (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 Th11: :: VECTSP_6:11 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v1, v2 being Element of V for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v1, v2 being Element of V for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v1, v2 being Element of V for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> let v1, v2 be Element of V; ::_thesis: for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> let f be Function of V,GF; ::_thesis: f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> A1: len (f (#) <*v1,v2*>) = len <*v1,v2*> by Def5 .= 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, Def5 .= (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, Def5 .= (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 :: VECTSP_6:12 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v1, v2, v3 being Element of V for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v1, v2, v3 being Element of V for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v1, v2, v3 being Element of V for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> let v1, v2, v3 be Element of V; ::_thesis: for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> let f be Function of V,GF; ::_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 Def5 .= 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, Def5 .= (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, Def5 .= (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, Def5 .= (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; theorem Th13: :: VECTSP_6:13 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for F, G being FinSequence of V for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for F, G being FinSequence of V for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for F, G being FinSequence of V for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) let F, G be FinSequence of V; ::_thesis: for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) let f be Function of V,GF; ::_thesis: f (#) (F ^ G) = (f (#) F) ^ (f (#) G) set H = (f (#) F) ^ (f (#) G); set I = F ^ G; A1: len F = len (f (#) F) by Def5; A2: len ((f (#) F) ^ (f (#) G)) = (len (f (#) F)) + (len (f (#) G)) by FINSEQ_1:22 .= (len F) + (len (f (#) G)) by Def5 .= (len F) + (len G) by Def5 .= len (F ^ G) by FINSEQ_1:22 ; A3: len G = len (f (#) G) by Def5; now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f_(#)_F)_^_(f_(#)_G))_holds_ ((f_(#)_F)_^_(f_(#)_G))_._k_=_(f_._((F_^_G)_/._k))_*_((F_^_G)_/._k) let k be Nat; ::_thesis: ( k in dom ((f (#) F) ^ (f (#) G)) implies ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) ) assume A4: k in dom ((f (#) F) ^ (f (#) G)) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) now__::_thesis:_((f_(#)_F)_^_(f_(#)_G))_._k_=_(f_._((F_^_G)_/._k))_*_((F_^_G)_/._k) percases ( k in dom (f (#) F) or ex n being Nat st ( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ) by A4, FINSEQ_1:25; supposeA5: k in dom (f (#) F) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) then A6: k in dom F by A1, FINSEQ_3:29; then A7: k in dom (F ^ G) by FINSEQ_3:22; A8: F /. k = F . k by A6, PARTFUN1:def_6 .= (F ^ G) . k by A6, FINSEQ_1:def_7 .= (F ^ G) /. k by A7, PARTFUN1:def_6 ; thus ((f (#) F) ^ (f (#) G)) . k = (f (#) F) . k by A5, FINSEQ_1:def_7 .= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A5, A8, Def5 ; ::_thesis: verum end; supposeA9: ex n being Nat st ( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) A10: k in dom (F ^ G) by A2, A4, FINSEQ_3:29; consider n being Nat such that A11: n in dom (f (#) G) and A12: k = (len (f (#) F)) + n by A9; A13: n in dom G by A3, A11, FINSEQ_3:29; then A14: G /. n = G . n by PARTFUN1:def_6 .= (F ^ G) . k by A1, A12, A13, FINSEQ_1:def_7 .= (F ^ G) /. k by A10, PARTFUN1:def_6 ; thus ((f (#) F) ^ (f (#) G)) . k = (f (#) G) . n by A11, A12, FINSEQ_1:def_7 .= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A11, A14, Def5 ; ::_thesis: verum end; end; end; hence ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) ; ::_thesis: verum end; hence f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by A2, Def5; ::_thesis: verum end; definition let GF be non empty addLoopStr ; let V be non empty VectSpStr over GF; let L be Linear_Combination of V; assume A1: ( V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable ) ; func Sum L -> Element of V means :Def6: :: VECTSP_6:def 6 ex F being FinSequence of the carrier 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 the carrier of V st ( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) proof consider F being FinSequence such that A2: rng F = Carrier L and A3: F is one-to-one by FINSEQ_4:58; reconsider F = F as FinSequence of the carrier of V by A2, FINSEQ_1:def_4; take Sum (L (#) F) ; ::_thesis: ex F being FinSequence of the carrier 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 A2, A3; ::_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 the carrier of V st ( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) & ex F being FinSequence of the carrier 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 the carrier of V st ( F is one-to-one & rng F = Carrier L & v1 = Sum (L (#) F) ) & ex F being FinSequence of the carrier 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 A4: F1 is one-to-one and A5: rng F1 = Carrier L and A6: v1 = Sum (L (#) F1) ; ::_thesis: ( for F being FinSequence of the carrier 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 A7: F2 is one-to-one and A8: rng F2 = Carrier L and A9: v2 = Sum (L (#) F2) ; ::_thesis: v1 = v2 defpred S1[ set , set ] means {$2} = F1 " {(F2 . $1)}; A10: len F1 = len F2 by A4, A5, A7, A8, FINSEQ_1:48; A11: dom F1 = Seg (len F1) by FINSEQ_1:def_3; A12: dom F2 = Seg (len F2) by FINSEQ_1:def_3; A13: 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 A5, A8, A10, A11, A12, FUNCT_1:def_3; then consider y being set such that A14: F1 " {(F2 . x)} = {y} by A4, FUNCT_1:74; take y ; ::_thesis: ( y in dom F1 & S1[x,y] ) y in F1 " {(F2 . x)} by A14, TARSKI:def_1; hence y in dom F1 by FUNCT_1:def_7; ::_thesis: S1[x,y] thus S1[x,y] by A14; ::_thesis: verum end; consider f being Function of (dom F1),(dom F1) such that A15: for x being set st x in dom F1 holds S1[x,f . x] from FUNCT_2:sch_1(A13); A16: rng f = dom F1 proof thus rng f c= dom F1 by RELAT_1:def_19; :: 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 A17: y in dom F1 ; ::_thesis: y in rng f then F1 . y in rng F2 by A5, A8, FUNCT_1:def_3; then consider x being set such that A18: x in dom F2 and A19: F2 . x = F1 . y by FUNCT_1:def_3; F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A17, A19, FUNCT_1:59; then F1 " {(F2 . x)} c= {y} by A4, FUNCT_1:82; then {(f . x)} c= {y} by A10, A11, A12, A15, A18; then A20: f . x = y by ZFMISC_1:18; x in dom f by A10, A11, A12, A18, FUNCT_2:def_1; hence y in rng f by A20, FUNCT_1:def_3; ::_thesis: verum end; set G1 = L (#) F1; A21: len (L (#) F1) = len F1 by Def5; A22: ( dom F1 = {} implies dom F1 = {} ) ; A23: 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 A24: y1 in dom f and A25: y2 in dom f and A26: f . y1 = f . y2 ; ::_thesis: y1 = y2 A27: y2 in dom F1 by A22, A25, FUNCT_2:def_1; then A28: F1 " {(F2 . y2)} = {(f . y2)} by A15; A29: y1 in dom F1 by A22, A24, FUNCT_2:def_1; then F2 . y1 in rng F1 by A5, A8, A10, A11, A12, FUNCT_1:def_3; then A30: {(F2 . y1)} c= rng F1 by ZFMISC_1:31; F2 . y2 in rng F1 by A5, A8, A10, A11, A12, A27, FUNCT_1:def_3; then A31: {(F2 . y2)} c= rng F1 by ZFMISC_1:31; F1 " {(F2 . y1)} = {(f . y1)} by A15, A29; then {(F2 . y1)} = {(F2 . y2)} by A26, A28, A30, A31, FUNCT_1:91; then A32: F2 . y1 = F2 . y2 by ZFMISC_1:3; ( y1 in dom F2 & y2 in dom F2 ) by A10, A11, A12, A22, A24, A25, FUNCT_2:def_1; hence y1 = y2 by A7, A32, FUNCT_1:def_4; ::_thesis: verum end; set G2 = L (#) F2; A33: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def_3; reconsider f = f as Permutation of (dom F1) by A16, A23, 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; A34: len (L (#) F2) = len F2 by Def5; A35: 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 A36: i in dom (L (#) F2) ; ::_thesis: (L (#) F2) . i = (L (#) F1) . (f . i) then A37: ( (L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) & F2 . i = F2 /. i ) by A34, A12, A33, Def5, PARTFUN1:def_6; i in dom F2 by A34, A36, FINSEQ_3:29; then reconsider u = F2 . i as Element of V by FINSEQ_2:11; i in dom f by A10, A21, A34, A35, A33, A36, FUNCT_2:def_1; then A38: f . i in dom F1 by A16, FUNCT_1:def_3; then reconsider m = f . i as Element of NAT by A11; reconsider v = F1 . m as Element of V by A38, FINSEQ_2:11; {(F1 . (f . i))} = Im (F1,(f . i)) by A38, FUNCT_1:59 .= F1 .: (F1 " {(F2 . i)}) by A10, A34, A11, A33, A15, A36 ; then A39: u = v by FUNCT_1:75, ZFMISC_1:18; F1 . m = F1 /. m by A38, PARTFUN1:def_6; hence (L (#) F2) . i = (L (#) F1) . (f . i) by A21, A11, A35, A38, A39, A37, Def5; ::_thesis: verum end; hence v1 = v2 by A1, A4, A5, A6, A7, A8, A9, A21, A34, FINSEQ_1:48, RLVECT_2:6; ::_thesis: verum end; end; :: deftheorem Def6 defines Sum VECTSP_6:def_6_:_ for GF being non empty addLoopStr for V being non empty VectSpStr over GF for L being Linear_Combination of V st V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable holds for b4 being Element of V holds ( b4 = Sum L iff ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & b4 = Sum (L (#) F) ) ); Lm1: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Def6; Carrier (ZeroLC V) = {} by Def3; then F = {} by A1, RELAT_1:41; then len F = 0 ; then len ((ZeroLC V) (#) F) = 0 by Def5; hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; ::_thesis: verum end; theorem :: VECTSP_6:14 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for A being Subset of V st 0. GF <> 1. GF holds ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for A being Subset of V st 0. GF <> 1. GF holds ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for A being Subset of V st 0. GF <> 1. GF 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: ( 0. GF <> 1. GF implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) ) assume A1: 0. GF <> 1. GF ; ::_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 A2: A <> {} and A3: A is linearly-closed ; ::_thesis: for l being Linear_Combination of A holds Sum l in A A4: S1[ 0 ] proof 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 Def3; then Sum l = 0. V by Lm1; hence Sum l in A by A2, A3, VECTSP_4:1; ::_thesis: verum end; A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] 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 the carrier of GF = l . $1; consider F being FinSequence of V such that A7: F is one-to-one and A8: rng F = Carrier l and A9: Sum l = Sum (l (#) F) by Def6; reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18; assume A10: card (Carrier l) = k + 1 ; ::_thesis: Sum l in A then A11: len F = k + 1 by A7, A8, FINSEQ_4:62; then A12: len (l (#) F) = k + 1 by Def5; A13: k + 1 in Seg (k + 1) by FINSEQ_1:4; then A14: k + 1 in dom F by A11, FINSEQ_1:def_3; k + 1 in dom F by A11, A13, FINSEQ_1:def_3; then reconsider v = F . (k + 1) as Element of V by FINSEQ_2:11; consider f being Function of the carrier of V, the carrier of GF such that A15: f . v = 0. GF and A16: 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, the carrier of GF) by FUNCT_2:8; A17: v in Carrier l by A8, A14, FUNCT_1:def_3; now__::_thesis:_for_u_being_Element_of_V_st_not_u_in_Carrier_l_holds_ f_._u_=_0._GF let u be Element of V; ::_thesis: ( not u in Carrier l implies f . u = 0. GF ) assume A18: not u in Carrier l ; ::_thesis: f . u = 0. GF hence f . u = l . u by A17, A16 .= 0. GF by A18 ; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def1; A19: A \ {v} c= A by XBOOLE_1:36; A20: Carrier l c= A by Def4; then A21: (l . v) * v in A by A3, A17, VECTSP_4:def_1; A22: 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 Element of V such that A23: u = x and A24: f . u <> 0. GF ; f . u = l . u by A15, A16, A24; then A25: x in Carrier l by A23, A24; not x in {v} by A15, A23, A24, TARSKI:def_1; hence x in (Carrier l) \ {v} by A25, 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 A26: x in (Carrier l) \ {v} ; ::_thesis: x in Carrier f then x in Carrier l by XBOOLE_0:def_5; then consider u being Element of V such that A27: x = u and A28: l . u <> 0. GF ; not x in {v} by A26, XBOOLE_0:def_5; then x <> v by TARSKI:def_1; then l . u = f . u by A16, A27; hence x in Carrier f by A27, A28; ::_thesis: verum end; then Carrier f c= A \ {v} by A20, XBOOLE_1:33; then Carrier f c= A by A19, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by Def4; A29: len G = k by A11, FINSEQ_3:53; then A30: len (f (#) G) = k by Def5; A31: 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 A32: y in dom G and A33: G . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A32, FINSEQ_3:23; A34: ( dom G c= dom F & G . y = F . y ) by A32, FUNCT_1:47, RELAT_1:60; now__::_thesis:_not_x_=_v assume x = v ; ::_thesis: contradiction then A35: k + 1 = y by A7, A14, A32, A33, A34, FUNCT_1:def_4; y <= k by A29, A32, FINSEQ_3:25; hence contradiction by A35, XREAL_1:29; ::_thesis: verum end; then A36: not x in {v} by TARSKI:def_1; x in rng F by A32, A33, A34, FUNCT_1:def_3; hence x in Carrier f by A8, A22, A36, 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 A37: x in Carrier f ; ::_thesis: x in rng G then x in rng F by A8, A22, XBOOLE_0:def_5; then consider y being set such that A38: y in dom F and A39: F . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A38, FINSEQ_3:23; now__::_thesis:_y_in_Seg_k assume not y in Seg k ; ::_thesis: contradiction then y in (dom F) \ (Seg k) by A38, XBOOLE_0:def_5; then y in (Seg (k + 1)) \ (Seg k) by A11, 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 A22, A37, A39, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then y in (dom F) /\ (Seg k) by A38, XBOOLE_0:def_4; then A40: y in dom G by RELAT_1:61; then G . y = F . y by FUNCT_1:47; hence x in rng G by A39, A40, 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 A30, FINSEQ_1:def_3 ; then A41: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A12, 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 ) A42: rng F c= the carrier of V by FINSEQ_1:def_4; assume A43: x in dom (f (#) G) ; ::_thesis: (f (#) G) . x = (l (#) F) . x then reconsider n = x as Element of NAT by FINSEQ_3:23; n in dom (l (#) F) by A41, A43, XBOOLE_0:def_4; then A44: n in dom F by A11, A12, FINSEQ_3:29; then F . n in rng F by FUNCT_1:def_3; then reconsider w = F . n as Element of V by A42; A45: n in dom G by A29, A30, A43, FINSEQ_3:29; then A46: G . n in rng G by FUNCT_1:def_3; rng G c= the carrier of V by FINSEQ_1:def_4; then reconsider u = G . n as Element of V by A46; not u in {v} by A22, A31, A46, XBOOLE_0:def_5; then A47: u <> v by TARSKI:def_1; A48: (f (#) G) . n = (f . u) * u by A45, Th8 .= (l . u) * u by A16, A47 ; w = u by A45, FUNCT_1:47; hence (f (#) G) . x = (l (#) F) . x by A48, A44, Th8; ::_thesis: verum end; then f (#) G = (l (#) F) | (Seg k) by A41, FUNCT_1:46; then A49: f (#) G = (l (#) F) | (dom (f (#) G)) by A30, FINSEQ_1:def_3; v in rng F by A14, FUNCT_1:def_3; then {v} c= Carrier l by A8, ZFMISC_1:31; then card (Carrier f) = (k + 1) - (card {v}) by A10, A22, CARD_2:44 .= (k + 1) - 1 by CARD_1:30 .= k by XCMPLX_1:26 ; then A50: Sum f in A by A6; G is one-to-one by A7, FUNCT_1:52; then A51: Sum (f (#) G) = Sum f by A31, Def6; (l (#) F) . (len F) = (l . v) * v by A11, A14, Th8; then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by A11, A12, A30, A49, RLVECT_1:38; hence Sum l in A by A3, A9, A21, A51, A50, VECTSP_4:def_1; ::_thesis: verum end; let l be Linear_Combination of A; ::_thesis: Sum l in A A52: card (Carrier l) = card (Carrier l) ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A5); hence Sum l in A by A52; ::_thesis: verum end; assume A53: 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 Lm1, Th5; then A54: 0. V in A by A53; A55: for a being Element of GF for v being Element of V st v in A holds a * v in A proof let a be Element of GF; ::_thesis: for v being Element of V st v in A holds a * v in A let v be Element of V; ::_thesis: ( v in A implies a * v in A ) assume A56: v in A ; ::_thesis: a * v in A now__::_thesis:_a_*_v_in_A percases ( a = 0. GF or a <> 0. GF ) ; suppose a = 0. GF ; ::_thesis: a * v in A hence a * v in A by A54, VECTSP_1:14; ::_thesis: verum end; supposeA57: a <> 0. GF ; ::_thesis: a * v in A deffunc H1( set ) -> Element of the carrier of GF = 0. GF; consider f being Function of V,GF such that A58: f . v = a and A59: 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, the carrier of GF) by FUNCT_2:8; now__::_thesis:_for_u_being_Element_of_V_st_not_u_in_{v}_holds_ f_._u_=_0._GF let u be Element of V; ::_thesis: ( not u in {v} implies f . u = 0. GF ) assume not u in {v} ; ::_thesis: f . u = 0. GF then u <> v by TARSKI:def_1; hence f . u = 0. GF by A59; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def1; A60: 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 Element of V such that A61: x = u and A62: f . u <> 0. GF ; u = v by A59, A62; hence x in {v} by A61, 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 A57, A58; ::_thesis: verum end; {v} c= A by A56, ZFMISC_1:31; then reconsider f = f as Linear_Combination of A by A60, Def4; consider F being FinSequence of V such that A63: ( F is one-to-one & rng F = Carrier f ) and A64: Sum (f (#) F) = Sum f by Def6; F = <*v*> by A60, A63, FINSEQ_3:97; then f (#) F = <*((f . v) * v)*> by Th10; then Sum f = a * v by A58, A64, RLVECT_1:44; hence a * v in A by A53; ::_thesis: verum end; end; end; hence a * v in A ; ::_thesis: verum end; thus for v, u being Element of V st v in A & u in A holds v + u in A :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of GF for b2 being Element of the carrier of V holds ( not b2 in A or b1 * b2 in A ) proof let v, u be Element of V; ::_thesis: ( v in A & u in A implies v + u in A ) assume that A65: v in A and A66: 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. GF) * v) + v by VECTSP_1:def_17 .= ((1. GF) * v) + ((1. GF) * v) by VECTSP_1:def_17 .= ((1. GF) + (1. GF)) * v by VECTSP_1:def_15 ; hence v + u in A by A55, A65; ::_thesis: verum end; supposeA67: v <> u ; ::_thesis: v + u in A deffunc H1( set ) -> Element of the carrier of GF = 0. GF; consider f being Function of V,GF such that A68: ( f . v = 1. GF & f . u = 1. GF ) and A69: for w being Element of V st w <> v & w <> u holds f . w = H1(w) from FUNCT_2:sch_7(A67); reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8; now__::_thesis:_for_w_being_Element_of_V_st_not_w_in_{v,u}_holds_ f_._w_=_0._GF let w be Element of V; ::_thesis: ( not w in {v,u} implies f . w = 0. GF ) assume not w in {v,u} ; ::_thesis: f . w = 0. GF then ( w <> v & w <> u ) by TARSKI:def_2; hence f . w = 0. GF by A69; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def1; A70: 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 Element of V st ( x = w & f . w <> 0. GF ) ; then ( x = v or x = u ) by A69; 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 A1, A68; ::_thesis: verum end; then A71: Carrier f c= A by A65, A66, ZFMISC_1:32; A72: ( (1. GF) * u = u & (1. GF) * v = v ) by VECTSP_1:def_17; reconsider f = f as Linear_Combination of A by A71, Def4; consider F being FinSequence of V such that A73: ( F is one-to-one & rng F = Carrier f ) and A74: Sum (f (#) F) = Sum f by Def6; ( F = <*v,u*> or F = <*u,v*> ) by A67, A70, A73, FINSEQ_3:99; then ( f (#) F = <*((1. GF) * v),((1. GF) * u)*> or f (#) F = <*((1. GF) * u),((1. GF) * v)*> ) by A68, Th11; then Sum f = v + u by A74, A72, RLVECT_1:45; hence v + u in A by A53; ::_thesis: verum end; end; end; hence v + u in A ; ::_thesis: verum end; thus for b1 being Element of the carrier of GF for b2 being Element of the carrier of V holds ( not b2 in A or b1 * b2 in A ) by A55; ::_thesis: verum end; theorem :: VECTSP_6:15 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V by Lm1; theorem :: VECTSP_6:16 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Th6; hence Sum l = 0. V by Lm1; ::_thesis: verum end; theorem Th17: :: VECTSP_6:17 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for l being Linear_Combination of {v} holds Sum l = (l . v) * v proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for l being Linear_Combination of {v} holds Sum l = (l . v) * v let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for l being Linear_Combination of {v} holds Sum l = (l . v) * v let v be Element 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 Def4; 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 Def3; hence Sum l = 0. V by Lm1 .= (0. GF) * v by VECTSP_1:14 .= (l . v) * v by A2, Th3 ; ::_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 Def6; F = <*v*> by A3, FINSEQ_3:97; then l (#) F = <*((l . v) * v)*> by Th10; 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 Th18: :: VECTSP_6:18 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v1, v2 being Element 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 GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v1, v2 being Element of V st v1 <> v2 holds for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v1, v2 being Element 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 Element 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 Def4; 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 Def3; hence Sum l = 0. V by Lm1 .= (0. V) + (0. V) by RLVECT_1:4 .= ((0. GF) * v1) + (0. V) by VECTSP_1:14 .= ((0. GF) * v1) + ((0. GF) * v2) by VECTSP_1:14 .= ((l . v1) * v1) + ((0. GF) * v2) by A3, Th3 .= ((l . v1) * v1) + ((l . v2) * v2) by A3, Th3 ; ::_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 Def4; A5: not v2 in Carrier l by A1, A4, TARSKI:def_1; thus Sum l = Sum L .= (l . v1) * v1 by Th17 .= ((l . v1) * v1) + (0. V) by RLVECT_1:4 .= ((l . v1) * v1) + ((0. GF) * v2) by VECTSP_1:14 .= ((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 Def4; A7: not v1 in Carrier l by A1, A6, TARSKI:def_1; thus Sum l = Sum L .= (l . v2) * v2 by Th17 .= (0. V) + ((l . v2) * v2) by RLVECT_1:4 .= ((0. GF) * v1) + ((l . v2) * v2) by VECTSP_1:14 .= ((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 Def6; ( 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 Th11; 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 :: VECTSP_6:19 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V st Carrier L = {} holds Sum L = 0. V proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V st Carrier L = {} holds Sum L = 0. V let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Def3; hence Sum L = 0. V by Lm1; ::_thesis: verum end; theorem :: VECTSP_6:20 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L being Linear_Combination of V st Carrier L = {v} holds Sum L = (L . v) * v proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L being Linear_Combination of V st Carrier L = {v} holds Sum L = (L . v) * v let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for L being Linear_Combination of V st Carrier L = {v} holds Sum L = (L . v) * v let v be Element 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 Def4; hence Sum L = (L . v) * v by Th17; ::_thesis: verum end; theorem :: VECTSP_6:21 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v1, v2 being Element 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 GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v1, v2 being Element 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 V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v1, v2 being Element 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 Element 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, Def4; hence Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A2, Th18; ::_thesis: verum end; definition let GF be non empty ZeroStr ; let V be non empty VectSpStr over GF; let L1, L2 be Linear_Combination of V; :: original: = redefine predL1 = L2 means :: VECTSP_6:def 7 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 = VECTSP_6:def_7_:_ for GF being non empty ZeroStr for V being non empty VectSpStr over GF 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 GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; let L1, L2 be Linear_Combination of V; funcL1 + L2 -> Linear_Combination of V equals :: VECTSP_6:def 8 L1 + L2; coherence L1 + L2 is Linear_Combination of V proof set f = L1 + L2; A1: ( dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:def_1; A2: dom (L1 + L2) = (dom L1) /\ (dom L2) by VFUNCT_1:def_1; then L1 + L2 is Function of V,GF by A1, FUNCT_2:67; then A3: L1 + L2 is Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8; now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_(Carrier_L1)_\/_(Carrier_L2)_holds_ (L1_+_L2)_._v_=_0._GF let v be Element of V; ::_thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies (L1 + L2) . v = 0. GF ) assume A4: not v in (Carrier L1) \/ (Carrier L2) ; ::_thesis: (L1 + L2) . v = 0. GF then not v in Carrier L2 by XBOOLE_0:def_3; then A5: L2 . v = 0. GF ; A6: ( L1 /. v = L1 . v & L2 /. v = L2 . v ) by A1, PARTFUN1:def_6; not v in Carrier L1 by A4, XBOOLE_0:def_3; then A7: L1 . v = 0. GF ; thus (L1 + L2) . v = (L1 + L2) /. v by A1, A2, PARTFUN1:def_6 .= (0. GF) + (0. GF) by A1, A2, A5, A6, A7, VFUNCT_1:def_1 .= 0. GF by RLVECT_1:4 ; ::_thesis: verum end; hence L1 + L2 is Linear_Combination of V by A3, Def1; ::_thesis: verum end; end; :: deftheorem defines + VECTSP_6:def_8_:_ for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds L1 + L2 = L1 + L2; theorem Th22: :: VECTSP_6:22 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v) let v be Element 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) ( dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:def_1; then A1: ( L1 /. v = L1 . v & L2 /. v = L2 . v ) by PARTFUN1:def_6; A2: dom (L1 + L2) = the carrier of V by FUNCT_2:def_1; hence (L1 + L2) . v = (L1 + L2) /. v by PARTFUN1:def_6 .= (L1 . v) + (L2 . v) by A1, A2, VFUNCT_1:def_1 ; ::_thesis: verum end; theorem Th23: :: VECTSP_6:23 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Element of V such that A1: x = u and A2: (L1 + L2) . u <> 0. GF ; (L1 + L2) . u = (L1 . u) + (L2 . u) by Th22; then ( L1 . u <> 0. GF or L2 . u <> 0. GF ) by A2, RLVECT_1:4; then ( x in { v1 where v1 is Element of V : L1 . v1 <> 0. GF } or x in { v2 where v2 is Element of V : L2 . v2 <> 0. GF } ) by A1; hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th24: :: VECTSP_6:24 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF 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 GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF 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 V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Def4; then A1: (Carrier L1) \/ (Carrier L2) c= A by XBOOLE_1:8; Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by Th23; hence Carrier (L1 + L2) c= A by A1, XBOOLE_1:1; :: according to VECTSP_6:def_4 ::_thesis: verum end; theorem Th25: :: VECTSP_6:25 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1 let L1, L2 be Linear_Combination of V; ::_thesis: L1 + L2 = L2 + L1 let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: (L1 + L2) . v = (L2 + L1) . v thus (L1 + L2) . v = (L2 . v) + (L1 . v) by Th22 .= (L2 + L1) . v by Th22 ; ::_thesis: verum end; theorem :: VECTSP_6:26 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Element of V; :: according to VECTSP_6:def_7 ::_thesis: (L1 + (L2 + L3)) . v = ((L1 + L2) + L3) . v thus (L1 + (L2 + L3)) . v = (L1 . v) + ((L2 + L3) . v) by Th22 .= (L1 . v) + ((L2 . v) + (L3 . v)) by Th22 .= ((L1 . v) + (L2 . v)) + (L3 . v) by RLVECT_1:def_3 .= ((L1 + L2) . v) + (L3 . v) by Th22 .= ((L1 + L2) + L3) . v by Th22 ; ::_thesis: verum end; theorem :: VECTSP_6:27 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds ( L + (ZeroLC V) = L & (ZeroLC V) + L = L ) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Element of V; :: according to VECTSP_6:def_7 ::_thesis: (L + (ZeroLC V)) . v = L . v thus (L + (ZeroLC V)) . v = (L . v) + ((ZeroLC V) . v) by Th22 .= (L . v) + (0. GF) by Th3 .= L . v by RLVECT_1:4 ; ::_thesis: verum end; hence (ZeroLC V) + L = L by Th25; ::_thesis: verum end; definition let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; let a be Element of GF; let L be Linear_Combination of V; funca * L -> Linear_Combination of V means :Def9: :: VECTSP_6:def 9 for v being Element of V holds it . v = a * (L . v); existence ex b1 being Linear_Combination of V st for v being Element of V holds b1 . v = a * (L . v) proof deffunc H1( Element of V) -> Element of the carrier of GF = a * (L . $1); consider f being Function of the carrier of V, the carrier of GF 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, the carrier of GF) by FUNCT_2:8; now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_Carrier_L_holds_ f_._v_=_0._GF let v be Element of V; ::_thesis: ( not v in Carrier L implies f . v = 0. GF ) assume not v in Carrier L ; ::_thesis: f . v = 0. GF then L . v = 0. GF ; hence f . v = a * (0. GF) by A1 .= 0. GF by VECTSP_1:6 ; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by Def1; take f ; ::_thesis: for v being Element of V holds f . v = a * (L . v) let v be Element 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 Element of V holds b1 . v = a * (L . v) ) & ( for v being Element of V holds b2 . v = a * (L . v) ) holds b1 = b2 proof let L1, L2 be Linear_Combination of V; ::_thesis: ( ( for v being Element of V holds L1 . v = a * (L . v) ) & ( for v being Element of V holds L2 . v = a * (L . v) ) implies L1 = L2 ) assume A2: for v being Element of V holds L1 . v = a * (L . v) ; ::_thesis: ( ex v being Element of V st not L2 . v = a * (L . v) or L1 = L2 ) assume A3: for v being Element of V holds L2 . v = a * (L . v) ; ::_thesis: L1 = L2 let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: L1 . v = L2 . v thus L1 . v = a * (L . v) by A2 .= L2 . v by A3 ; ::_thesis: verum end; end; :: deftheorem Def9 defines * VECTSP_6:def_9_:_ for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a being Element of GF for L, b5 being Linear_Combination of V holds ( b5 = a * L iff for v being Element of V holds b5 . v = a * (L . v) ); theorem Th28: :: VECTSP_6:28 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a being Element of GF for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a being Element of GF for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a being Element of GF for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L let a be Element of GF; ::_thesis: for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L let L be Linear_Combination of V; ::_thesis: Carrier (a * L) c= Carrier L set T = { u where u is Element of V : (a * L) . u <> 0. GF } ; set S = { v where v is Element of V : L . v <> 0. GF } ; { u where u is Element of V : (a * L) . u <> 0. GF } c= { v where v is Element of V : L . v <> 0. GF } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Element of V : (a * L) . u <> 0. GF } or x in { v where v is Element of V : L . v <> 0. GF } ) assume x in { u where u is Element of V : (a * L) . u <> 0. GF } ; ::_thesis: x in { v where v is Element of V : L . v <> 0. GF } then consider u being Element of V such that A1: x = u and A2: (a * L) . u <> 0. GF ; (a * L) . u = a * (L . u) by Def9; then L . u <> 0. GF by A2, VECTSP_1:6; hence x in { v where v is Element of V : L . v <> 0. GF } by A1; ::_thesis: verum end; hence Carrier (a * L) c= Carrier L ; ::_thesis: verum end; theorem Th29: :: VECTSP_6:29 for GF being Field for V being VectSp of GF for a being Element of GF for L being Linear_Combination of V st a <> 0. GF holds Carrier (a * L) = Carrier L proof let GF be Field; ::_thesis: for V being VectSp of GF for a being Element of GF for L being Linear_Combination of V st a <> 0. GF holds Carrier (a * L) = Carrier L let V be VectSp of GF; ::_thesis: for a being Element of GF for L being Linear_Combination of V st a <> 0. GF holds Carrier (a * L) = Carrier L let a be Element of GF; ::_thesis: for L being Linear_Combination of V st a <> 0. GF holds Carrier (a * L) = Carrier L let L be Linear_Combination of V; ::_thesis: ( a <> 0. GF implies Carrier (a * L) = Carrier L ) set T = { u where u is Vector of V : (a * L) . u <> 0. GF } ; set S = { v where v is Vector of V : L . v <> 0. GF } ; assume A1: a <> 0. GF ; ::_thesis: Carrier (a * L) = Carrier L { u where u is Vector of V : (a * L) . u <> 0. GF } = { v where v is Vector of V : L . v <> 0. GF } proof thus { u where u is Vector of V : (a * L) . u <> 0. GF } c= { v where v is Vector of V : L . v <> 0. GF } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is Vector of V : L . v <> 0. GF } c= { u where u is Vector of V : (a * L) . u <> 0. GF } 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. GF } or x in { v where v is Vector of V : L . v <> 0. GF } ) assume x in { u where u is Vector of V : (a * L) . u <> 0. GF } ; ::_thesis: x in { v where v is Vector of V : L . v <> 0. GF } then consider u being Vector of V such that A2: x = u and A3: (a * L) . u <> 0. GF ; (a * L) . u = a * (L . u) by Def9; then L . u <> 0. GF by A3, VECTSP_1:7; hence x in { v where v is Vector of V : L . v <> 0. GF } 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. GF } or x in { u where u is Vector of V : (a * L) . u <> 0. GF } ) assume x in { v where v is Vector of V : L . v <> 0. GF } ; ::_thesis: x in { u where u is Vector of V : (a * L) . u <> 0. GF } then consider v being Vector of V such that A4: x = v and A5: L . v <> 0. GF ; (a * L) . v = a * (L . v) by Def9; then (a * L) . v <> 0. GF by A1, A5, VECTSP_1:12; hence x in { u where u is Vector of V : (a * L) . u <> 0. GF } by A4; ::_thesis: verum end; hence Carrier (a * L) = Carrier L ; ::_thesis: verum end; theorem Th30: :: VECTSP_6:30 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V let L be Linear_Combination of V; ::_thesis: (0. GF) * L = ZeroLC V let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: ((0. GF) * L) . v = (ZeroLC V) . v thus ((0. GF) * L) . v = (0. GF) * (L . v) by Def9 .= 0. GF by VECTSP_1:7 .= (ZeroLC V) . v by Th3 ; ::_thesis: verum end; theorem Th31: :: VECTSP_6:31 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a being Element of GF 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 GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a being Element of GF 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 V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a being Element of GF 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 Element of GF; ::_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 L is Linear_Combination of A ; ::_thesis: a * L is Linear_Combination of A then A1: Carrier L c= A by Def4; Carrier (a * L) c= Carrier L by Th28; then Carrier (a * L) c= A by A1, XBOOLE_1:1; hence a * L is Linear_Combination of A by Def4; ::_thesis: verum end; theorem :: VECTSP_6:32 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a, b being Element of GF for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a, b being Element of GF for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a, b being Element of GF for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L) let a, b be Element of GF; ::_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 Element of V; :: according to VECTSP_6:def_7 ::_thesis: ((a + b) * L) . v = ((a * L) + (b * L)) . v thus ((a + b) * L) . v = (a + b) * (L . v) by Def9 .= (a * (L . v)) + (b * (L . v)) by VECTSP_1:def_7 .= ((a * L) . v) + (b * (L . v)) by Def9 .= ((a * L) . v) + ((b * L) . v) by Def9 .= ((a * L) + (b * L)) . v by Th22 ; ::_thesis: verum end; theorem :: VECTSP_6:33 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a being Element of GF for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a being Element of GF for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a being Element of GF for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2) let a be Element of GF; ::_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 Element of V; :: according to VECTSP_6:def_7 ::_thesis: (a * (L1 + L2)) . v = ((a * L1) + (a * L2)) . v thus (a * (L1 + L2)) . v = a * ((L1 + L2) . v) by Def9 .= a * ((L1 . v) + (L2 . v)) by Th22 .= (a * (L1 . v)) + (a * (L2 . v)) by VECTSP_1:def_7 .= ((a * L1) . v) + (a * (L2 . v)) by Def9 .= ((a * L1) . v) + ((a * L2) . v) by Def9 .= ((a * L1) + (a * L2)) . v by Th22 ; ::_thesis: verum end; theorem Th34: :: VECTSP_6:34 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a, b being Element of GF for L being Linear_Combination of V holds a * (b * L) = (a * b) * L proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for a, b being Element of GF for L being Linear_Combination of V holds a * (b * L) = (a * b) * L let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a, b being Element of GF for L being Linear_Combination of V holds a * (b * L) = (a * b) * L let a, b be Element of GF; ::_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 Element of V; :: according to VECTSP_6:def_7 ::_thesis: (a * (b * L)) . v = ((a * b) * L) . v thus (a * (b * L)) . v = a * ((b * L) . v) by Def9 .= a * (b * (L . v)) by Def9 .= (a * b) * (L . v) by GROUP_1:def_3 .= ((a * b) * L) . v by Def9 ; ::_thesis: verum end; theorem :: VECTSP_6:35 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds (1. GF) * L = L proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds (1. GF) * L = L let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds (1. GF) * L = L let L be Linear_Combination of V; ::_thesis: (1. GF) * L = L let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: ((1. GF) * L) . v = L . v thus ((1. GF) * L) . v = (1. GF) * (L . v) by Def9 .= L . v by VECTSP_1:def_8 ; ::_thesis: verum end; definition let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; let L be Linear_Combination of V; func - L -> Linear_Combination of V equals :: VECTSP_6:def 10 (- (1. GF)) * L; correctness coherence (- (1. GF)) * L is Linear_Combination of V; ; involutiveness for b1, b2 being Linear_Combination of V st b1 = (- (1. GF)) * b2 holds b2 = (- (1. GF)) * b1 proof let L, L9 be Linear_Combination of V; ::_thesis: ( L = (- (1. GF)) * L9 implies L9 = (- (1. GF)) * L ) assume A1: L = (- (1. GF)) * L9 ; ::_thesis: L9 = (- (1. GF)) * L let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: L9 . v = ((- (1. GF)) * L) . v thus L9 . v = (1. GF) * (L9 . v) by VECTSP_1:def_8 .= ((1. GF) * (1. GF)) * (L9 . v) by VECTSP_1:def_8 .= ((- (1. GF)) * (- (1. GF))) * (L9 . v) by VECTSP_1:10 .= (((- (1. GF)) * (- (1. GF))) * L9) . v by Def9 .= ((- (1. GF)) * L) . v by A1, Th34 ; ::_thesis: verum end; end; :: deftheorem defines - VECTSP_6:def_10_:_ for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds - L = (- (1. GF)) * L; Lm2: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for a being Element of GF holds (- (1. GF)) * a = - a proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of GF holds (- (1. GF)) * a = - a let a be Element of GF; ::_thesis: (- (1. GF)) * a = - a thus (- (1. GF)) * a = ((0. GF) - (1. GF)) * a by RLVECT_1:14 .= ((0. GF) * a) - ((1. GF) * a) by VECTSP_1:13 .= (0. GF) - ((1. GF) * a) by VECTSP_1:7 .= - ((1. GF) * a) by RLVECT_1:14 .= - a by VECTSP_1:def_8 ; ::_thesis: verum end; theorem Th36: :: VECTSP_6:36 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L being Linear_Combination of V holds (- L) . v = - (L . v) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L being Linear_Combination of V holds (- L) . v = - (L . v) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for L being Linear_Combination of V holds (- L) . v = - (L . v) let v be Element 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. GF)) * (L . v) by Def9 .= - (L . v) by Lm2 ; ::_thesis: verum end; theorem :: VECTSP_6:37 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds L2 = - L1 proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds L2 = - L1 let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Element of V; :: according to VECTSP_6:def_7 ::_thesis: L2 . v = (- L1) . v (L1 . v) + (L2 . v) = (ZeroLC V) . v by A1, Th22 .= 0. GF by Th3 ; hence L2 . v = - (L1 . v) by RLVECT_1:6 .= (- L1) . v by Th36 ; ::_thesis: verum end; Lm3: for GF being Field holds - (1. GF) <> 0. GF proof let GF be Field; ::_thesis: - (1. GF) <> 0. GF assume not - (1. GF) <> 0. GF ; ::_thesis: contradiction then 1. GF = - (0. GF) by RLVECT_1:17; hence contradiction by RLVECT_1:12; ::_thesis: verum end; theorem Th38: :: VECTSP_6:38 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds Carrier (- L) = Carrier L proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds Carrier (- L) = Carrier L let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds Carrier (- L) = Carrier L let L be Linear_Combination of V; ::_thesis: Carrier (- L) = Carrier L ( Carrier (- L) c= Carrier L & Carrier (- (- L)) c= Carrier (- L) ) by Th28; hence Carrier (- L) = Carrier L by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: VECTSP_6:39 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF 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 Th31; definition let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; let L1, L2 be Linear_Combination of V; funcL1 - L2 -> Linear_Combination of V equals :: VECTSP_6:def 11 L1 + (- L2); coherence L1 + (- L2) is Linear_Combination of V ; end; :: deftheorem defines - VECTSP_6:def_11_:_ for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2); theorem Th40: :: VECTSP_6:40 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for v being Element of V for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) let v be Element 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 Th22 .= (L1 . v) + (- (L2 . v)) by Th36 .= (L1 . v) - (L2 . v) by RLVECT_1:def_11 ; ::_thesis: verum end; theorem :: VECTSP_6:41 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Th23; hence Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by Th38; ::_thesis: verum end; theorem :: VECTSP_6:42 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF 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 GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF 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 V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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, Th31; hence L1 - L2 is Linear_Combination of A by A1, Th24; ::_thesis: verum end; theorem Th43: :: VECTSP_6:43 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds L - L = ZeroLC V proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds L - L = ZeroLC V let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_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 Element of V; :: according to VECTSP_6:def_7 ::_thesis: (L - L) . v = (ZeroLC V) . v thus (L - L) . v = (L . v) - (L . v) by Th40 .= 0. GF by RLVECT_1:15 .= (ZeroLC V) . v by Th3 ; ::_thesis: verum end; theorem Th44: :: VECTSP_6:44 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2) let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 + L2) = (Sum L1) + (Sum L2) set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2); set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1); consider p being FinSequence such that A1: rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) and A2: p is one-to-one by FINSEQ_4:58; reconsider p = p as FinSequence of the carrier of V by A1, FINSEQ_1:def_4; A3: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2)) by XBOOLE_1:4; set C3 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)); consider r being FinSequence such that A4: rng r = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) and A5: r is one-to-one by FINSEQ_4:58; reconsider r = r as FinSequence of the carrier of V by A4, FINSEQ_1:def_4; A6: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2)) by XBOOLE_1:4; set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2); consider q being FinSequence such that A7: rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) and A8: q is one-to-one by FINSEQ_4:58; reconsider q = q as FinSequence of the carrier of V by A7, FINSEQ_1:def_4; consider F being FinSequence of V such that A9: F is one-to-one and A10: rng F = Carrier (L1 + L2) and A11: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by Def6; set FF = F ^ r; consider G being FinSequence of V such that A12: G is one-to-one and A13: rng G = Carrier L1 and A14: Sum (L1 (#) G) = Sum L1 by Def6; rng (F ^ r) = (rng F) \/ (rng r) by FINSEQ_1:31; then rng (F ^ r) = (Carrier (L1 + L2)) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A10, A4, XBOOLE_1:39; then A15: rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A6, XBOOLE_1:7, XBOOLE_1:12; set GG = G ^ p; rng (G ^ p) = (rng G) \/ (rng p) by FINSEQ_1:31; then rng (G ^ p) = (Carrier L1) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A13, A1, XBOOLE_1:39; then A16: rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A3, XBOOLE_1:7, XBOOLE_1:12; rng F misses rng r proof set x = the Element of (rng F) /\ (rng r); assume not rng F misses rng r ; ::_thesis: contradiction then (rng F) /\ (rng r) <> {} by XBOOLE_0:def_7; then ( the Element of (rng F) /\ (rng r) in Carrier (L1 + L2) & the Element of (rng F) /\ (rng r) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) ) by A10, A4, XBOOLE_0:def_4; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then A17: F ^ r is one-to-one by A9, A5, FINSEQ_3:91; rng G misses rng p proof set x = the Element of (rng G) /\ (rng p); assume not rng G misses rng p ; ::_thesis: contradiction then (rng G) /\ (rng p) <> {} by XBOOLE_0:def_7; then ( the Element of (rng G) /\ (rng p) in Carrier L1 & the Element of (rng G) /\ (rng p) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) ) by A13, A1, XBOOLE_0:def_4; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then A18: G ^ p is one-to-one by A12, A2, FINSEQ_3:91; then A19: len (G ^ p) = len (F ^ r) by A17, A16, A15, FINSEQ_1:48; deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . $1); consider P being FinSequence such that A20: len P = len (F ^ r) and A21: for k being Nat st k in dom P holds P . k = H1(k) from FINSEQ_1:sch_2(); A22: dom P = Seg (len (F ^ r)) by A20, FINSEQ_1:def_3; A23: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_ (G_^_p)_._x_=_(F_^_r)_._(P_._x) let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (F ^ r) . (P . x) ) assume A24: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (F ^ r) . (P . x) then reconsider n = x as Element of NAT by FINSEQ_3:23; (G ^ p) . n in rng (F ^ r) by A16, A15, A24, FUNCT_1:def_3; then A25: F ^ r just_once_values (G ^ p) . n by A17, FINSEQ_4:8; n in Seg (len (F ^ r)) by A19, A24, FINSEQ_1:def_3; then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A21, A22 .= (G ^ p) . n by A25, FINSEQ_4:def_3 ; hence (G ^ p) . x = (F ^ r) . (P . x) ; ::_thesis: verum end; A26: rng P c= dom (F ^ r) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in dom (F ^ r) ) assume x in rng P ; ::_thesis: x in dom (F ^ r) then consider y being set such that A27: y in dom P and A28: P . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A27, FINSEQ_3:23; y in dom (G ^ p) by A19, A20, A27, FINSEQ_3:29; then (G ^ p) . y in rng (F ^ r) by A16, A15, FUNCT_1:def_3; then A29: F ^ r just_once_values (G ^ p) . y by A17, FINSEQ_4:8; P . y = (F ^ r) <- ((G ^ p) . y) by A21, A27; hence x in dom (F ^ r) by A28, A29, FINSEQ_4:def_3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_implies_x_in_dom_(G_^_p)_)_) let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) ) thus ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) ::_thesis: ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) proof assume x in dom (G ^ p) ; ::_thesis: ( x in dom P & P . x in dom (F ^ r) ) then x in Seg (len P) by A19, A20, FINSEQ_1:def_3; hence x in dom P by FINSEQ_1:def_3; ::_thesis: P . x in dom (F ^ r) then P . x in rng P by FUNCT_1:def_3; hence P . x in dom (F ^ r) by A26; ::_thesis: verum end; assume that A30: x in dom P and P . x in dom (F ^ r) ; ::_thesis: x in dom (G ^ p) x in Seg (len P) by A30, FINSEQ_1:def_3; hence x in dom (G ^ p) by A19, A20, FINSEQ_1:def_3; ::_thesis: verum end; then A31: G ^ p = (F ^ r) * P by A23, FUNCT_1:10; dom (F ^ r) c= rng P proof set f = ((F ^ r) ") * (G ^ p); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (F ^ r) or x in rng P ) assume A32: x in dom (F ^ r) ; ::_thesis: x in rng P dom ((F ^ r) ") = rng (G ^ p) by A17, A16, A15, FUNCT_1:33; then A33: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28 .= dom (F ^ r) by A17, FUNCT_1:33 ; ((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by A31, RELAT_1:36 .= (id (dom (F ^ r))) * P by A17, FUNCT_1:39 .= P by A26, RELAT_1:53 ; hence x in rng P by A32, A33; ::_thesis: verum end; then A34: dom (F ^ r) = rng P by A26, XBOOLE_0:def_10; A35: len r = len ((L1 + L2) (#) r) by Def5; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_ ((L1_+_L2)_(#)_r)_._k_=_(0._GF)_*_(r_/._k) let k be Element of NAT ; ::_thesis: ( k in dom r implies ((L1 + L2) (#) r) . k = (0. GF) * (r /. k) ) assume A36: k in dom r ; ::_thesis: ((L1 + L2) (#) r) . k = (0. GF) * (r /. k) then r /. k = r . k by PARTFUN1:def_6; then r /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) by A4, A36, FUNCT_1:def_3; then A37: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def_5; k in dom ((L1 + L2) (#) r) by A35, A36, FINSEQ_3:29; then ((L1 + L2) (#) r) . k = ((L1 + L2) . (r /. k)) * (r /. k) by Def5; hence ((L1 + L2) (#) r) . k = (0. GF) * (r /. k) by A37; ::_thesis: verum end; then A38: Sum ((L1 + L2) (#) r) = (0. GF) * (Sum r) by A35, RLVECT_2:67 .= 0. V by VECTSP_1:14 ; A39: len p = len (L1 (#) p) by Def5; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_ (L1_(#)_p)_._k_=_(0._GF)_*_(p_/._k) let k be Element of NAT ; ::_thesis: ( k in dom p implies (L1 (#) p) . k = (0. GF) * (p /. k) ) assume A40: k in dom p ; ::_thesis: (L1 (#) p) . k = (0. GF) * (p /. k) then p /. k = p . k by PARTFUN1:def_6; then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by A1, A40, FUNCT_1:def_3; then A41: not p /. k in Carrier L1 by XBOOLE_0:def_5; k in dom (L1 (#) p) by A39, A40, FINSEQ_3:29; then (L1 (#) p) . k = (L1 . (p /. k)) * (p /. k) by Def5; hence (L1 (#) p) . k = (0. GF) * (p /. k) by A41; ::_thesis: verum end; then A42: Sum (L1 (#) p) = (0. GF) * (Sum p) by A39, RLVECT_2:67 .= 0. V by VECTSP_1:14 ; A43: len q = len (L2 (#) q) by Def5; now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_q_holds_ (L2_(#)_q)_._k_=_(0._GF)_*_(q_/._k) let k be Element of NAT ; ::_thesis: ( k in dom q implies (L2 (#) q) . k = (0. GF) * (q /. k) ) assume A44: k in dom q ; ::_thesis: (L2 (#) q) . k = (0. GF) * (q /. k) then q /. k = q . k by PARTFUN1:def_6; then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by A7, A44, FUNCT_1:def_3; then A45: not q /. k in Carrier L2 by XBOOLE_0:def_5; k in dom (L2 (#) q) by A43, A44, FINSEQ_3:29; then (L2 (#) q) . k = (L2 . (q /. k)) * (q /. k) by Def5; hence (L2 (#) q) . k = (0. GF) * (q /. k) by A45; ::_thesis: verum end; then A46: Sum (L2 (#) q) = (0. GF) * (Sum q) by A43, RLVECT_2:67 .= 0. V by VECTSP_1:14 ; set g = L1 (#) (G ^ p); A47: len (L1 (#) (G ^ p)) = len (G ^ p) by Def5; then A48: Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by FINSEQ_1:def_3; set f = (L1 + L2) (#) (F ^ r); consider H being FinSequence of V such that A49: H is one-to-one and A50: rng H = Carrier L2 and A51: Sum (L2 (#) H) = Sum L2 by Def6; set HH = H ^ q; rng H misses rng q proof set x = the Element of (rng H) /\ (rng q); assume not rng H misses rng q ; ::_thesis: contradiction then (rng H) /\ (rng q) <> {} by XBOOLE_0:def_7; then ( the Element of (rng H) /\ (rng q) in Carrier L2 & the Element of (rng H) /\ (rng q) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) ) by A50, A7, XBOOLE_0:def_4; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then A52: H ^ q is one-to-one by A49, A8, FINSEQ_3:91; rng (H ^ q) = (rng H) \/ (rng q) by FINSEQ_1:31; then rng (H ^ q) = (Carrier L2) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A50, A7, XBOOLE_1:39; then A53: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by XBOOLE_1:7, XBOOLE_1:12; then A54: len (G ^ p) = len (H ^ q) by A52, A18, A16, FINSEQ_1:48; deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . $1); consider R being FinSequence such that A55: len R = len (H ^ q) and A56: for k being Nat st k in dom R holds R . k = H2(k) from FINSEQ_1:sch_2(); A57: dom R = Seg (len (H ^ q)) by A55, FINSEQ_1:def_3; A58: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_ (G_^_p)_._x_=_(H_^_q)_._(R_._x) let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (H ^ q) . (R . x) ) assume A59: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (H ^ q) . (R . x) then reconsider n = x as Element of NAT by FINSEQ_3:23; (G ^ p) . n in rng (H ^ q) by A16, A53, A59, FUNCT_1:def_3; then A60: H ^ q just_once_values (G ^ p) . n by A52, FINSEQ_4:8; n in Seg (len (H ^ q)) by A54, A59, FINSEQ_1:def_3; then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A56, A57 .= (G ^ p) . n by A60, FINSEQ_4:def_3 ; hence (G ^ p) . x = (H ^ q) . (R . x) ; ::_thesis: verum end; A61: rng R c= dom (H ^ q) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng R or x in dom (H ^ q) ) assume x in rng R ; ::_thesis: x in dom (H ^ q) then consider y being set such that A62: y in dom R and A63: R . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A62, FINSEQ_3:23; y in dom (G ^ p) by A54, A55, A62, FINSEQ_3:29; then (G ^ p) . y in rng (H ^ q) by A16, A53, FUNCT_1:def_3; then A64: H ^ q just_once_values (G ^ p) . y by A52, FINSEQ_4:8; R . y = (H ^ q) <- ((G ^ p) . y) by A56, A62; hence x in dom (H ^ q) by A63, A64, FINSEQ_4:def_3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_)_)_&_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_implies_x_in_dom_(G_^_p)_)_) let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) ) thus ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) ::_thesis: ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) proof assume x in dom (G ^ p) ; ::_thesis: ( x in dom R & R . x in dom (H ^ q) ) then x in Seg (len R) by A54, A55, FINSEQ_1:def_3; hence x in dom R by FINSEQ_1:def_3; ::_thesis: R . x in dom (H ^ q) then R . x in rng R by FUNCT_1:def_3; hence R . x in dom (H ^ q) by A61; ::_thesis: verum end; assume that A65: x in dom R and R . x in dom (H ^ q) ; ::_thesis: x in dom (G ^ p) x in Seg (len R) by A65, FINSEQ_1:def_3; hence x in dom (G ^ p) by A54, A55, FINSEQ_1:def_3; ::_thesis: verum end; then A66: G ^ p = (H ^ q) * R by A58, FUNCT_1:10; dom (H ^ q) c= rng R proof set f = ((H ^ q) ") * (G ^ p); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (H ^ q) or x in rng R ) assume A67: x in dom (H ^ q) ; ::_thesis: x in rng R dom ((H ^ q) ") = rng (G ^ p) by A52, A16, A53, FUNCT_1:33; then A68: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28 .= dom (H ^ q) by A52, FUNCT_1:33 ; ((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by A66, RELAT_1:36 .= (id (dom (H ^ q))) * R by A52, FUNCT_1:39 .= R by A61, RELAT_1:53 ; hence x in rng R by A67, A68; ::_thesis: verum end; then A69: dom (H ^ q) = rng R by A61, XBOOLE_0:def_10; set h = L2 (#) (H ^ q); A70: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Th13 .= (Sum (L2 (#) H)) + (0. V) by A46, RLVECT_1:41 .= Sum (L2 (#) H) by RLVECT_1:4 ; A71: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Th13 .= (Sum (L1 (#) G)) + (0. V) by A42, RLVECT_1:41 .= Sum (L1 (#) G) by RLVECT_1:4 ; A72: dom P = dom (F ^ r) by A20, FINSEQ_3:29; then A73: P is one-to-one by A34, FINSEQ_4:60; A74: dom R = dom (H ^ q) by A55, FINSEQ_3:29; then A75: R is one-to-one by A69, FINSEQ_4:60; reconsider R = R as Function of (dom (H ^ q)),(dom (H ^ q)) by A61, A74, FUNCT_2:2; reconsider R = R as Permutation of (dom (H ^ q)) by A69, A75, FUNCT_2:57; A76: len (L2 (#) (H ^ q)) = len (H ^ q) by Def5; then dom (L2 (#) (H ^ q)) = dom (H ^ q) by FINSEQ_3:29; then reconsider R = R as Permutation of (dom (L2 (#) (H ^ q))) ; reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of the carrier of V by FINSEQ_2:47; A77: len Hp = len (G ^ p) by A54, A76, FINSEQ_2:44; reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by A26, A72, FUNCT_2:2; reconsider P = P as Permutation of (dom (F ^ r)) by A34, A73, FUNCT_2:57; A78: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by Def5; then dom ((L1 + L2) (#) (F ^ r)) = dom (F ^ r) by FINSEQ_3:29; then reconsider P = P as Permutation of (dom ((L1 + L2) (#) (F ^ r))) ; reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of the carrier of V by FINSEQ_2:47; A79: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Th13 .= (Sum ((L1 + L2) (#) F)) + (0. V) by A38, RLVECT_1:41 .= Sum ((L1 + L2) (#) F) by RLVECT_1:4 ; deffunc H3( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1); consider I being FinSequence such that A80: len I = len (G ^ p) and A81: for k being Nat st k in dom I holds I . k = H3(k) from FINSEQ_1:sch_2(); A82: dom I = Seg (len (G ^ p)) by A80, FINSEQ_1:def_3; then A83: for k being Element of NAT st k in Seg (len (G ^ p)) holds I . k = H3(k) by A81; 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 A84: y in dom I and A85: I . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A84, FINSEQ_3:23; I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by A81, A84; hence x in the carrier of V by A85; ::_thesis: verum end; then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def_4; A86: len Fp = len I by A19, A78, A80, FINSEQ_2:44; A87: now__::_thesis:_for_x_being_set_st_x_in_Seg_(len_I)_holds_ I_._x_=_Fp_._x let x be set ; ::_thesis: ( x in Seg (len I) implies I . x = Fp . x ) assume A88: x in Seg (len I) ; ::_thesis: I . x = Fp . x then reconsider k = x as Element of NAT ; A89: x in dom Hp by A80, A77, A88, FINSEQ_1:def_3; then A90: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def_6 .= (L2 (#) (H ^ q)) . (R . k) by A89, FUNCT_1:12 ; set v = (G ^ p) /. k; x in dom Fp by A86, A88, FINSEQ_1:def_3; then A91: Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k) by FUNCT_1:12; A92: x in dom (H ^ q) by A54, A80, A88, FINSEQ_1:def_3; then R . k in dom R by A69, A74, FUNCT_1:def_3; then reconsider j = R . k as Element of NAT by FINSEQ_3:23; A93: x in dom (G ^ p) by A80, A88, FINSEQ_1:def_3; then A94: (H ^ q) . j = (G ^ p) . k by A58 .= (G ^ p) /. k by A93, PARTFUN1:def_6 ; A95: dom (F ^ r) = dom (G ^ p) by A19, FINSEQ_3:29; then P . k in dom P by A34, A72, A93, FUNCT_1:def_3; then reconsider l = P . k as Element of NAT by FINSEQ_3:23; A96: (F ^ r) . l = (G ^ p) . k by A23, A93 .= (G ^ p) /. k by A93, PARTFUN1:def_6 ; R . k in dom (H ^ q) by A69, A74, A92, FUNCT_1:def_3; then A97: (L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A94, Th8; P . k in dom (F ^ r) by A34, A72, A93, A95, FUNCT_1:def_3; then A98: ((L1 + L2) (#) (F ^ r)) . l = ((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k) by A96, Th8 .= ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k) by Th22 .= ((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)) by VECTSP_1:def_15 ; A99: x in dom (L1 (#) (G ^ p)) by A80, A47, A88, FINSEQ_1:def_3; then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def_6 .= (L1 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A99, Def5 ; hence I . x = Fp . x by A80, A81, A82, A88, A90, A97, A91, A98; ::_thesis: verum end; ( dom I = Seg (len I) & dom Fp = Seg (len I) ) by A86, FINSEQ_1:def_3; then A100: I = Fp by A87, FUNCT_1:2; ( Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) & Sum Hp = Sum (L2 (#) (H ^ q)) ) by RLVECT_2:7; hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A11, A14, A51, A71, A70, A79, A80, A83, A77, A47, A100, A48, RLVECT_2:2; ::_thesis: verum end; theorem :: VECTSP_6:45 for GF being Field for V being VectSp of GF for L being Linear_Combination of V for a being Element of GF holds Sum (a * L) = a * (Sum L) proof let GF be Field; ::_thesis: for V being VectSp of GF for L being Linear_Combination of V for a being Element of GF holds Sum (a * L) = a * (Sum L) let V be VectSp of GF; ::_thesis: for L being Linear_Combination of V for a being Element of GF holds Sum (a * L) = a * (Sum L) let L be Linear_Combination of V; ::_thesis: for a being Element of GF holds Sum (a * L) = a * (Sum L) let a be Element of GF; ::_thesis: Sum (a * L) = a * (Sum L) percases ( a <> 0. GF or a = 0. GF ) ; supposeA1: a <> 0. GF ; ::_thesis: Sum (a * L) = a * (Sum L) set l = a * L; consider F being FinSequence of the carrier of V such that A2: F is one-to-one and A3: rng F = Carrier (a * L) and A4: Sum (a * L) = Sum ((a * L) (#) F) by Def6; consider G being FinSequence of the carrier of V such that A5: G is one-to-one and A6: rng G = Carrier L and A7: Sum L = Sum (L (#) G) by Def6; A8: len G = len F by A1, A2, A3, A5, A6, Th29, FINSEQ_1:48; set f = (a * L) (#) F; set g = L (#) G; deffunc H1( Nat) -> set = F <- (G . $1); consider P being FinSequence such that A9: len P = len F and A10: for k being Nat st k in dom P holds P . k = H1(k) from FINSEQ_1:sch_2(); A11: Carrier (a * L) = Carrier L by A1, Th29; A12: rng P c= Seg (len F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in Seg (len F) ) assume x in rng P ; ::_thesis: x in Seg (len F) then consider y being set such that A13: y in dom P and A14: P . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A13, FINSEQ_3:23; y in Seg (len F) by A9, A13, FINSEQ_1:def_3; then y in dom G by A8, FINSEQ_1:def_3; then G . y in rng F by A3, A6, A11, FUNCT_1:def_3; then A15: F just_once_values G . y by A2, FINSEQ_4:8; P . y = F <- (G . y) by A10, A13; then P . y in dom F by A15, FINSEQ_4:def_3; hence x in Seg (len F) by A14, FINSEQ_1:def_3; ::_thesis: verum end; A16: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_G_implies_(_x_in_dom_P_&_P_._x_in_dom_F_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_F_implies_x_in_dom_G_)_) let x be set ; ::_thesis: ( ( x in dom G implies ( x in dom P & P . x in dom F ) ) & ( x in dom P & P . x in dom F implies x in dom G ) ) thus ( x in dom G implies ( x in dom P & P . x in dom F ) ) ::_thesis: ( x in dom P & P . x in dom F implies x in dom G ) proof assume x in dom G ; ::_thesis: ( x in dom P & P . x in dom F ) then x in Seg (len P) by A9, A8, FINSEQ_1:def_3; hence x in dom P by FINSEQ_1:def_3; ::_thesis: P . x in dom F then P . x in rng P by FUNCT_1:def_3; then P . x in Seg (len F) by A12; hence P . x in dom F by FINSEQ_1:def_3; ::_thesis: verum end; assume that A17: x in dom P and P . x in dom F ; ::_thesis: x in dom G x in Seg (len P) by A17, FINSEQ_1:def_3; hence x in dom G by A9, A8, FINSEQ_1:def_3; ::_thesis: verum end; A18: dom P = Seg (len F) by A9, FINSEQ_1:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_G_holds_ G_._x_=_F_._(P_._x) let x be set ; ::_thesis: ( x in dom G implies G . x = F . (P . x) ) assume A19: x in dom G ; ::_thesis: G . x = F . (P . x) then reconsider n = x as Element of NAT by FINSEQ_3:23; G . n in rng F by A3, A6, A11, A19, FUNCT_1:def_3; then A20: F just_once_values G . n by A2, FINSEQ_4:8; n in Seg (len F) by A8, A19, FINSEQ_1:def_3; then F . (P . n) = F . (F <- (G . n)) by A10, A18 .= G . n by A20, FINSEQ_4:def_3 ; hence G . x = F . (P . x) ; ::_thesis: verum end; then A21: G = F * P by A16, FUNCT_1:10; Seg (len F) c= rng P proof set f = (F ") * G; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg (len F) or x in rng P ) assume A22: x in Seg (len F) ; ::_thesis: x in rng P dom (F ") = rng G by A2, A3, A6, A11, FUNCT_1:33; then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28 .= dom F by A2, FUNCT_1:33 ; A24: rng P c= dom F by A12, FINSEQ_1:def_3; (F ") * G = ((F ") * F) * P by A21, RELAT_1:36 .= (id (dom F)) * P by A2, FUNCT_1:39 .= P by A24, RELAT_1:53 ; hence x in rng P by A22, A23, FINSEQ_1:def_3; ::_thesis: verum end; then A25: Seg (len F) = rng P by A12, XBOOLE_0:def_10; A26: dom P = Seg (len F) by A9, FINSEQ_1:def_3; then A27: P is one-to-one by A25, FINSEQ_4:60; reconsider P = P as Function of (Seg (len F)),(Seg (len F)) by A12, A26, FUNCT_2:2; reconsider P = P as Permutation of (Seg (len F)) by A25, A27, FUNCT_2:57; A28: len ((a * L) (#) F) = len F by Def5; then dom ((a * L) (#) F) = Seg (len F) by FINSEQ_1:def_3; then reconsider P = P as Permutation of (dom ((a * L) (#) F)) ; reconsider Fp = ((a * L) (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47; A29: len Fp = len ((a * L) (#) F) by FINSEQ_2:44; then A30: len Fp = len (L (#) G) by A8, A28, Def5; A31: now__::_thesis:_for_k_being_Element_of_NAT_ for_v_being_Vector_of_V_st_k_in_dom_(L_(#)_G)_&_v_=_(L_(#)_G)_._k_holds_ Fp_._k_=_a_*_v let k be Element of NAT ; ::_thesis: for v being Vector of V st k in dom (L (#) G) & v = (L (#) G) . k holds Fp . k = a * v let v be Vector of V; ::_thesis: ( k in dom (L (#) G) & v = (L (#) G) . k implies Fp . k = a * v ) assume that A32: k in dom (L (#) G) and A33: v = (L (#) G) . k ; ::_thesis: Fp . k = a * v A34: k in Seg (len (L (#) G)) by A32, FINSEQ_1:def_3; then A35: k in dom P by A9, A28, A29, A30, FINSEQ_1:def_3; A36: k in dom G by A8, A28, A29, A30, A34, FINSEQ_1:def_3; then G . k in rng G by FUNCT_1:def_3; then F just_once_values G . k by A2, A3, A6, A11, FINSEQ_4:8; then A37: F <- (G . k) in dom F by FINSEQ_4:def_3; then reconsider i = F <- (G . k) as Element of NAT by FINSEQ_3:23; A38: G /. k = G . k by A36, PARTFUN1:def_6 .= F . (P . k) by A21, A35, FUNCT_1:13 .= F . i by A10, A18, A28, A29, A30, A34 .= F /. i by A37, PARTFUN1:def_6 ; i in Seg (len ((a * L) (#) F)) by A28, A37, FINSEQ_1:def_3; then A39: i in dom ((a * L) (#) F) by FINSEQ_1:def_3; thus Fp . k = ((a * L) (#) F) . (P . k) by A35, FUNCT_1:13 .= ((a * L) (#) F) . (F <- (G . k)) by A10, A18, A28, A29, A30, A34 .= ((a * L) . (F /. i)) * (F /. i) by A39, Def5 .= (a * (L . (F /. i))) * (F /. i) by Def9 .= a * ((L . (F /. i)) * (F /. i)) by VECTSP_1:def_16 .= a * v by A32, A33, A38, Def5 ; ::_thesis: verum end; ( Sum Fp = Sum ((a * L) (#) F) & dom Fp = dom (L (#) G) ) by A30, FINSEQ_3:29, RLVECT_2:7; hence Sum (a * L) = a * (Sum L) by A4, A7, A30, A31, RLVECT_2:66; ::_thesis: verum end; supposeA40: a = 0. GF ; ::_thesis: Sum (a * L) = a * (Sum L) hence Sum (a * L) = Sum (ZeroLC V) by Th30 .= 0. V by Lm1 .= a * (Sum L) by A40, VECTSP_1:14 ; ::_thesis: verum end; end; end; theorem Th46: :: VECTSP_6:46 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds Sum (- L) = - (Sum L) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L being Linear_Combination of V holds Sum (- L) = - (Sum L) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds Sum (- L) = - (Sum L) let L be Linear_Combination of V; ::_thesis: Sum (- L) = - (Sum L) (Sum L) + (Sum (- L)) = Sum (L - L) by Th44 .= Sum (ZeroLC V) by Th43 .= 0. V by Lm1 ; hence Sum (- L) = - (Sum L) by VECTSP_1:16; ::_thesis: verum end; theorem :: VECTSP_6:47 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) proof let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2) let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 - L2) = (Sum L1) - (Sum L2) thus Sum (L1 - L2) = (Sum L1) + (Sum (- L2)) by Th44 .= (Sum L1) + (- (Sum L2)) by Th46 .= (Sum L1) - (Sum L2) by RLVECT_1:def_11 ; ::_thesis: verum end; theorem :: VECTSP_6:48 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr for a being Element of GF holds (- (1. GF)) * a = - a by Lm2; theorem :: VECTSP_6:49 for GF being Field holds - (1. GF) <> 0. GF by Lm3;