:: FVSUM_1 semantic presentation begin theorem Th1: :: FVSUM_1:1 for K being non empty Abelian addLoopStr holds the addF of K is commutative proof let K be non empty Abelian addLoopStr ; ::_thesis: the addF of K is commutative now__::_thesis:_for_a,_b_being_Element_of_K_holds_the_addF_of_K_._(a,b)_=_the_addF_of_K_._(b,a) let a, b be Element of K; ::_thesis: the addF of K . (a,b) = the addF of K . (b,a) thus the addF of K . (a,b) = a + b .= the addF of K . (b,a) by RLVECT_1:2 ; ::_thesis: verum end; hence the addF of K is commutative by BINOP_1:def_2; ::_thesis: verum end; theorem Th2: :: FVSUM_1:2 for K being non empty add-associative addLoopStr holds the addF of K is associative proof let K be non empty add-associative addLoopStr ; ::_thesis: the addF of K is associative now__::_thesis:_for_a,_b,_c_being_Element_of_K_holds_the_addF_of_K_._(a,(_the_addF_of_K_._(b,c)))_=_the_addF_of_K_._((_the_addF_of_K_._(a,b)),c) let a, b, c be Element of K; ::_thesis: the addF of K . (a,( the addF of K . (b,c))) = the addF of K . (( the addF of K . (a,b)),c) thus the addF of K . (a,( the addF of K . (b,c))) = a + (b + c) .= (a + b) + c by RLVECT_1:def_3 .= the addF of K . (( the addF of K . (a,b)),c) ; ::_thesis: verum end; hence the addF of K is associative by BINOP_1:def_3; ::_thesis: verum end; theorem Th3: :: FVSUM_1:3 for K being non empty commutative multMagma holds the multF of K is commutative proof let K be non empty commutative multMagma ; ::_thesis: the multF of K is commutative now__::_thesis:_for_a,_b_being_Element_of_K_holds_the_multF_of_K_._(a,b)_=_the_multF_of_K_._(b,a) let a, b be Element of K; ::_thesis: the multF of K . (a,b) = the multF of K . (b,a) thus the multF of K . (a,b) = a * b .= b * a .= the multF of K . (b,a) ; ::_thesis: verum end; hence the multF of K is commutative by BINOP_1:def_2; ::_thesis: verum end; registration let K be non empty Abelian addLoopStr ; cluster the addF of K -> commutative ; coherence the addF of K is commutative by Th1; end; registration let K be non empty add-associative addLoopStr ; cluster the addF of K -> associative ; coherence the addF of K is associative by Th2; end; registration let K be non empty commutative multMagma ; cluster the multF of K -> commutative ; coherence the multF of K is commutative by Th3; end; theorem Th4: :: FVSUM_1:4 for K being non empty commutative left_unital multLoopStr holds 1. K is_a_unity_wrt the multF of K proof let K be non empty commutative left_unital multLoopStr ; ::_thesis: 1. K is_a_unity_wrt the multF of K set o = the multF of K; now__::_thesis:_for_h_being_Element_of_K_holds_ (_the_multF_of_K_._((1._K),h)_=_h_&_the_multF_of_K_._(h,(1._K))_=_h_) let h be Element of K; ::_thesis: ( the multF of K . ((1. K),h) = h & the multF of K . (h,(1. K)) = h ) thus the multF of K . ((1. K),h) = (1. K) * h .= h by VECTSP_1:def_8 ; ::_thesis: the multF of K . (h,(1. K)) = h thus the multF of K . (h,(1. K)) = h * (1. K) .= h by VECTSP_1:def_8 ; ::_thesis: verum end; hence 1. K is_a_unity_wrt the multF of K by BINOP_1:3; ::_thesis: verum end; theorem Th5: :: FVSUM_1:5 for K being non empty commutative left_unital multLoopStr holds the_unity_wrt the multF of K = 1. K proof let K be non empty commutative left_unital multLoopStr ; ::_thesis: the_unity_wrt the multF of K = 1. K reconsider e = 1. K as Element of K ; e is_a_unity_wrt the multF of K by Th4; hence the_unity_wrt the multF of K = 1. K by BINOP_1:def_8; ::_thesis: verum end; theorem Th6: :: FVSUM_1:6 for K being non empty left_zeroed right_zeroed addLoopStr holds 0. K is_a_unity_wrt the addF of K proof let K be non empty left_zeroed right_zeroed addLoopStr ; ::_thesis: 0. K is_a_unity_wrt the addF of K now__::_thesis:_for_a_being_Element_of_K_holds_ (_the_addF_of_K_._((0._K),a)_=_a_&_the_addF_of_K_._(a,(0._K))_=_a_) let a be Element of K; ::_thesis: ( the addF of K . ((0. K),a) = a & the addF of K . (a,(0. K)) = a ) thus the addF of K . ((0. K),a) = (0. K) + a .= a by ALGSTR_1:def_2 ; ::_thesis: the addF of K . (a,(0. K)) = a thus the addF of K . (a,(0. K)) = a + (0. K) .= a by RLVECT_1:def_4 ; ::_thesis: verum end; hence 0. K is_a_unity_wrt the addF of K by BINOP_1:3; ::_thesis: verum end; theorem Th7: :: FVSUM_1:7 for K being non empty left_zeroed right_zeroed addLoopStr holds the_unity_wrt the addF of K = 0. K proof let K be non empty left_zeroed right_zeroed addLoopStr ; ::_thesis: the_unity_wrt the addF of K = 0. K reconsider e = 0. K as Element of K ; e is_a_unity_wrt the addF of K by Th6; hence the_unity_wrt the addF of K = 0. K by BINOP_1:def_8; ::_thesis: verum end; theorem Th8: :: FVSUM_1:8 for K being non empty left_zeroed right_zeroed addLoopStr holds the addF of K is having_a_unity proof let K be non empty left_zeroed right_zeroed addLoopStr ; ::_thesis: the addF of K is having_a_unity take 0. K ; :: according to SETWISEO:def_2 ::_thesis: 0. K is_a_unity_wrt the addF of K thus 0. K is_a_unity_wrt the addF of K by Th6; ::_thesis: verum end; theorem :: FVSUM_1:9 for K being non empty commutative left_unital multLoopStr holds the multF of K is having_a_unity ; theorem Th10: :: FVSUM_1:10 for K being non empty distributive doubleLoopStr holds the multF of K is_distributive_wrt the addF of K proof let K be non empty distributive doubleLoopStr ; ::_thesis: the multF of K is_distributive_wrt the addF of K now__::_thesis:_for_a1,_a2,_a3_being_Element_of_K_holds_ (_the_multF_of_K_._(a1,(_the_addF_of_K_._(a2,a3)))_=_the_addF_of_K_._((_the_multF_of_K_._(a1,a2)),(_the_multF_of_K_._(a1,a3)))_&_the_multF_of_K_._((_the_addF_of_K_._(a1,a2)),a3)_=_the_addF_of_K_._((_the_multF_of_K_._(a1,a3)),(_the_multF_of_K_._(a2,a3)))_) let a1, a2, a3 be Element of K; ::_thesis: ( the multF of K . (a1,( the addF of K . (a2,a3))) = the addF of K . (( the multF of K . (a1,a2)),( the multF of K . (a1,a3))) & the multF of K . (( the addF of K . (a1,a2)),a3) = the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3))) ) thus the multF of K . (a1,( the addF of K . (a2,a3))) = a1 * (a2 + a3) .= (a1 * a2) + (a1 * a3) by VECTSP_1:def_7 .= the addF of K . (( the multF of K . (a1,a2)),( the multF of K . (a1,a3))) ; ::_thesis: the multF of K . (( the addF of K . (a1,a2)),a3) = the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3))) thus the multF of K . (( the addF of K . (a1,a2)),a3) = (a1 + a2) * a3 .= (a1 * a3) + (a2 * a3) by VECTSP_1:def_7 .= the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3))) ; ::_thesis: verum end; hence the multF of K is_distributive_wrt the addF of K by BINOP_1:11; ::_thesis: verum end; definition let K be non empty multMagma ; let a be Element of K; funca multfield -> UnOp of the carrier of K equals :: FVSUM_1:def 1 the multF of K [;] (a,(id the carrier of K)); coherence the multF of K [;] (a,(id the carrier of K)) is UnOp of the carrier of K ; end; :: deftheorem defines multfield FVSUM_1:def_1_:_ for K being non empty multMagma for a being Element of K holds a multfield = the multF of K [;] (a,(id the carrier of K)); definition let K be non empty addLoopStr ; func diffield K -> BinOp of the carrier of K equals :: FVSUM_1:def 2 the addF of K * ((id the carrier of K),(comp K)); correctness coherence the addF of K * ((id the carrier of K),(comp K)) is BinOp of the carrier of K; ; end; :: deftheorem defines diffield FVSUM_1:def_2_:_ for K being non empty addLoopStr holds diffield K = the addF of K * ((id the carrier of K),(comp K)); theorem Th11: :: FVSUM_1:11 for K being non empty addLoopStr for a1, a2 being Element of K holds (diffield K) . (a1,a2) = a1 - a2 proof let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K holds (diffield K) . (a1,a2) = a1 - a2 let a1, a2 be Element of K; ::_thesis: (diffield K) . (a1,a2) = a1 - a2 thus (diffield K) . (a1,a2) = the addF of K . (a1,((comp K) . a2)) by FINSEQOP:82 .= a1 - a2 by VECTSP_1:def_13 ; ::_thesis: verum end; Lm1: for K being non empty multMagma for a, b being Element of K holds ( the multF of K [;] (b,(id the carrier of K))) . a = b * a proof let K be non empty multMagma ; ::_thesis: for a, b being Element of K holds ( the multF of K [;] (b,(id the carrier of K))) . a = b * a let a, b be Element of K; ::_thesis: ( the multF of K [;] (b,(id the carrier of K))) . a = b * a thus ( the multF of K [;] (b,(id the carrier of K))) . a = the multF of K . (b,((id the carrier of K) . a)) by FUNCOP_1:53 .= b * a by FUNCT_1:18 ; ::_thesis: verum end; theorem Th12: :: FVSUM_1:12 for K being non empty distributive doubleLoopStr for a being Element of K holds a multfield is_distributive_wrt the addF of K by Th10, FINSEQOP:54; theorem Th13: :: FVSUM_1:13 for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds comp K is_an_inverseOp_wrt the addF of K proof let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: comp K is_an_inverseOp_wrt the addF of K now__::_thesis:_for_a_being_Element_of_K_holds_ (_the_addF_of_K_._(a,((comp_K)_._a))_=_the_unity_wrt_the_addF_of_K_&_the_addF_of_K_._(((comp_K)_._a),a)_=_the_unity_wrt_the_addF_of_K_) let a be Element of K; ::_thesis: ( the addF of K . (a,((comp K) . a)) = the_unity_wrt the addF of K & the addF of K . (((comp K) . a),a) = the_unity_wrt the addF of K ) thus the addF of K . (a,((comp K) . a)) = a + (- a) by VECTSP_1:def_13 .= 0. K by RLVECT_1:5 .= the_unity_wrt the addF of K by Th7 ; ::_thesis: the addF of K . (((comp K) . a),a) = the_unity_wrt the addF of K thus the addF of K . (((comp K) . a),a) = (- a) + a by VECTSP_1:def_13 .= 0. K by RLVECT_1:5 .= the_unity_wrt the addF of K by Th7 ; ::_thesis: verum end; hence comp K is_an_inverseOp_wrt the addF of K by FINSEQOP:def_1; ::_thesis: verum end; theorem Th14: :: FVSUM_1:14 for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds the addF of K is having_an_inverseOp proof let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: the addF of K is having_an_inverseOp comp K is_an_inverseOp_wrt the addF of K by Th13; hence the addF of K is having_an_inverseOp by FINSEQOP:def_2; ::_thesis: verum end; theorem Th15: :: FVSUM_1:15 for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds the_inverseOp_wrt the addF of K = comp K proof let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: the_inverseOp_wrt the addF of K = comp K A1: comp K is_an_inverseOp_wrt the addF of K by Th13; ( the addF of K is having_a_unity & the addF of K is having_an_inverseOp ) by Th8, Th14; hence the_inverseOp_wrt the addF of K = comp K by A1, FINSEQOP:def_3; ::_thesis: verum end; theorem :: FVSUM_1:16 for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds comp K is_distributive_wrt the addF of K proof let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: comp K is_distributive_wrt the addF of K the addF of K is having_a_unity by Th8; then the_inverseOp_wrt the addF of K is_distributive_wrt the addF of K by Th14, FINSEQOP:63; hence comp K is_distributive_wrt the addF of K by Th15; ::_thesis: verum end; begin definition let K be non empty addLoopStr ; let p1, p2 be FinSequence of the carrier of K; funcp1 + p2 -> FinSequence of the carrier of K equals :: FVSUM_1:def 3 the addF of K .: (p1,p2); correctness coherence the addF of K .: (p1,p2) is FinSequence of the carrier of K; ; end; :: deftheorem defines + FVSUM_1:def_3_:_ for K being non empty addLoopStr for p1, p2 being FinSequence of the carrier of K holds p1 + p2 = the addF of K .: (p1,p2); theorem :: FVSUM_1:17 for K being non empty addLoopStr for p1, p2 being FinSequence of the carrier of K for a1, a2 being Element of K for i being Element of NAT st i in dom (p1 + p2) & a1 = p1 . i & a2 = p2 . i holds (p1 + p2) . i = a1 + a2 by FUNCOP_1:22; definition let i be Element of NAT ; let K be non empty addLoopStr ; let R1, R2 be Element of i -tuples_on the carrier of K; :: original: + redefine funcR1 + R2 -> Element of i -tuples_on the carrier of K; coherence R1 + R2 is Element of i -tuples_on the carrier of K by FINSEQ_2:120; end; theorem :: FVSUM_1:18 for i, j being Element of NAT for K being non empty addLoopStr for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (R1 + R2) . j = a1 + a2 proof let i, j be Element of NAT ; ::_thesis: for K being non empty addLoopStr for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (R1 + R2) . j = a1 + a2 let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (R1 + R2) . j = a1 + a2 let a1, a2 be Element of K; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (R1 + R2) . j = a1 + a2 let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a1 = R1 . j & a2 = R2 . j implies (R1 + R2) . j = a1 + a2 ) assume j in Seg i ; ::_thesis: ( not a1 = R1 . j or not a2 = R2 . j or (R1 + R2) . j = a1 + a2 ) then j in Seg (len (R1 + R2)) by CARD_1:def_7; then j in dom (R1 + R2) by FINSEQ_1:def_3; hence ( not a1 = R1 . j or not a2 = R2 . j or (R1 + R2) . j = a1 + a2 ) by FUNCOP_1:22; ::_thesis: verum end; theorem :: FVSUM_1:19 for K being non empty addLoopStr for a1, a2 being Element of K holds <*a1*> + <*a2*> = <*(a1 + a2)*> by FINSEQ_2:74; theorem :: FVSUM_1:20 for i being Element of NAT for K being non empty addLoopStr for a1, a2 being Element of K holds (i |-> a1) + (i |-> a2) = i |-> (a1 + a2) by FINSEQOP:17; Lm2: for i being Element of NAT for K being non empty left_zeroed right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R proof let i be Element of NAT ; ::_thesis: for K being non empty left_zeroed right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R let K be non empty left_zeroed right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R let R be Element of i -tuples_on the carrier of K; ::_thesis: R + (i |-> (0. K)) = R ( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8; hence R + (i |-> (0. K)) = R by FINSEQOP:56; ::_thesis: verum end; theorem Th21: :: FVSUM_1:21 for i being Element of NAT for K being non empty left_zeroed Abelian right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds ( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R ) proof let i be Element of NAT ; ::_thesis: for K being non empty left_zeroed Abelian right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds ( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R ) let K be non empty left_zeroed Abelian right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds ( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R ) let R be Element of i -tuples_on the carrier of K; ::_thesis: ( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R ) thus R + (i |-> (0. K)) = R by Lm2; ::_thesis: R = (i |-> (0. K)) + R hence R = (i |-> (0. K)) + R by FINSEQOP:33; ::_thesis: verum end; definition let K be non empty addLoopStr ; let p be FinSequence of the carrier of K; func - p -> FinSequence of the carrier of K equals :: FVSUM_1:def 4 (comp K) * p; correctness coherence (comp K) * p is FinSequence of the carrier of K; ; end; :: deftheorem defines - FVSUM_1:def_4_:_ for K being non empty addLoopStr for p being FinSequence of the carrier of K holds - p = (comp K) * p; theorem Th22: :: FVSUM_1:22 for i being Element of NAT for K being non empty addLoopStr for a being Element of K for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds (- p) . i = - a proof let i be Element of NAT ; ::_thesis: for K being non empty addLoopStr for a being Element of K for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds (- p) . i = - a let K be non empty addLoopStr ; ::_thesis: for a being Element of K for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds (- p) . i = - a let a be Element of K; ::_thesis: for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds (- p) . i = - a let p be FinSequence of the carrier of K; ::_thesis: ( i in dom (- p) & a = p . i implies (- p) . i = - a ) assume ( i in dom (- p) & a = p . i ) ; ::_thesis: (- p) . i = - a then (- p) . i = (comp K) . a by FUNCT_1:12; hence (- p) . i = - a by VECTSP_1:def_13; ::_thesis: verum end; definition let i be Element of NAT ; let K be non empty addLoopStr ; let R be Element of i -tuples_on the carrier of K; :: original: - redefine func - R -> Element of i -tuples_on the carrier of K; coherence - R is Element of i -tuples_on the carrier of K by FINSEQ_2:113; end; theorem :: FVSUM_1:23 for j, i being Element of NAT for K being non empty addLoopStr for a being Element of K for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds (- R) . j = - a proof let j, i be Element of NAT ; ::_thesis: for K being non empty addLoopStr for a being Element of K for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds (- R) . j = - a let K be non empty addLoopStr ; ::_thesis: for a being Element of K for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds (- R) . j = - a let a be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds (- R) . j = - a let R be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a = R . j implies (- R) . j = - a ) assume j in Seg i ; ::_thesis: ( not a = R . j or (- R) . j = - a ) then j in Seg (len (- R)) by CARD_1:def_7; then j in dom (- R) by FINSEQ_1:def_3; hence ( not a = R . j or (- R) . j = - a ) by Th22; ::_thesis: verum end; theorem :: FVSUM_1:24 for K being non empty addLoopStr for a being Element of K holds - <*a*> = <*(- a)*> proof let K be non empty addLoopStr ; ::_thesis: for a being Element of K holds - <*a*> = <*(- a)*> let a be Element of K; ::_thesis: - <*a*> = <*(- a)*> thus - <*a*> = <*((comp K) . a)*> by FINSEQ_2:35 .= <*(- a)*> by VECTSP_1:def_13 ; ::_thesis: verum end; theorem Th25: :: FVSUM_1:25 for i being Element of NAT for K being non empty addLoopStr for a being Element of K holds - (i |-> a) = i |-> (- a) proof let i be Element of NAT ; ::_thesis: for K being non empty addLoopStr for a being Element of K holds - (i |-> a) = i |-> (- a) let K be non empty addLoopStr ; ::_thesis: for a being Element of K holds - (i |-> a) = i |-> (- a) let a be Element of K; ::_thesis: - (i |-> a) = i |-> (- a) thus - (i |-> a) = i |-> ((comp K) . a) by FINSEQOP:16 .= i |-> (- a) by VECTSP_1:def_13 ; ::_thesis: verum end; Lm3: for i being Element of NAT for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K) proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K) let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K) let R be Element of i -tuples_on the carrier of K; ::_thesis: R + (- R) = i |-> (0. K) A1: ( the addF of K is having_an_inverseOp & the addF of K is having_a_unity ) by Th8, Th14; thus R + (- R) = the addF of K .: (R,((the_inverseOp_wrt the addF of K) * R)) by Th15 .= i |-> (the_unity_wrt the addF of K) by A1, FINSEQOP:73 .= i |-> (0. K) by Th7 ; ::_thesis: verum end; theorem Th26: :: FVSUM_1:26 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds ( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) ) proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds ( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) ) let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds ( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) ) let R be Element of i -tuples_on the carrier of K; ::_thesis: ( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) ) thus R + (- R) = i |-> (0. K) by Lm3; ::_thesis: (- R) + R = i |-> (0. K) hence (- R) + R = i |-> (0. K) by FINSEQOP:33; ::_thesis: verum end; theorem Th27: :: FVSUM_1:27 for i being Element of NAT for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds ( R1 = - R2 & R2 = - R1 ) proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds ( R1 = - R2 & R2 = - R1 ) let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds ( R1 = - R2 & R2 = - R1 ) let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( R1 + R2 = i |-> (0. K) implies ( R1 = - R2 & R2 = - R1 ) ) A1: ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15; ( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8; hence ( R1 + R2 = i |-> (0. K) implies ( R1 = - R2 & R2 = - R1 ) ) by A1, FINSEQOP:74; ::_thesis: verum end; theorem Th28: :: FVSUM_1:28 for i being Element of NAT for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds - (- R) = R proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds - (- R) = R let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds - (- R) = R let R be Element of i -tuples_on the carrier of K; ::_thesis: - (- R) = R R + (- R) = i |-> (0. K) by Lm3; hence - (- R) = R by Th27; ::_thesis: verum end; theorem :: FVSUM_1:29 for i being Element of NAT for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds R1 = R2 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds R1 = R2 let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds R1 = R2 let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( - R1 = - R2 implies R1 = R2 ) assume - R1 = - R2 ; ::_thesis: R1 = R2 hence R1 = - (- R2) by Th28 .= R2 by Th28 ; ::_thesis: verum end; Lm4: for i being Element of NAT for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds R1 = R2 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds R1 = R2 let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds R1 = R2 let R1, R, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( R1 + R = R2 + R implies R1 = R2 ) assume R1 + R = R2 + R ; ::_thesis: R1 = R2 then R1 + (R + (- R)) = (R2 + R) + (- R) by FINSEQOP:28; then A1: R1 + (R + (- R)) = R2 + (R + (- R)) by FINSEQOP:28; R + (- R) = i |-> (0. K) by Lm3; then R1 = R2 + (i |-> (0. K)) by A1, Lm2; hence R1 = R2 by Lm2; ::_thesis: verum end; theorem :: FVSUM_1:30 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds R1 = R2 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds R1 = R2 let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds R1 = R2 let R, R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( ( R1 + R = R2 + R or R1 + R = R + R2 ) implies R1 = R2 ) ( R1 + R = R2 + R iff R1 + R = R + R2 ) by FINSEQOP:33; hence ( ( R1 + R = R2 + R or R1 + R = R + R2 ) implies R1 = R2 ) by Lm4; ::_thesis: verum end; theorem Th31: :: FVSUM_1:31 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2) proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2) let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2) let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: - (R1 + R2) = (- R1) + (- R2) (R1 + R2) + ((- R1) + (- R2)) = ((R1 + R2) + (- R1)) + (- R2) by FINSEQOP:28 .= ((R2 + R1) + (- R1)) + (- R2) by FINSEQOP:33 .= (R2 + (R1 + (- R1))) + (- R2) by FINSEQOP:28 .= (R2 + (i |-> (0. K))) + (- R2) by Lm3 .= R2 + (- R2) by Lm2 .= i |-> (0. K) by Lm3 ; hence - (R1 + R2) = (- R1) + (- R2) by Th27; ::_thesis: verum end; definition let K be non empty addLoopStr ; let p1, p2 be FinSequence of the carrier of K; funcp1 - p2 -> FinSequence of the carrier of K equals :: FVSUM_1:def 5 (diffield K) .: (p1,p2); correctness coherence (diffield K) .: (p1,p2) is FinSequence of the carrier of K; ; end; :: deftheorem defines - FVSUM_1:def_5_:_ for K being non empty addLoopStr for p1, p2 being FinSequence of the carrier of K holds p1 - p2 = (diffield K) .: (p1,p2); theorem Th32: :: FVSUM_1:32 for i being Element of NAT for K being non empty addLoopStr for a1, a2 being Element of K for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds (p1 - p2) . i = a1 - a2 proof let i be Element of NAT ; ::_thesis: for K being non empty addLoopStr for a1, a2 being Element of K for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds (p1 - p2) . i = a1 - a2 let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds (p1 - p2) . i = a1 - a2 let a1, a2 be Element of K; ::_thesis: for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds (p1 - p2) . i = a1 - a2 let p1, p2 be FinSequence of the carrier of K; ::_thesis: ( i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i implies (p1 - p2) . i = a1 - a2 ) assume ( i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i ) ; ::_thesis: (p1 - p2) . i = a1 - a2 then (p1 - p2) . i = (diffield K) . (a1,a2) by FUNCOP_1:22; hence (p1 - p2) . i = a1 - a2 by Th11; ::_thesis: verum end; definition let i be Element of NAT ; let K be non empty addLoopStr ; let R1, R2 be Element of i -tuples_on the carrier of K; :: original: - redefine funcR1 - R2 -> Element of i -tuples_on the carrier of K; coherence R1 - R2 is Element of i -tuples_on the carrier of K by FINSEQ_2:120; end; theorem :: FVSUM_1:33 for j, i being Element of NAT for K being non empty addLoopStr for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (R1 - R2) . j = a1 - a2 proof let j, i be Element of NAT ; ::_thesis: for K being non empty addLoopStr for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (R1 - R2) . j = a1 - a2 let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (R1 - R2) . j = a1 - a2 let a1, a2 be Element of K; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (R1 - R2) . j = a1 - a2 let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a1 = R1 . j & a2 = R2 . j implies (R1 - R2) . j = a1 - a2 ) assume j in Seg i ; ::_thesis: ( not a1 = R1 . j or not a2 = R2 . j or (R1 - R2) . j = a1 - a2 ) then j in Seg (len (R1 - R2)) by CARD_1:def_7; then j in dom (R1 - R2) by FINSEQ_1:def_3; hence ( not a1 = R1 . j or not a2 = R2 . j or (R1 - R2) . j = a1 - a2 ) by Th32; ::_thesis: verum end; theorem :: FVSUM_1:34 for K being non empty addLoopStr for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*> proof let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*> let a1, a2 be Element of K; ::_thesis: <*a1*> - <*a2*> = <*(a1 - a2)*> thus <*a1*> - <*a2*> = <*((diffield K) . (a1,a2))*> by FINSEQ_2:74 .= <*(a1 - a2)*> by Th11 ; ::_thesis: verum end; theorem :: FVSUM_1:35 for i being Element of NAT for K being non empty addLoopStr for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2) proof let i be Element of NAT ; ::_thesis: for K being non empty addLoopStr for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2) let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2) let a1, a2 be Element of K; ::_thesis: (i |-> a1) - (i |-> a2) = i |-> (a1 - a2) thus (i |-> a1) - (i |-> a2) = i |-> ((diffield K) . (a1,a2)) by FINSEQOP:17 .= i |-> (a1 - a2) by Th11 ; ::_thesis: verum end; theorem :: FVSUM_1:36 for i being Element of NAT for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R let R be Element of i -tuples_on the carrier of K; ::_thesis: R - (i |-> (0. K)) = R thus R - (i |-> (0. K)) = R + (- (i |-> (0. K))) by FINSEQOP:84 .= R + (i |-> (- (0. K))) by Th25 .= R + (i |-> (0. K)) by RLVECT_1:12 .= R by Lm2 ; ::_thesis: verum end; theorem :: FVSUM_1:37 for i being Element of NAT for K being non empty left_zeroed Abelian right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R proof let i be Element of NAT ; ::_thesis: for K being non empty left_zeroed Abelian right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R let K be non empty left_zeroed Abelian right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R let R be Element of i -tuples_on the carrier of K; ::_thesis: (i |-> (0. K)) - R = - R thus (i |-> (0. K)) - R = (i |-> (0. K)) + (- R) by FINSEQOP:84 .= - R by Th21 ; ::_thesis: verum end; theorem :: FVSUM_1:38 for i being Element of NAT for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2 let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2 let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: R1 - (- R2) = R1 + R2 thus R1 - (- R2) = R1 + (- (- R2)) by FINSEQOP:84 .= R1 + R2 by Th28 ; ::_thesis: verum end; theorem :: FVSUM_1:39 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1 let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1 let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: - (R1 - R2) = R2 - R1 thus - (R1 - R2) = - (R1 + (- R2)) by FINSEQOP:84 .= (- R1) + (- (- R2)) by Th31 .= (- R1) + R2 by Th28 .= R2 + (- R1) by FINSEQOP:33 .= R2 - R1 by FINSEQOP:84 ; ::_thesis: verum end; theorem Th40: :: FVSUM_1:40 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2 let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2 let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: - (R1 - R2) = (- R1) + R2 thus - (R1 - R2) = - (R1 + (- R2)) by FINSEQOP:84 .= (- R1) + (- (- R2)) by Th31 .= (- R1) + R2 by Th28 ; ::_thesis: verum end; theorem Th41: :: FVSUM_1:41 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K) proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K) let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K) let R be Element of i -tuples_on the carrier of K; ::_thesis: R - R = i |-> (0. K) thus R - R = R + (- R) by FINSEQOP:84 .= i |-> (0. K) by Lm3 ; ::_thesis: verum end; theorem :: FVSUM_1:42 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K st R1 - R2 = i |-> (0. K) holds R1 = R2 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K st R1 - R2 = i |-> (0. K) holds R1 = R2 let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st R1 - R2 = i |-> (0. K) holds R1 = R2 let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( R1 - R2 = i |-> (0. K) implies R1 = R2 ) assume R1 - R2 = i |-> (0. K) ; ::_thesis: R1 = R2 then R1 + (- R2) = i |-> (0. K) by FINSEQOP:84; then R1 = - (- R2) by Th27; hence R1 = R2 by Th28; ::_thesis: verum end; theorem :: FVSUM_1:43 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3) proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3) let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3) let R1, R2, R3 be Element of i -tuples_on the carrier of K; ::_thesis: (R1 - R2) - R3 = R1 - (R2 + R3) thus (R1 - R2) - R3 = (R1 - R2) + (- R3) by FINSEQOP:84 .= (R1 + (- R2)) + (- R3) by FINSEQOP:84 .= R1 + ((- R2) + (- R3)) by FINSEQOP:28 .= R1 + (- (R2 + R3)) by Th31 .= R1 - (R2 + R3) by FINSEQOP:84 ; ::_thesis: verum end; theorem Th44: :: FVSUM_1:44 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 - R3) = (R1 + R2) - R3 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 - R3) = (R1 + R2) - R3 let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 - R3) = (R1 + R2) - R3 let R1, R2, R3 be Element of i -tuples_on the carrier of K; ::_thesis: R1 + (R2 - R3) = (R1 + R2) - R3 thus R1 + (R2 - R3) = R1 + (R2 + (- R3)) by FINSEQOP:84 .= (R1 + R2) + (- R3) by FINSEQOP:28 .= (R1 + R2) - R3 by FINSEQOP:84 ; ::_thesis: verum end; theorem :: FVSUM_1:45 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 - (R2 - R3) = (R1 - R2) + R3 proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 - (R2 - R3) = (R1 - R2) + R3 let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 - (R2 - R3) = (R1 - R2) + R3 let R1, R2, R3 be Element of i -tuples_on the carrier of K; ::_thesis: R1 - (R2 - R3) = (R1 - R2) + R3 thus R1 - (R2 - R3) = R1 + (- (R2 - R3)) by FINSEQOP:84 .= R1 + ((- R2) + R3) by Th40 .= (R1 + (- R2)) + R3 by FINSEQOP:28 .= (R1 - R2) + R3 by FINSEQOP:84 ; ::_thesis: verum end; theorem :: FVSUM_1:46 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R let R1, R be Element of i -tuples_on the carrier of K; ::_thesis: R1 = (R1 + R) - R thus R1 = R1 + (i |-> (0. K)) by Lm2 .= R1 + (R - R) by Th41 .= (R1 + R) - R by Th44 ; ::_thesis: verum end; theorem :: FVSUM_1:47 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R let R1, R be Element of i -tuples_on the carrier of K; ::_thesis: R1 = (R1 - R) + R thus R1 = R1 + (i |-> (0. K)) by Lm2 .= R1 + ((- R) + R) by Th26 .= (R1 + (- R)) + R by FINSEQOP:28 .= (R1 - R) + R by FINSEQOP:84 ; ::_thesis: verum end; theorem Th48: :: FVSUM_1:48 for K being non empty multMagma for a, b being Element of K holds ( the multF of K [;] (a,(id the carrier of K))) . b = a * b proof let K be non empty multMagma ; ::_thesis: for a, b being Element of K holds ( the multF of K [;] (a,(id the carrier of K))) . b = a * b let a, b be Element of K; ::_thesis: ( the multF of K [;] (a,(id the carrier of K))) . b = a * b thus ( the multF of K [;] (a,(id the carrier of K))) . b = the multF of K . (a,((id the carrier of K) . b)) by FUNCOP_1:53 .= a * b by FUNCT_1:18 ; ::_thesis: verum end; theorem :: FVSUM_1:49 for K being non empty multMagma for a, b being Element of K holds (a multfield) . b = a * b by Th48; definition let K be non empty multMagma ; let p be FinSequence of the carrier of K; let a be Element of K; funca * p -> FinSequence of the carrier of K equals :: FVSUM_1:def 6 (a multfield) * p; correctness coherence (a multfield) * p is FinSequence of the carrier of K; ; end; :: deftheorem defines * FVSUM_1:def_6_:_ for K being non empty multMagma for p being FinSequence of the carrier of K for a being Element of K holds a * p = (a multfield) * p; theorem Th50: :: FVSUM_1:50 for i being Element of NAT for K being non empty multMagma for a, a9 being Element of K for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds (a * p) . i = a * a9 proof let i be Element of NAT ; ::_thesis: for K being non empty multMagma for a, a9 being Element of K for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds (a * p) . i = a * a9 let K be non empty multMagma ; ::_thesis: for a, a9 being Element of K for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds (a * p) . i = a * a9 let a, a9 be Element of K; ::_thesis: for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds (a * p) . i = a * a9 let p be FinSequence of the carrier of K; ::_thesis: ( i in dom (a * p) & a9 = p . i implies (a * p) . i = a * a9 ) assume A1: ( i in dom (a * p) & a9 = p . i ) ; ::_thesis: (a * p) . i = a * a9 then A2: a9 in dom ( the multF of K [;] (a,(id the carrier of K))) by FUNCT_1:11; thus (a * p) . i = ( the multF of K [;] (a,(id the carrier of K))) . a9 by A1, FUNCT_1:12 .= the multF of K . (a,((id the carrier of K) . a9)) by A2, FUNCOP_1:32 .= a * a9 by FUNCT_1:18 ; ::_thesis: verum end; definition let i be Element of NAT ; let K be non empty multMagma ; let R be Element of i -tuples_on the carrier of K; let a be Element of K; :: original: * redefine funca * R -> Element of i -tuples_on the carrier of K; coherence a * R is Element of i -tuples_on the carrier of K by FINSEQ_2:113; end; theorem :: FVSUM_1:51 for j, i being Element of NAT for K being non empty multMagma for a9, a being Element of K for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds (a * R) . j = a * a9 proof let j, i be Element of NAT ; ::_thesis: for K being non empty multMagma for a9, a being Element of K for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds (a * R) . j = a * a9 let K be non empty multMagma ; ::_thesis: for a9, a being Element of K for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds (a * R) . j = a * a9 let a9, a be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds (a * R) . j = a * a9 let R be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a9 = R . j implies (a * R) . j = a * a9 ) assume j in Seg i ; ::_thesis: ( not a9 = R . j or (a * R) . j = a * a9 ) then j in Seg (len (a * R)) by CARD_1:def_7; then j in dom (a * R) by FINSEQ_1:def_3; hence ( not a9 = R . j or (a * R) . j = a * a9 ) by Th50; ::_thesis: verum end; theorem :: FVSUM_1:52 for K being non empty multMagma for a, a1 being Element of K holds a * <*a1*> = <*(a * a1)*> proof let K be non empty multMagma ; ::_thesis: for a, a1 being Element of K holds a * <*a1*> = <*(a * a1)*> let a, a1 be Element of K; ::_thesis: a * <*a1*> = <*(a * a1)*> thus a * <*a1*> = <*(( the multF of K [;] (a,(id the carrier of K))) . a1)*> by FINSEQ_2:35 .= <*(a * a1)*> by Th48 ; ::_thesis: verum end; theorem Th53: :: FVSUM_1:53 for i being Element of NAT for K being non empty multMagma for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2) proof let i be Element of NAT ; ::_thesis: for K being non empty multMagma for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2) let K be non empty multMagma ; ::_thesis: for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2) let a1, a2 be Element of K; ::_thesis: a1 * (i |-> a2) = i |-> (a1 * a2) thus a1 * (i |-> a2) = i |-> (( the multF of K [;] (a1,(id the carrier of K))) . a2) by FINSEQOP:16 .= i |-> (a1 * a2) by Th48 ; ::_thesis: verum end; theorem :: FVSUM_1:54 for i being Element of NAT for K being non empty associative multMagma for a1, a2 being Element of K for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R) proof let i be Element of NAT ; ::_thesis: for K being non empty associative multMagma for a1, a2 being Element of K for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R) let K be non empty associative multMagma ; ::_thesis: for a1, a2 being Element of K for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R) let a1, a2 be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R) let R be Element of i -tuples_on the carrier of K; ::_thesis: (a1 * a2) * R = a1 * (a2 * R) set F = the multF of K; set f = id the carrier of K; thus (a1 * a2) * R = ( the multF of K [;] (a1,( the multF of K [;] (a2,(id the carrier of K))))) * R by FUNCOP_1:62 .= (( the multF of K [;] (a1,(id the carrier of K))) * ( the multF of K [;] (a2,(id the carrier of K)))) * R by FUNCOP_1:55 .= a1 * (a2 * R) by RELAT_1:36 ; ::_thesis: verum end; theorem :: FVSUM_1:55 for i being Element of NAT for K being non empty distributive doubleLoopStr for a1, a2 being Element of K for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R) proof let i be Element of NAT ; ::_thesis: for K being non empty distributive doubleLoopStr for a1, a2 being Element of K for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R) let K be non empty distributive doubleLoopStr ; ::_thesis: for a1, a2 being Element of K for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R) let a1, a2 be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R) let R be Element of i -tuples_on the carrier of K; ::_thesis: (a1 + a2) * R = (a1 * R) + (a2 * R) thus (a1 + a2) * R = ( the addF of K .: (( the multF of K [;] (a1,(id the carrier of K))),( the multF of K [;] (a2,(id the carrier of K))))) * R by Th10, FINSEQOP:35 .= (a1 * R) + (a2 * R) by FUNCOP_1:25 ; ::_thesis: verum end; theorem :: FVSUM_1:56 for i being Element of NAT for K being non empty distributive doubleLoopStr for a being Element of K for R1, R2 being Element of i -tuples_on the carrier of K holds a * (R1 + R2) = (a * R1) + (a * R2) by Th12, FINSEQOP:51; theorem :: FVSUM_1:57 for i being Element of NAT for K being non empty commutative distributive left_unital doubleLoopStr for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R proof let i be Element of NAT ; ::_thesis: for K being non empty commutative distributive left_unital doubleLoopStr for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R let K be non empty commutative distributive left_unital doubleLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R let R be Element of i -tuples_on the carrier of K; ::_thesis: (1. K) * R = R A1: rng R c= the carrier of K by FINSEQ_1:def_4; the_unity_wrt the multF of K = 1. K by Th5; hence (1. K) * R = (id the carrier of K) * R by FINSEQOP:44 .= R by A1, RELAT_1:53 ; ::_thesis: verum end; theorem :: FVSUM_1:58 for i being Element of NAT for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K) proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K) let K be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K) let R be Element of i -tuples_on the carrier of K; ::_thesis: (0. K) * R = i |-> (0. K) A1: rng R c= the carrier of K by FINSEQ_1:def_4; A2: the addF of K is having_an_inverseOp by Th14; A3: ( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8; thus (0. K) * R = the multF of K [;] ((0. K),((id the carrier of K) * R)) by FUNCOP_1:34 .= the multF of K [;] ((0. K),R) by A1, RELAT_1:53 .= i |-> (0. K) by A3, A2, Th10, FINSEQOP:76 ; ::_thesis: verum end; theorem :: FVSUM_1:59 for i being Element of NAT for K being non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R let K be non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R let R be Element of i -tuples_on the carrier of K; ::_thesis: (- (1. K)) * R = - R A1: ( (comp K) . (1. K) = - (1. K) & the_unity_wrt the multF of K = 1. K ) by Th5, VECTSP_1:def_13; A2: ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15; ( the multF of K is having_a_unity & the addF of K is having_a_unity ) by Th8; hence (- (1. K)) * R = - R by A1, A2, Th10, FINSEQOP:68; ::_thesis: verum end; definition let M be non empty multMagma ; let p1, p2 be FinSequence of the carrier of M; func mlt (p1,p2) -> FinSequence of the carrier of M equals :: FVSUM_1:def 7 the multF of M .: (p1,p2); correctness coherence the multF of M .: (p1,p2) is FinSequence of the carrier of M; ; end; :: deftheorem defines mlt FVSUM_1:def_7_:_ for M being non empty multMagma for p1, p2 being FinSequence of the carrier of M holds mlt (p1,p2) = the multF of M .: (p1,p2); theorem :: FVSUM_1:60 for i being Element of NAT for K being non empty multMagma for a1, a2 being Element of K for p1, p2 being FinSequence of the carrier of K st i in dom (mlt (p1,p2)) & a1 = p1 . i & a2 = p2 . i holds (mlt (p1,p2)) . i = a1 * a2 by FUNCOP_1:22; definition let i be Element of NAT ; let K be non empty multMagma ; let R1, R2 be Element of i -tuples_on the carrier of K; :: original: mlt redefine func mlt (R1,R2) -> Element of i -tuples_on the carrier of K; coherence mlt (R1,R2) is Element of i -tuples_on the carrier of K by FINSEQ_2:120; end; theorem :: FVSUM_1:61 for j, i being Element of NAT for K being non empty multMagma for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (mlt (R1,R2)) . j = a1 * a2 proof let j, i be Element of NAT ; ::_thesis: for K being non empty multMagma for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (mlt (R1,R2)) . j = a1 * a2 let K be non empty multMagma ; ::_thesis: for a1, a2 being Element of K for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (mlt (R1,R2)) . j = a1 * a2 let a1, a2 be Element of K; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds (mlt (R1,R2)) . j = a1 * a2 let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a1 = R1 . j & a2 = R2 . j implies (mlt (R1,R2)) . j = a1 * a2 ) assume j in Seg i ; ::_thesis: ( not a1 = R1 . j or not a2 = R2 . j or (mlt (R1,R2)) . j = a1 * a2 ) then j in Seg (len (mlt (R1,R2))) by CARD_1:def_7; then j in dom (mlt (R1,R2)) by FINSEQ_1:def_3; hence ( not a1 = R1 . j or not a2 = R2 . j or (mlt (R1,R2)) . j = a1 * a2 ) by FUNCOP_1:22; ::_thesis: verum end; theorem :: FVSUM_1:62 for K being non empty multMagma for a1, a2 being Element of K holds mlt (<*a1*>,<*a2*>) = <*(a1 * a2)*> by FINSEQ_2:74; Lm5: for K being non empty multMagma for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*> proof let K be non empty multMagma ; ::_thesis: for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*> let a1, a2, b1, b2 be Element of K; ::_thesis: mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*> ( <*a1,a2*> = <*a1*> ^ <*a2*> & <*b1,b2*> = <*b1*> ^ <*b2*> ) by FINSEQ_1:def_9; hence mlt (<*a1,a2*>,<*b1,b2*>) = (mlt (<*a1*>,<*b1*>)) ^ <*(a2 * b2)*> by FINSEQOP:10 .= <*(a1 * b1)*> ^ <*(a2 * b2)*> by FINSEQ_2:74 .= <*(a1 * b1),(a2 * b2)*> by FINSEQ_1:def_9 ; ::_thesis: verum end; theorem :: FVSUM_1:63 for i being Element of NAT for K being non empty commutative multMagma for R1, R2 being Element of i -tuples_on the carrier of K holds mlt (R1,R2) = mlt (R2,R1) by FINSEQOP:33; theorem Th64: :: FVSUM_1:64 for K being non empty commutative multMagma for p, q being FinSequence of the carrier of K holds mlt (p,q) = mlt (q,p) proof let K be non empty commutative multMagma ; ::_thesis: for p, q being FinSequence of the carrier of K holds mlt (p,q) = mlt (q,p) let p, q be FinSequence of the carrier of K; ::_thesis: mlt (p,q) = mlt (q,p) reconsider r = mlt (p,q) as FinSequence of the carrier of K ; reconsider s = mlt (q,p) as FinSequence of the carrier of K ; reconsider k = min ((len p),(len q)) as Element of NAT by XXREAL_0:15; A1: len r = min ((len p),(len q)) by FINSEQ_2:71; then A2: dom r = Seg k by FINSEQ_1:def_3; min ((len p),(len q)) <= len q by XXREAL_0:17; then Seg k c= Seg (len q) by FINSEQ_1:5; then A3: Seg k c= dom q by FINSEQ_1:def_3; min ((len p),(len q)) <= len p by XXREAL_0:17; then Seg k c= Seg (len p) by FINSEQ_1:5; then A4: Seg k c= dom p by FINSEQ_1:def_3; A5: len s = min ((len q),(len p)) by FINSEQ_2:71; then A6: dom s = Seg k by FINSEQ_1:def_3; A7: dom r = Seg k by A1, FINSEQ_1:def_3; now__::_thesis:_for_i_being_Nat_st_i_in_dom_r_holds_ r_._i_=_s_._i let i be Nat; ::_thesis: ( i in dom r implies r . i = s . i ) assume A8: i in dom r ; ::_thesis: r . i = s . i then reconsider d1 = p . i, d2 = q . i as Element of K by A4, A3, A2, FINSEQ_2:11; thus r . i = d1 * d2 by A8, FUNCOP_1:22 .= d2 * d1 .= s . i by A7, A6, A8, FUNCOP_1:22 ; ::_thesis: verum end; hence mlt (p,q) = mlt (q,p) by A1, A5, FINSEQ_2:9; ::_thesis: verum end; theorem :: FVSUM_1:65 for i being Element of NAT for K being non empty associative multMagma for R1, R2, R3 being Element of i -tuples_on the carrier of K holds mlt (R1,(mlt (R2,R3))) = mlt ((mlt (R1,R2)),R3) by FINSEQOP:28; theorem Th66: :: FVSUM_1:66 for i being Element of NAT for K being non empty associative commutative multMagma for a being Element of K for R being Element of i -tuples_on the carrier of K holds ( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R ) proof let i be Element of NAT ; ::_thesis: for K being non empty associative commutative multMagma for a being Element of K for R being Element of i -tuples_on the carrier of K holds ( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R ) let K be non empty associative commutative multMagma ; ::_thesis: for a being Element of K for R being Element of i -tuples_on the carrier of K holds ( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R ) let a be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K holds ( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R ) let R be Element of i -tuples_on the carrier of K; ::_thesis: ( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R ) thus mlt ((i |-> a),R) = the multF of K [;] (a,R) by FINSEQOP:20 .= a * R by FINSEQOP:22 ; ::_thesis: mlt (R,(i |-> a)) = a * R hence mlt (R,(i |-> a)) = a * R by FINSEQOP:33; ::_thesis: verum end; theorem :: FVSUM_1:67 for i being Element of NAT for K being non empty associative commutative multMagma for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2) proof let i be Element of NAT ; ::_thesis: for K being non empty associative commutative multMagma for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2) let K be non empty associative commutative multMagma ; ::_thesis: for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2) let a1, a2 be Element of K; ::_thesis: mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2) thus mlt ((i |-> a1),(i |-> a2)) = a1 * (i |-> a2) by Th66 .= i |-> (a1 * a2) by Th53 ; ::_thesis: verum end; theorem :: FVSUM_1:68 for i being Element of NAT for K being non empty associative multMagma for a being Element of K for R1, R2 being Element of i -tuples_on the carrier of K holds a * (mlt (R1,R2)) = mlt ((a * R1),R2) by FINSEQOP:26; theorem :: FVSUM_1:69 for i being Element of NAT for K being non empty associative commutative multMagma for a being Element of K for R1, R2 being Element of i -tuples_on the carrier of K holds ( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) ) proof let i be Element of NAT ; ::_thesis: for K being non empty associative commutative multMagma for a being Element of K for R1, R2 being Element of i -tuples_on the carrier of K holds ( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) ) let K be non empty associative commutative multMagma ; ::_thesis: for a being Element of K for R1, R2 being Element of i -tuples_on the carrier of K holds ( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) ) let a be Element of K; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds ( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) ) let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) ) thus a * (mlt (R1,R2)) = mlt ((a * R1),R2) by FINSEQOP:26; ::_thesis: a * (mlt (R1,R2)) = mlt (R1,(a * R2)) thus a * (mlt (R1,R2)) = a * (mlt (R2,R1)) by FINSEQOP:33 .= mlt ((a * R2),R1) by FINSEQOP:26 .= mlt (R1,(a * R2)) by FINSEQOP:33 ; ::_thesis: verum end; theorem :: FVSUM_1:70 for i being Element of NAT for K being non empty associative commutative multMagma for a being Element of K for R being Element of i -tuples_on the carrier of K holds a * R = mlt ((i |-> a),R) by Th66; begin registration cluster non empty Abelian right_zeroed -> non empty left_zeroed for addLoopStr ; coherence for b1 being non empty addLoopStr st b1 is Abelian & b1 is right_zeroed holds b1 is left_zeroed proof let L be non empty addLoopStr ; ::_thesis: ( L is Abelian & L is right_zeroed implies L is left_zeroed ) assume that A1: L is Abelian and A2: L is right_zeroed ; ::_thesis: L is left_zeroed let x be Element of L; :: according to ALGSTR_1:def_2 ::_thesis: (0. L) + x = x thus (0. L) + x = x + (0. L) by A1, RLVECT_1:def_2 .= x by A2, RLVECT_1:def_4 ; ::_thesis: verum end; end; definition let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; let p be FinSequence of the carrier of K; redefine func Sum p equals :: FVSUM_1:def 8 the addF of K $$ p; compatibility for b1 being Element of the carrier of K holds ( b1 = Sum p iff b1 = the addF of K $$ p ) proof set q = <*> the carrier of K; deffunc H1( Element of NAT ) -> Element of the carrier of K = the addF of K $$ (p | $1); let s be Element of K; ::_thesis: ( s = Sum p iff s = the addF of K $$ p ) consider f being Function of NAT, the carrier of K such that A1: for i being Element of NAT holds f . i = H1(i) from FUNCT_2:sch_4(); hereby ::_thesis: ( s = the addF of K $$ p implies s = Sum p ) defpred S1[ set , set ] means ex q being FinSequence of the carrier of K st ( q = p * (Sgm (dom (p | $1))) & $2 = Sum q ); assume A2: s = Sum p ; ::_thesis: s = the addF of K $$ p A3: for x being Element of Fin NAT ex y being Element of K st S1[x,y] proof let B be Element of Fin NAT; ::_thesis: ex y being Element of K st S1[B,y] percases ( dom p = {} or dom p <> {} ) ; supposeA4: dom p = {} ; ::_thesis: ex y being Element of K st S1[B,y] reconsider u = Sum (<*> the carrier of K) as Element of K ; reconsider q = <*> the carrier of K as FinSequence of the carrier of K ; take u ; ::_thesis: S1[B,u] take q ; ::_thesis: ( q = p * (Sgm (dom (p | B))) & u = Sum q ) p = {} by A4; hence q = p * (Sgm (dom (p | B))) ; ::_thesis: u = Sum q thus u = Sum q ; ::_thesis: verum end; suppose dom p <> {} ; ::_thesis: ex y being Element of K st S1[B,y] then reconsider domp = dom p as non empty set ; reconsider p9 = p as Function of domp, the carrier of K by FINSEQ_2:26; A5: dom (p | B) c= dom p by RELAT_1:60; reconsider pB = p | B as FinSubsequence ; rng (Sgm (dom pB)) = dom pB by FINSEQ_1:50; then reconsider p99 = Sgm (dom (p | B)) as FinSequence of domp by A5, FINSEQ_1:def_4; reconsider q = p9 * p99 as FinSequence of the carrier of K ; reconsider u = Sum q as Element of K ; take u ; ::_thesis: S1[B,u] take q ; ::_thesis: ( q = p * (Sgm (dom (p | B))) & u = Sum q ) thus ( q = p * (Sgm (dom (p | B))) & u = Sum q ) ; ::_thesis: verum end; end; end; consider G being Function of (Fin NAT), the carrier of K such that A6: for B being Element of Fin NAT holds S1[B,G . B] from FUNCT_2:sch_3(A3); A7: now__::_thesis:_for_B9_being_Element_of_Fin_NAT_st_B9_c=_dom_p_&_B9_<>_{}_holds_ for_x_being_Element_of_NAT_st_x_in_(dom_p)_\_B9_holds_ G_._(B9_\/_{x})_=_the_addF_of_K_._((G_._B9),(([#]_(p,(the_unity_wrt_the_addF_of_K)))_._x)) let B9 be Element of Fin NAT; ::_thesis: ( B9 c= dom p & B9 <> {} implies for x being Element of NAT st x in (dom p) \ B9 holds G . (B9 \/ {x}) = the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) ) assume that B9 c= dom p and B9 <> {} ; ::_thesis: for x being Element of NAT st x in (dom p) \ B9 holds G . (B9 \/ {x}) = the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) let x be Element of NAT ; ::_thesis: ( x in (dom p) \ B9 implies G . (B9 \/ {x}) = the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) ) set f2 = Sgm (dom (p | (B9 \/ {x}))); set f3 = (Sgm (dom (p | (B9 \/ {x})))) -| x; set f4 = (Sgm (dom (p | (B9 \/ {x})))) |-- x; reconsider Y = (finSeg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}) as finite set ; A8: Seg (len (Sgm (dom (p | (B9 \/ {x}))))) = dom (Sgm (dom (p | (B9 \/ {x})))) by FINSEQ_1:def_3; set R = rng ((Sgm (dom (p | (B9 \/ {x})))) | Y); set M = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y); A9: rng (Sgm Y) = Y by FINSEQ_1:def_13; dom (Sgm Y) = finSeg (card Y) by FINSEQ_3:40; then dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) = Seg (card Y) by A8, A9, RELAT_1:27; then reconsider M = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y) as FinSequence by FINSEQ_1:def_2; ( rng (Sgm (dom (p | (B9 \/ {x})))) c= NAT & rng M c= rng (Sgm (dom (p | (B9 \/ {x})))) ) by FINSEQ_1:def_4, RELAT_1:26; then rng M c= NAT by XBOOLE_1:1; then reconsider L = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y) as FinSequence of NAT by FINSEQ_1:def_4; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_L_implies_y_in_rng_((Sgm_(dom_(p_|_(B9_\/_{x}))))_|_Y)_)_&_(_y_in_rng_((Sgm_(dom_(p_|_(B9_\/_{x}))))_|_Y)_implies_y_in_rng_L_)_) let y be set ; ::_thesis: ( ( y in rng L implies y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) ) & ( y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) implies y in rng L ) ) hereby ::_thesis: ( y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) implies y in rng L ) assume y in rng L ; ::_thesis: y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) then consider x being set such that A10: x in dom L and A11: y = L . x by FUNCT_1:def_3; x in dom (Sgm Y) by A10, FUNCT_1:11; then A12: (Sgm Y) . x in Y by A9, FUNCT_1:def_3; y = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . x) by A10, A11, FUNCT_1:12; hence y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by A8, A12, FUNCT_1:50; ::_thesis: verum end; assume y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) ; ::_thesis: y in rng L then consider x being set such that A13: x in dom ((Sgm (dom (p | (B9 \/ {x})))) | Y) and A14: y = ((Sgm (dom (p | (B9 \/ {x})))) | Y) . x by FUNCT_1:def_3; A15: x in (dom (Sgm (dom (p | (B9 \/ {x}))))) /\ Y by A13, RELAT_1:61; then A16: x in Y by XBOOLE_0:def_4; then consider z being set such that A17: z in dom (Sgm Y) and A18: x = (Sgm Y) . z by A9, FUNCT_1:def_3; x in dom (Sgm (dom (p | (B9 \/ {x})))) by A15, XBOOLE_0:def_4; then A19: z in dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) by A17, A18, FUNCT_1:11; then L . z = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . z) by FUNCT_1:12 .= y by A14, A16, A18, FUNCT_1:49 ; hence y in rng L by A19, FUNCT_1:def_3; ::_thesis: verum end; then A20: rng L = rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by TARSKI:1; x in {x} by TARSKI:def_1; then A21: x in B9 \/ {x} by XBOOLE_0:def_3; dom (p | (B9 \/ {x})) = (dom p) /\ (B9 \/ {x}) by RELAT_1:61; then dom (p | (B9 \/ {x})) c= dom p by XBOOLE_1:17; then A22: dom (p | (B9 \/ {x})) c= Seg (len p) by FINSEQ_1:def_3; reconsider pB9x = p | (B9 \/ {x}) as FinSubsequence ; rng (Sgm (dom (p | (B9 \/ {x})))) c= Seg (len p) by A22, FINSEQ_1:def_13; then A23: rng (Sgm (dom (p | (B9 \/ {x})))) c= dom p by FINSEQ_1:def_3; rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= rng (Sgm (dom (p | (B9 \/ {x})))) by RELAT_1:70; then rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= dom p by A23, XBOOLE_1:1; then A24: rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= Seg (len p) by FINSEQ_1:def_3; reconsider pp = p | (B9 \/ {x}) as FinSubsequence ; A25: dom (p | B9) = (dom p) /\ B9 by RELAT_1:61; A26: now__::_thesis:_for_l,_m,_k1,_k2_being_Nat_st_1_<=_l_&_l_<_m_&_m_<=_len_L_&_k1_=_L_._l_&_k2_=_L_._m_holds_ k1_<_k2 let l, m, k1, k2 be Nat; ::_thesis: ( 1 <= l & l < m & m <= len L & k1 = L . l & k2 = L . m implies k1 < k2 ) assume that A27: 1 <= l and A28: l < m and A29: m <= len L and A30: ( k1 = L . l & k2 = L . m ) ; ::_thesis: k1 < k2 l <= len L by A28, A29, XXREAL_0:2; then A31: l in dom L by A27, FINSEQ_3:25; then A32: L . l = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . l) by FUNCT_1:12; A33: (Sgm Y) . l in dom (Sgm (dom (p | (B9 \/ {x})))) by A31, FUNCT_1:11; 1 <= m by A27, A28, XXREAL_0:2; then A34: m in dom L by A29, FINSEQ_3:25; then A35: L . m = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . m) by FUNCT_1:12; m in dom (Sgm Y) by A34, FUNCT_1:11; then A36: m <= len (Sgm Y) by FINSEQ_3:25; A37: (Sgm Y) . m in dom (Sgm (dom (p | (B9 \/ {x})))) by A34, FUNCT_1:11; reconsider l = l, m = m as Element of NAT by ORDINAL1:def_12; reconsider K1 = (Sgm Y) . l, K2 = (Sgm Y) . m as Element of NAT by A33, A37; A38: 1 <= K1 by A33, FINSEQ_3:25; A39: K2 <= len (Sgm (dom (p | (B9 \/ {x})))) by A37, FINSEQ_3:25; K1 < K2 by A27, A28, A36, FINSEQ_1:def_13; hence k1 < k2 by A22, A30, A32, A35, A38, A39, FINSEQ_1:def_13; ::_thesis: verum end; assume A40: x in (dom p) \ B9 ; ::_thesis: G . (B9 \/ {x}) = the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) then A41: x in dom p by XBOOLE_0:def_5; then reconsider D = dom p, E = rng p as non empty set by RELAT_1:42; x in dom p by A40, XBOOLE_0:def_5; then A42: {x} c= dom p by ZFMISC_1:31; p . x = p /. x by A41, PARTFUN1:def_6; then reconsider px = p . x as Element of K ; A43: dom <*px*> = Seg 1 by FINSEQ_1:38; rng <*x*> = {x} by FINSEQ_1:38; then ( dom <*x*> = Seg 1 & rng <*x*> c= dom p ) by A41, FINSEQ_1:38, ZFMISC_1:31; then A44: dom (p * <*x*>) = dom <*px*> by A43, RELAT_1:27; A45: now__::_thesis:_for_e_being_set_st_e_in_dom_<*px*>_holds_ (p_*_<*x*>)_._e_=_<*px*>_._e let e be set ; ::_thesis: ( e in dom <*px*> implies (p * <*x*>) . e = <*px*> . e ) assume A46: e in dom <*px*> ; ::_thesis: (p * <*x*>) . e = <*px*> . e then A47: e = 1 by A43, FINSEQ_1:2, TARSKI:def_1; thus (p * <*x*>) . e = p . (<*x*> . e) by A44, A46, FUNCT_1:12 .= p . x by A47, FINSEQ_1:40 .= <*px*> . e by A47, FINSEQ_1:40 ; ::_thesis: verum end; reconsider x9 = x as Element of D by A40, XBOOLE_0:def_5; reconsider p9 = p as Function of D,E by FUNCT_2:1; A48: E c= the carrier of K by FINSEQ_1:def_4; not x in B9 by A40, XBOOLE_0:def_5; then A49: not x in dom (p | B9) by A25, XBOOLE_0:def_4; A50: rng (Sgm (dom pp)) = dom pp by FINSEQ_1:50; then A51: rng (Sgm (dom (p | (B9 \/ {x})))) c= dom p by RELAT_1:60; dom pp = (dom p) /\ (B9 \/ {x}) by RELAT_1:61; then A52: x in rng (Sgm (dom (p | (B9 \/ {x})))) by A50, A41, A21, XBOOLE_0:def_4; then rng ((Sgm (dom (p | (B9 \/ {x})))) |-- x) c= rng (Sgm (dom (p | (B9 \/ {x})))) by FINSEQ_4:44; then A53: rng ((Sgm (dom (p | (B9 \/ {x})))) |-- x) c= D by A51, XBOOLE_1:1; rng ((Sgm (dom (p | (B9 \/ {x})))) -| x) c= rng (Sgm (dom (p | (B9 \/ {x})))) by A52, FINSEQ_4:39; then rng ((Sgm (dom (p | (B9 \/ {x})))) -| x) c= D by A51, XBOOLE_1:1; then reconsider f39 = (Sgm (dom (p | (B9 \/ {x})))) -| x, f49 = (Sgm (dom (p | (B9 \/ {x})))) |-- x as FinSequence of D by A53, FINSEQ_1:def_4; consider q2 being FinSequence of the carrier of K such that A54: q2 = p * (Sgm (dom (p | (B9 \/ {x})))) and A55: G . (B9 \/ {.x.}) = Sum q2 by A6; reconsider p3 = p9 * f39, p4 = p9 * f49 as FinSequence of E ; rng p3 c= E by FINSEQ_1:def_4; then A56: rng p3 c= the carrier of K by A48, XBOOLE_1:1; rng p4 c= E by FINSEQ_1:def_4; then rng p4 c= the carrier of K by A48, XBOOLE_1:1; then reconsider p3 = p3, p4 = p4 as FinSequence of the carrier of K by A56, FINSEQ_1:def_4; consider q1 being FinSequence of the carrier of K such that A57: q1 = p * (Sgm (dom (p | B9))) and A58: G . B9 = Sum q1 by A6; A59: Sgm (dom (p | (B9 \/ {x}))) is one-to-one by A22, FINSEQ_3:92; rng ((Sgm (dom (p | (B9 \/ {x})))) | ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) = (Sgm (dom (p | (B9 \/ {x})))) .: ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x})) by RELAT_1:115 .= (Sgm (dom (p | (B9 \/ {x})))) .: ((dom (Sgm (dom (p | (B9 \/ {x}))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x})) by FINSEQ_1:def_3 .= ((Sgm (dom (p | (B9 \/ {x})))) .: (dom (Sgm (dom (p | (B9 \/ {x})))))) \ {x} by SETWISEO:6 .= (rng (Sgm (dom pB9x))) \ {x} by RELAT_1:113 .= (dom (p | (B9 \/ {x}))) \ {x} by FINSEQ_1:50 .= ((dom p) /\ (B9 \/ {x})) \ {x} by RELAT_1:61 .= (((dom p) /\ B9) \/ ((dom p) /\ {x})) \ {x} by XBOOLE_1:23 .= (((dom p) /\ B9) \/ {x}) \ {x} by A42, XBOOLE_1:28 .= (dom (p | B9)) \ {x} by A25, XBOOLE_1:40 .= dom (p | B9) by A49, ZFMISC_1:57 ; then Sgm (dom (p | B9)) = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) by A24, A20, A26, FINSEQ_1:def_13 .= (Sgm (dom (p | (B9 \/ {x})))) * (Sgm ((dom (Sgm (dom (p | (B9 \/ {x}))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) by FINSEQ_1:def_3 .= (Sgm (dom (p | (B9 \/ {x})))) - {x} by FINSEQ_3:def_1 .= ((Sgm (dom (p | (B9 \/ {x})))) -| x) ^ ((Sgm (dom (p | (B9 \/ {x})))) |-- x) by A52, A59, FINSEQ_4:55 ; then A60: q1 = p3 ^ p4 by A57, FINSEQOP:9; q2 = p9 * ((f39 ^ <*x9*>) ^ f49) by A54, A52, FINSEQ_4:51 .= (p9 * (f39 ^ <*x9*>)) ^ (p9 * f49) by FINSEQOP:9 .= ((p9 * f39) ^ (p9 * <*x9*>)) ^ (p9 * f49) by FINSEQOP:9 .= (p3 ^ <*px*>) ^ p4 by A44, A45, FUNCT_1:2 ; hence G . (B9 \/ {x}) = (Sum (p3 ^ <*px*>)) + (Sum p4) by A55, RLVECT_1:41 .= ((Sum p3) + (Sum <*px*>)) + (Sum p4) by RLVECT_1:41 .= ((Sum p3) + (Sum p4)) + (Sum <*px*>) by RLVECT_1:def_3 .= (Sum q1) + (Sum <*px*>) by A60, RLVECT_1:41 .= the addF of K . ((Sum q1),px) by RLVECT_1:44 .= the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) by A58, A41, SETWOP_2:20 ; ::_thesis: verum end; A61: now__::_thesis:_for_x_being_Element_of_NAT_holds_G_._{x}_=_([#]_(p,(the_unity_wrt_the_addF_of_K)))_._x let x be Element of NAT ; ::_thesis: G . {b1} = ([#] (p,(the_unity_wrt the addF of K))) . b1 consider q being FinSequence of the carrier of K such that A62: q = p * (Sgm (dom (p | {x}))) and A63: G . {.x.} = Sum q by A6; A64: {} c= Seg 0 ; percases ( not x in dom p or x in dom p ) ; supposeA65: not x in dom p ; ::_thesis: G . {b1} = ([#] (p,(the_unity_wrt the addF of K))) . b1 then dom p misses {x} by ZFMISC_1:50; then (dom p) /\ {x} = {} by XBOOLE_0:def_7; then q = p * (Sgm {}) by A62, RELAT_1:61 .= p * {} by A64, FINSEQ_1:51 .= <*> the carrier of K ; hence G . {x} = 0. K by A63, RLVECT_1:43 .= the_unity_wrt the addF of K by Th7 .= ([#] (p,(the_unity_wrt the addF of K))) . x by A65, SETWOP_2:20 ; ::_thesis: verum end; supposeA66: x in dom p ; ::_thesis: G . {b1} = ([#] (p,(the_unity_wrt the addF of K))) . b1 then p . x = p /. x by PARTFUN1:def_6; then reconsider px = p . x as Element of K ; A67: dom <*px*> = Seg 1 by FINSEQ_1:38; rng <*x*> = {x} by FINSEQ_1:38; then ( dom <*x*> = Seg 1 & rng <*x*> c= dom p ) by A66, FINSEQ_1:38, ZFMISC_1:31; then A68: dom (p * <*x*>) = dom <*px*> by A67, RELAT_1:27; A69: now__::_thesis:_for_e_being_set_st_e_in_dom_<*px*>_holds_ (p_*_<*x*>)_._e_=_<*px*>_._e let e be set ; ::_thesis: ( e in dom <*px*> implies (p * <*x*>) . e = <*px*> . e ) assume A70: e in dom <*px*> ; ::_thesis: (p * <*x*>) . e = <*px*> . e then A71: e = 1 by A67, FINSEQ_1:2, TARSKI:def_1; thus (p * <*x*>) . e = p . (<*x*> . e) by A68, A70, FUNCT_1:12 .= p . x by A71, FINSEQ_1:40 .= <*px*> . e by A71, FINSEQ_1:40 ; ::_thesis: verum end; A72: x <> 0 by A66, FINSEQ_3:25; q = p * (Sgm ((dom p) /\ {x})) by A62, RELAT_1:61 .= p * (Sgm {x}) by A66, ZFMISC_1:46 .= p * <*x*> by A72, FINSEQ_3:44 .= <*px*> by A68, A69, FUNCT_1:2 ; hence G . {x} = px by A63, RLVECT_1:44 .= ([#] (p,(the_unity_wrt the addF of K))) . x by A66, SETWOP_2:20 ; ::_thesis: verum end; end; end; A73: now__::_thesis:_for_e_being_Element_of_K_st_e_is_a_unity_wrt_the_addF_of_K_holds_ e_=_G_._{} let e be Element of K; ::_thesis: ( e is_a_unity_wrt the addF of K implies e = G . {} ) assume A74: e is_a_unity_wrt the addF of K ; ::_thesis: e = G . {} 0. K is_a_unity_wrt the addF of K by Th6; then A75: e = 0. K by A74, BINOP_1:10; A76: {} c= Seg 0 ; consider q being FinSequence of the carrier of K such that A77: q = p * (Sgm (dom (p | ({}. NAT)))) and A78: G . ({}. NAT) = Sum q by A6; q = p * (Sgm (dom {})) by A77 .= p * {} by A76, FINSEQ_1:51 .= <*> the carrier of K ; hence e = G . {} by A78, A75, RLVECT_1:43; ::_thesis: verum end; consider q1 being FinSequence of the carrier of K such that A79: q1 = p * (Sgm (dom (p | (dom p)))) and A80: G . (findom p) = Sum q1 by A6; A81: the addF of K is having_a_unity by Th8; q1 = p * (Sgm (dom p)) by A79 .= p * (Sgm (Seg (len p))) by FINSEQ_1:def_3 .= p * (idseq (len p)) by FINSEQ_3:48 .= p by FINSEQ_2:54 ; hence s = the addF of K $$ ((findom p),([#] (p,(the_unity_wrt the addF of K)))) by A2, A81, A80, A73, A61, A7, SETWISEO:def_3 .= the addF of K $$ p by Th8, SETWOP_2:def_2 ; ::_thesis: verum end; A82: p | (len p) = p | (Seg (len p)) by FINSEQ_1:def_15 .= p | (dom p) by FINSEQ_1:def_3 .= p ; A83: now__::_thesis:_for_j_being_Element_of_NAT_ for_a_being_Element_of_K_st_j_<_len_p_&_a_=_p_._(j_+_1)_holds_ f_._(j_+_1)_=_(f_._j)_+_a let j be Element of NAT ; ::_thesis: for a being Element of K st j < len p & a = p . (j + 1) holds f . (j + 1) = (f . j) + a let a be Element of K; ::_thesis: ( j < len p & a = p . (j + 1) implies f . (j + 1) = (f . j) + a ) assume that A84: j < len p and A85: a = p . (j + 1) ; ::_thesis: f . (j + 1) = (f . j) + a A86: j + 1 <= len p by A84, NAT_1:13; then A87: len (p | (j + 1)) = j + 1 by FINSEQ_1:59; j <= j + 1 by NAT_1:11; then A88: Seg j c= Seg (j + 1) by FINSEQ_1:5; A89: p | j = p | (Seg j) by FINSEQ_1:def_15 .= (p | (Seg (j + 1))) | (Seg j) by A88, RELAT_1:74 .= (p | (j + 1)) | (Seg j) by FINSEQ_1:def_15 ; A90: 1 <= j + 1 by NAT_1:11; then A91: j + 1 in dom (p | (j + 1)) by A87, FINSEQ_3:25; j + 1 in dom p by A86, A90, FINSEQ_3:25; then a = p /. (j + 1) by A85, PARTFUN1:def_6 .= (p | (j + 1)) /. (j + 1) by A91, FINSEQ_4:70 .= (p | (j + 1)) . (j + 1) by A91, PARTFUN1:def_6 ; then p | (j + 1) = (p | j) ^ <*a*> by A87, A89, FINSEQ_3:55; hence f . (j + 1) = the addF of K $$ ((p | j) ^ <*a*>) by A1 .= the addF of K . (( the addF of K $$ (p | j)),a) by Th8, FINSOP_1:4 .= (f . j) + a by A1 ; ::_thesis: verum end; p | 0 = <*> the carrier of K ; then A92: f . 0 = the addF of K $$ (<*> the carrier of K) by A1 .= the_unity_wrt the addF of K by Th8, FINSOP_1:10 .= 0. K by Th7 ; assume s = the addF of K $$ p ; ::_thesis: s = Sum p then s = f . (len p) by A1, A82; hence s = Sum p by A92, A83, RLVECT_1:def_12; ::_thesis: verum end; end; :: deftheorem defines Sum FVSUM_1:def_8_:_ for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for p being FinSequence of the carrier of K holds Sum p = the addF of K $$ p; theorem :: FVSUM_1:71 for K being non empty right_complementable add-associative right_zeroed addLoopStr for a being Element of K for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a proof let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a being Element of K for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a let a be Element of K; ::_thesis: for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a let p be FinSequence of the carrier of K; ::_thesis: Sum (p ^ <*a*>) = (Sum p) + a thus Sum (p ^ <*a*>) = (Sum p) + (Sum <*a*>) by RLVECT_1:41 .= (Sum p) + a by RLVECT_1:44 ; ::_thesis: verum end; theorem :: FVSUM_1:72 for K being non empty right_complementable add-associative right_zeroed addLoopStr for a being Element of K for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p) proof let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a being Element of K for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p) let a be Element of K; ::_thesis: for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p) let p be FinSequence of the carrier of K; ::_thesis: Sum (<*a*> ^ p) = a + (Sum p) thus Sum (<*a*> ^ p) = (Sum <*a*>) + (Sum p) by RLVECT_1:41 .= a + (Sum p) by RLVECT_1:44 ; ::_thesis: verum end; theorem :: FVSUM_1:73 for K being non empty right_complementable Abelian add-associative right_zeroed distributive doubleLoopStr for a being Element of K for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p) proof let K be non empty right_complementable Abelian add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for a being Element of K for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p) let a be Element of K; ::_thesis: for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p) let p be FinSequence of the carrier of K; ::_thesis: Sum (a * p) = a * (Sum p) set rM = the multF of K [;] (a,(id the carrier of K)); ( the addF of K is having_a_unity & the multF of K is_distributive_wrt the addF of K ) by Th8, Th10; hence Sum (a * p) = ( the multF of K [;] (a,(id the carrier of K))) . (Sum p) by Th14, SETWOP_2:30 .= a * (Sum p) by Lm1 ; ::_thesis: verum end; theorem :: FVSUM_1:74 for K being non empty addLoopStr for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K proof let K be non empty addLoopStr ; ::_thesis: for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K let R be Element of 0 -tuples_on the carrier of K; ::_thesis: Sum R = 0. K R = <*> the carrier of K ; hence Sum R = 0. K by RLVECT_1:43; ::_thesis: verum end; theorem :: FVSUM_1:75 for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p) proof let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p) let p be FinSequence of the carrier of K; ::_thesis: Sum (- p) = - (Sum p) ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15; hence Sum (- p) = (comp K) . (Sum p) by Th8, SETWOP_2:31 .= - (Sum p) by VECTSP_1:def_13 ; ::_thesis: verum end; theorem :: FVSUM_1:76 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 + R2) = (Sum R1) + (Sum R2) by Th8, SETWOP_2:35; theorem :: FVSUM_1:77 for i being Element of NAT for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2) proof let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2) let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2) let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2) ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15; hence Sum (R1 - R2) = (diffield K) . ((Sum R1),( the addF of K $$ R2)) by Th8, SETWOP_2:37 .= (Sum R1) - (Sum R2) by Th11 ; ::_thesis: verum end; begin Lm6: for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K proof let K be non empty commutative well-unital multLoopStr ; ::_thesis: Product (<*> the carrier of K) = 1. K 1. K = 1_ K ; hence Product (<*> the carrier of K) = 1. K by GROUP_4:8; ::_thesis: verum end; theorem :: FVSUM_1:78 for K being non empty associative commutative well-unital doubleLoopStr for a being Element of K for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1) proof let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: for a being Element of K for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1) let a be Element of K; ::_thesis: for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1) let p1 be FinSequence of the carrier of K; ::_thesis: Product (<*a*> ^ p1) = a * (Product p1) thus Product (<*a*> ^ p1) = (Product <*a*>) * (Product p1) by GROUP_4:5 .= a * (Product p1) by FINSOP_1:11 ; ::_thesis: verum end; theorem :: FVSUM_1:79 for K being non empty associative commutative well-unital doubleLoopStr for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3 proof let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3 let a1, a2, a3 be Element of K; ::_thesis: Product <*a1,a2,a3*> = (a1 * a2) * a3 thus Product <*a1,a2,a3*> = Product (<*a1,a2*> ^ <*a3*>) by FINSEQ_1:43 .= (Product <*a1,a2*>) * a3 by GROUP_4:6 .= (a1 * a2) * a3 by FINSOP_1:12 ; ::_thesis: verum end; theorem :: FVSUM_1:80 for K being non empty associative commutative well-unital doubleLoopStr for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K proof let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K let R be Element of 0 -tuples_on the carrier of K; ::_thesis: Product R = 1. K R = <*> the carrier of K ; hence Product R = 1. K by Lm6; ::_thesis: verum end; theorem :: FVSUM_1:81 for i being Element of NAT for K being non empty associative commutative well-unital doubleLoopStr holds Product (i |-> (1_ K)) = 1_ K proof let i be Element of NAT ; ::_thesis: for K being non empty associative commutative well-unital doubleLoopStr holds Product (i |-> (1_ K)) = 1_ K let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: Product (i |-> (1_ K)) = 1_ K the_unity_wrt the multF of K = 1_ K by Th5; hence Product (i |-> (1_ K)) = 1_ K by SETWOP_2:25; ::_thesis: verum end; theorem :: FVSUM_1:82 for K being non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for p being FinSequence of the carrier of K holds ( ex k being Element of NAT st ( k in dom p & p . k = 0. K ) iff Product p = 0. K ) proof let K be non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for p being FinSequence of the carrier of K holds ( ex k being Element of NAT st ( k in dom p & p . k = 0. K ) iff Product p = 0. K ) let p be FinSequence of the carrier of K; ::_thesis: ( ex k being Element of NAT st ( k in dom p & p . k = 0. K ) iff Product p = 0. K ) defpred S1[ Element of NAT ] means for p being FinSequence of the carrier of K st len p = $1 holds ( ex k being Element of NAT st ( k in Seg $1 & p . k = 0. K ) iff Product p = 0. K ); A1: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: for p being FinSequence of the carrier of K st len p = i holds ( ex k being Element of NAT st ( k in Seg i & p . k = 0. K ) iff Product p = 0. K ) ; ::_thesis: S1[i + 1] let p be FinSequence of the carrier of K; ::_thesis: ( len p = i + 1 implies ( ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) iff Product p = 0. K ) ) assume A3: len p = i + 1 ; ::_thesis: ( ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) iff Product p = 0. K ) then consider p9 being FinSequence of the carrier of K, a being Element of K such that A4: p = p9 ^ <*a*> by FINSEQ_2:19; A5: i + 1 = (len p9) + 1 by A3, A4, FINSEQ_2:16; then A6: i = len p9 by XCMPLX_1:2; A7: Product p = (Product p9) * a by A4, GROUP_4:6; thus ( ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) implies Product p = 0. K ) ::_thesis: ( Product p = 0. K implies ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) ) proof given k being Element of NAT such that A8: k in Seg (i + 1) and A9: p . k = 0. K ; ::_thesis: Product p = 0. K now__::_thesis:_Product_p_=_0._K percases ( k in Seg i or k = i + 1 ) by A8, FINSEQ_2:7; supposeA10: k in Seg i ; ::_thesis: Product p = 0. K then k in dom p9 by A6, FINSEQ_1:def_3; then p9 . k = p . k by A4, FINSEQ_1:def_7; then Product p9 = 0. K by A2, A6, A9, A10; hence Product p = 0. K by A7, VECTSP_1:7; ::_thesis: verum end; suppose k = i + 1 ; ::_thesis: Product p = 0. K then a = 0. K by A4, A5, A9, FINSEQ_1:42; hence Product p = 0. K by A7, VECTSP_1:7; ::_thesis: verum end; end; end; hence Product p = 0. K ; ::_thesis: verum end; assume A11: Product p = 0. K ; ::_thesis: ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) percases ( Product p9 = 0. K or a = 0. K ) by A7, A11, VECTSP_1:12; suppose Product p9 = 0. K ; ::_thesis: ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) then consider k being Element of NAT such that A12: k in Seg i and A13: p9 . k = 0. K by A2, A6; k in dom p9 by A6, A12, FINSEQ_1:def_3; then p . k = 0. K by A4, A13, FINSEQ_1:def_7; hence ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) by A12, FINSEQ_2:8; ::_thesis: verum end; suppose a = 0. K ; ::_thesis: ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) then p . (i + 1) = 0. K by A4, A5, FINSEQ_1:42; hence ex k being Element of NAT st ( k in Seg (i + 1) & p . k = 0. K ) by FINSEQ_1:4; ::_thesis: verum end; end; end; A14: Seg (len p) = dom p by FINSEQ_1:def_3; A15: S1[ 0 ] proof let p be FinSequence of the carrier of K; ::_thesis: ( len p = 0 implies ( ex k being Element of NAT st ( k in Seg 0 & p . k = 0. K ) iff Product p = 0. K ) ) assume len p = 0 ; ::_thesis: ( ex k being Element of NAT st ( k in Seg 0 & p . k = 0. K ) iff Product p = 0. K ) then p = <*> the carrier of K ; then A16: Product p = 1. K by Lm6; thus ( ex k being Element of NAT st ( k in Seg 0 & p . k = 0. K ) implies Product p = 0. K ) ; ::_thesis: ( Product p = 0. K implies ex k being Element of NAT st ( k in Seg 0 & p . k = 0. K ) ) assume Product p = 0. K ; ::_thesis: ex k being Element of NAT st ( k in Seg 0 & p . k = 0. K ) hence ex k being Element of NAT st ( k in Seg 0 & p . k = 0. K ) by A16; ::_thesis: verum end; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A15, A1); hence ( ex k being Element of NAT st ( k in dom p & p . k = 0. K ) iff Product p = 0. K ) by A14; ::_thesis: verum end; theorem :: FVSUM_1:83 for i, j being Element of NAT for K being non empty associative commutative well-unital doubleLoopStr for a being Element of K holds Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a)) by SETWOP_2:26; theorem :: FVSUM_1:84 for i, j being Element of NAT for K being non empty associative commutative well-unital doubleLoopStr for a being Element of K holds Product ((i * j) |-> a) = Product (j |-> (Product (i |-> a))) by SETWOP_2:27; theorem :: FVSUM_1:85 for i being Element of NAT for K being non empty associative commutative well-unital doubleLoopStr for a1, a2 being Element of K holds Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2)) by SETWOP_2:36; theorem Th86: :: FVSUM_1:86 for i being Element of NAT for K being non empty associative commutative well-unital doubleLoopStr for R1, R2 being Element of i -tuples_on the carrier of K holds Product (mlt (R1,R2)) = (Product R1) * (Product R2) by SETWOP_2:35; theorem :: FVSUM_1:87 for i being Element of NAT for K being non empty associative commutative well-unital doubleLoopStr for a being Element of K for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1) proof let i be Element of NAT ; ::_thesis: for K being non empty associative commutative well-unital doubleLoopStr for a being Element of K for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1) let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: for a being Element of K for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1) let a be Element of K; ::_thesis: for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1) let R1 be Element of i -tuples_on the carrier of K; ::_thesis: Product (a * R1) = (Product (i |-> a)) * (Product R1) thus Product (a * R1) = Product (mlt ((i |-> a),R1)) by Th66 .= (Product (i |-> a)) * (Product R1) by Th86 ; ::_thesis: verum end; begin definition let K be non empty doubleLoopStr ; let p, q be FinSequence of the carrier of K; funcp "*" q -> Element of K equals :: FVSUM_1:def 9 Sum (mlt (p,q)); coherence Sum (mlt (p,q)) is Element of K ; end; :: deftheorem defines "*" FVSUM_1:def_9_:_ for K being non empty doubleLoopStr for p, q being FinSequence of the carrier of K holds p "*" q = Sum (mlt (p,q)); theorem :: FVSUM_1:88 for K being non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr for a, b being Element of K holds <*a*> "*" <*b*> = a * b proof let K be non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr ; ::_thesis: for a, b being Element of K holds <*a*> "*" <*b*> = a * b let a, b be Element of K; ::_thesis: <*a*> "*" <*b*> = a * b set p = <*a*>; set q = <*b*>; set m = mlt (<*a*>,<*b*>); mlt (<*a*>,<*b*>) = <*(a * b)*> by FINSEQ_2:74; then mlt (<*a*>,<*b*>) = 1 |-> (a * b) by FINSEQ_2:59; hence <*a*> "*" <*b*> = a * b by FINSOP_1:16; ::_thesis: verum end; theorem :: FVSUM_1:89 for K being non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2) proof let K be non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr ; ::_thesis: for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2) let a1, a2, b1, b2 be Element of K; ::_thesis: <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2) set p = <*a1,a2*>; set q = <*b1,b2*>; the addF of K $$ (mlt (<*a1,a2*>,<*b1,b2*>)) = the addF of K $$ <*(a1 * b1),(a2 * b2)*> by Lm5 .= (a1 * b1) + (a2 * b2) by FINSOP_1:12 ; hence <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2) ; ::_thesis: verum end; theorem :: FVSUM_1:90 for K being non empty associative commutative well-unital doubleLoopStr for p, q being FinSequence of the carrier of K holds p "*" q = q "*" p by Th64;