:: Sum and Product of Finite Sequences of Elements of a Field
:: by Katarzyna Zawadzka
::
:: Received December 29, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

theorem Th1: :: FVSUM_1:1
for K being non empty Abelian addLoopStr holds the addF of K is commutative
proofend;

theorem Th2: :: FVSUM_1:2
for K being non empty add-associative addLoopStr holds the addF of K is associative
proofend;

theorem Th3: :: FVSUM_1:3
for K being non empty commutative multMagma holds the multF of K is commutative
proofend;

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
proofend;

theorem Th5: :: FVSUM_1:5
for K being non empty commutative left_unital multLoopStr holds the_unity_wrt the multF of K = 1. K
proofend;

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
proofend;

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
proofend;

theorem Th8: :: FVSUM_1:8
for K being non empty left_zeroed right_zeroed addLoopStr holds the addF of K is having_a_unity
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

begin

::
:: Some Operations on the i-tuples on Element of K
::
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
proofend;

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
proofend;

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 &amp; R = (i |-> (0. K)) + R )
proofend;

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) &amp; a = p . i holds
(- p) . i = - a
proofend;

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 &amp; a = R . j holds
(- R) . j = - a
proofend;

theorem :: FVSUM_1:24
for K being non empty addLoopStr
for a being Element of K holds - <*a*> = <*(- a)*>
proofend;

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)
proofend;

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)
proofend;

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) &amp; (- R) + R = i |-> (0. K) )
proofend;

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 &amp; R2 = - R1 )
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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) &amp; a1 = p1 . i &amp; a2 = p2 . i holds
(p1 - p2) . i = a1 - a2
proofend;

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 &amp; a1 = R1 . j &amp; a2 = R2 . j holds
(R1 - R2) . j = a1 - a2
proofend;

theorem :: FVSUM_1:34
for K being non empty addLoopStr
for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*>
proofend;

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)
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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) &amp; a9 = p . i holds
(a * p) . i = a * a9
proofend;

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 &amp; a9 = R . j holds
(a * R) . j = a * a9
proofend;

theorem :: FVSUM_1:52
for K being non empty multMagma
for a, a1 being Element of K holds a * <*a1*> = <*(a * a1)*>
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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
proofend;

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)) &amp; a1 = p1 . i &amp; 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 &amp; a1 = R1 . j &amp; a2 = R2 . j holds
(mlt (R1,R2)) . j = a1 * a2
proofend;

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)*>
proofend;

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)
proofend;

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 &amp; mlt (R,(i |-> a)) = a * R )
proofend;

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)
proofend;

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) &amp; a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )
proofend;

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

::
::The Sum of Finite Number of Elements
::
registration
cluster non empty Abelian right_zeroed  ->  non empty left_zeroed for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is Abelian &amp; b1 is right_zeroed holds
b1 is left_zeroed
proofend;
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 )
proofend;
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
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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)
proofend;

begin

Lm6:  for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K
proofend;

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)
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; p . k = 0. K ) iff Product p = 0. K )
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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;