:: 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 b₁ being non empty addLoopStr st b₁ is Abelian & b₁ is right_zeroed holds
b₁ 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 b₁ being Element of the carrier of K holds
( b₁ = Sum p iff b₁ = 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;