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


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

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

theorem Th3: :: FVSUM_1:3
for K being non empty commutative multMagma holds the multF of K is commutative
proof 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 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 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 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 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 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 end;

definition
let K be non empty multMagma ;
let a be Element of K;
func a 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 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 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 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 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 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 end;

::
:: 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;
func p1 + 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 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 Nat;
let K be non empty addLoopStr ;
let R1, R2 be Element of i -tuples_on the carrier of K;
:: original: +
redefine func R1 + 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 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 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 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 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 end;

theorem Th21: :: FVSUM_1:21
for i being 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 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 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 end;

definition
let i be 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 i, j being 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 end;

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

theorem Th25: :: FVSUM_1:25
for i being Nat
for K being non empty addLoopStr
for a being Element of K holds - (i |-> a) = i |-> (- a)
proof end;

Lm3: for i being 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 end;

theorem Th26: :: FVSUM_1:26
for i being 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 end;

theorem Th27: :: FVSUM_1:27
for i being 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 end;

theorem Th28: :: FVSUM_1:28
for i being 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 end;

theorem :: FVSUM_1:29
for i being 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 end;

Lm4: for i being Nat
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R, R1, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2

proof end;

theorem :: FVSUM_1:30
for i being 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 end;

theorem Th31: :: FVSUM_1:31
for i being 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 end;

definition
let K be non empty addLoopStr ;
let p1, p2 be FinSequence of the carrier of K;
func p1 - 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 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 end;

definition
let i be Nat;
let K be non empty addLoopStr ;
let R1, R2 be Element of i -tuples_on the carrier of K;
:: original: -
redefine func R1 - 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 i, j being 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 end;

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

theorem :: FVSUM_1:35
for i being Nat
for K being non empty addLoopStr
for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)
proof end;

theorem :: FVSUM_1:36
for i being 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 end;

theorem :: FVSUM_1:37
for i being 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 end;

theorem :: FVSUM_1:38
for i being 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 end;

theorem :: FVSUM_1:39
for i being 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 end;

theorem Th40: :: FVSUM_1:40
for i being 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 end;

theorem Th41: :: FVSUM_1:41
for i being 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 end;

theorem :: FVSUM_1:42
for i being 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 end;

theorem :: FVSUM_1:43
for i being 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 end;

theorem Th44: :: FVSUM_1:44
for i being 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 end;

theorem :: FVSUM_1:45
for i being 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 end;

theorem :: FVSUM_1:46
for i being Nat
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R, R1 being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R
proof end;

theorem :: FVSUM_1:47
for i being Nat
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R, R1 being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R
proof 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 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;
func a * 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 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 end;

definition
let i be 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 func a * 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 i, j being Nat
for K being non empty multMagma
for a, a9 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 end;

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

theorem Th53: :: FVSUM_1:53
for i being Nat
for K being non empty multMagma
for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)
proof end;

theorem :: FVSUM_1:54
for i being 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 end;

theorem :: FVSUM_1:55
for i being 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 end;

theorem :: FVSUM_1:56
for i being 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 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 end;

theorem :: FVSUM_1:58
for i being Nat
for K being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)
proof end;

theorem :: FVSUM_1:59
for i being Nat
for K being non empty right_complementable commutative distributive left_unital add-associative right_zeroed doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R
proof 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 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 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 i, j being 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 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 end;

theorem :: FVSUM_1:63
for i being 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 end;

theorem :: FVSUM_1:65
for i being 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 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 end;

theorem :: FVSUM_1:67
for i being 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 end;

theorem :: FVSUM_1:68
for i being 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 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 end;

theorem :: FVSUM_1:70
for i being 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;

::
::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 & b1 is right_zeroed holds
b1 is left_zeroed
proof 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 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 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 end;

theorem :: FVSUM_1:73
for K being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of K
for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p)
proof 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 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 end;

theorem :: FVSUM_1:76
for i being 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 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 end;

Lm6: for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K
proof 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 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 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 end;

theorem :: FVSUM_1:81
for i being Nat
for K being non empty associative commutative well-unital doubleLoopStr holds Product (i |-> (1_ K)) = 1_ K
proof end;

theorem :: FVSUM_1:82
for K being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being FinSequence of the carrier of K holds
( ex k being Nat st
( k in dom p & p . k = 0. K ) iff Product p = 0. K )
proof end;

theorem :: FVSUM_1:83
for i, j being 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 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 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 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 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 end;

definition
let K be non empty doubleLoopStr ;
let p, q be FinSequence of the carrier of K;
func p "*" 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 left_unital Abelian add-associative right_zeroed doubleLoopStr
for a, b being Element of K holds <*a*> "*" <*b*> = a * b
proof end;

theorem :: FVSUM_1:89
for K being non empty right_complementable associative commutative left_unital Abelian add-associative right_zeroed doubleLoopStr
for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)
proof 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;