:: FVSUM_1 semantic presentation

theorem :: FVSUM_1:1

canceled;

theorem Th2: :: FVSUM_1:2

for K being non empty Abelian LoopStr holds the add of K is commutative

proof end;

theorem Th3: :: FVSUM_1:3

for K being non empty add-associative LoopStr holds the add of K is associative

proof end;

theorem Th4: :: FVSUM_1:4

for K being non empty commutative HGrStr holds the mult of K is commutative

proof end;

theorem :: FVSUM_1:5

canceled;

theorem Th6: :: FVSUM_1:6

for K being non empty commutative left_unital doubleLoopStr holds 1. K is_a_unity_wrt the mult of K

proof end;

theorem Th7: :: FVSUM_1:7

for K being non empty commutative left_unital doubleLoopStr holds the_unity_wrt the mult of K = 1. K

proof end;

theorem Th8: :: FVSUM_1:8

for K being non empty right_zeroed left_zeroed LoopStr holds 0. K is_a_unity_wrt the add of K

proof end;

theorem Th9: :: FVSUM_1:9

for K being non empty right_zeroed left_zeroed LoopStr holds the_unity_wrt the add of K = 0. K

proof end;

theorem Th10: :: FVSUM_1:10

for K being non empty right_zeroed left_zeroed LoopStr holds the add of K has_a_unity

proof end;

theorem Th11: :: FVSUM_1:11

for K being non empty commutative left_unital doubleLoopStr holds the mult of K has_a_unity

proof end;

theorem Th12: :: FVSUM_1:12

for K being non empty distributive doubleLoopStr holds the mult of K is_distributive_wrt the add of K

proof end;

definition

let K be non empty HGrStr ;
let a be Element of K;
func a multfield -> UnOp of the carrier of K equals :: FVSUM_1:def 1
the mult of K [;] a,(id the carrier of K);
coherence ;

end;

:: deftheorem defines multfield FVSUM_1:def 1 :

definition

let K be non empty LoopStr ;
func diffield K -> BinOp of the carrier of K equals :: FVSUM_1:def 2
the add of K * (id the carrier of K),(comp K);
correctness ;

end;

:: deftheorem defines diffield FVSUM_1:def 2 :

theorem :: FVSUM_1:13

canceled;

theorem Th14: :: FVSUM_1:14

for K being non empty LoopStr
for a1, a2 being Element of K holds (diffield K) . a1,a2 = a1 - a2

proof end;

Lm1: for K being non empty HGrStr
for a, b being Element of K holds (the mult of K [;] b,(id the carrier of K)) . a = b * a

proof end;

theorem Th15: :: FVSUM_1:15

for K being non empty distributive doubleLoopStr
for a being Element of K holds a multfield is_distributive_wrt the add of K

proof end;

theorem Th16: :: FVSUM_1:16

for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr holds comp K is_an_inverseOp_wrt the add of K

proof end;

theorem Th17: :: FVSUM_1:17

for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr holds the add of K has_an_inverseOp

proof end;

theorem Th18: :: FVSUM_1:18

for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr holds the_inverseOp_wrt the add of K = comp K

proof end;

theorem :: FVSUM_1:19

for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds comp K is_distributive_wrt the add of K

proof end;

definition

let K be non empty LoopStr ;
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 add of K .: p1,p2;
correctness ;

end;

:: deftheorem defines + FVSUM_1:def 3 :

theorem :: FVSUM_1:20

canceled;

theorem Th21: :: FVSUM_1:21

for K being non empty LoopStr
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

proof end;

definition

let i be Nat;
let K be non empty LoopStr ;
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 by FINSEQ_2:140;

end;

theorem :: FVSUM_1:22

for i, j being Nat
for K being non empty LoopStr
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:23

for K being non empty LoopStr
for p being FinSequence of the carrier of K holds
( (<*> the carrier of K) + p = <*> the carrier of K & p + (<*> the carrier of K) = <*> the carrier of K ) by FINSEQ_2:87;

theorem :: FVSUM_1:24

for K being non empty LoopStr
for a1, a2 being Element of K holds <*a1*> + <*a2*> = <*(a1 + a2)*>

proof end;

theorem :: FVSUM_1:25

for i being Nat
for K being non empty LoopStr
for a1, a2 being Element of K holds (i |-> a1) + (i |-> a2) = i |-> (a1 + a2)

proof end;

theorem Th26: :: FVSUM_1:26

for i being Nat
for K being non empty Abelian LoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds R1 + R2 = R2 + R1

proof end;

theorem Th27: :: FVSUM_1:27

for i being Nat
for K being non empty add-associative LoopStr
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 + R3) = (R1 + R2) + R3

proof end;

Lm2: for i being Nat
for K being non empty right_zeroed left_zeroed LoopStr
for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R

proof end;

theorem Th28: :: FVSUM_1:28

for i being Nat
for K being non empty Abelian right_zeroed left_zeroed LoopStr
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 LoopStr ;
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 ;

end;

:: deftheorem defines - FVSUM_1:def 4 :

theorem :: FVSUM_1:29

canceled;

theorem Th30: :: FVSUM_1:30

for i being Nat
for K being non empty LoopStr
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 LoopStr ;
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 by FINSEQ_2:133;

end;

theorem :: FVSUM_1:31

for j, i being Nat
for K being non empty LoopStr
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:32

for K being non empty LoopStr holds - (<*> the carrier of K) = <*> the carrier of K by FINSEQ_2:38;

theorem :: FVSUM_1:33

for K being non empty LoopStr
for a being Element of K holds - <*a*> = <*(- a)*>

proof end;

theorem Th34: :: FVSUM_1:34

for i being Nat
for K being non empty LoopStr
for a being Element of K holds - (i |-> a) = i |-> (- a)

proof end;

Lm3: for i being Nat
for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)

proof end;

theorem Th35: :: FVSUM_1:35

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
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 Th36: :: FVSUM_1:36

for i being Nat
for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
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 Th37: :: FVSUM_1:37

for i being Nat
for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for R being Element of i -tuples_on the carrier of K holds - (- R) = R

proof end;

theorem :: FVSUM_1:38

for i being Nat
for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
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 add-associative right_zeroed right_complementable left_zeroed LoopStr
for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2

proof end;

theorem :: FVSUM_1:39

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
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 Th40: :: FVSUM_1:40

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
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 LoopStr ;
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 ;

end;

:: deftheorem defines - FVSUM_1:def 5 :

theorem :: FVSUM_1:41

canceled;

theorem Th42: :: FVSUM_1:42

for i being Nat
for K being non empty LoopStr
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 LoopStr ;
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 by FINSEQ_2:140;

end;

theorem :: FVSUM_1:43

for j, i being Nat
for K being non empty LoopStr
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:44

for K being non empty LoopStr
for p1 being FinSequence of the carrier of K holds
( (<*> the carrier of K) - p1 = <*> the carrier of K & p1 - (<*> the carrier of K) = <*> the carrier of K ) by FINSEQ_2:87;

theorem :: FVSUM_1:45

for K being non empty LoopStr
for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*>

proof end;

theorem :: FVSUM_1:46

for i being Nat
for K being non empty LoopStr
for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)

proof end;

theorem Th47: :: FVSUM_1:47

for i being Nat
for K being non empty LoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - R2 = R1 + (- R2) by FINSEQOP:89;

theorem :: FVSUM_1:48

for i being Nat
for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R

proof end;

theorem :: FVSUM_1:49

for i being Nat
for K being non empty Abelian right_zeroed left_zeroed LoopStr
for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R

proof end;

theorem :: FVSUM_1:50

for i being Nat
for K being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2

proof end;

theorem :: FVSUM_1:51

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1

proof end;

theorem Th52: :: FVSUM_1:52

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2

proof end;

theorem Th53: :: FVSUM_1:53

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K)

proof end;

theorem :: FVSUM_1:54

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
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:55

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3)

proof end;

theorem Th56: :: FVSUM_1:56

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
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:57

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
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:58

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R

proof end;

theorem :: FVSUM_1:59

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R

proof end;

theorem Th60: :: FVSUM_1:60

for K being non empty HGrStr
for a, b being Element of K holds (the mult of K [;] a,(id the carrier of K)) . b = a * b

proof end;

theorem :: FVSUM_1:61

for K being non empty HGrStr
for a, b being Element of K holds (a multfield ) . b = a * b by Th60;

definition

let K be non empty HGrStr ;
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 ;

end;

:: deftheorem defines * FVSUM_1:def 6 :

theorem Th62: :: FVSUM_1:62

for i being Nat
for K being non empty HGrStr
for a, a' being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a' = p . i holds
(a * p) . i = a * a'

proof end;

definition

let i be Nat;
let K be non empty HGrStr ;
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 by FINSEQ_2:133;

end;

theorem :: FVSUM_1:63

for j, i being Nat
for K being non empty HGrStr
for a', 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
(a * R) . j = a * a'

proof end;

theorem :: FVSUM_1:64

for K being non empty HGrStr
for a being Element of K holds a * (<*> the carrier of K) = <*> the carrier of K by FINSEQ_2:38;

theorem :: FVSUM_1:65

for K being non empty HGrStr
for a, a1 being Element of K holds a * <*a1*> = <*(a * a1)*>

proof end;

theorem Th66: :: FVSUM_1:66

for i being Nat
for K being non empty HGrStr
for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)

proof end;

theorem :: FVSUM_1:67

for i being Nat
for K being non empty associative HGrStr
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:68

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:69

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)

proof end;

theorem :: FVSUM_1:70

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:71

for i being Nat
for K being non empty add-associative right_zeroed right_complementable distributive 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:72

for i being Nat
for K being non empty add-associative right_zeroed right_complementable commutative distributive left_unital 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 HGrStr ;
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 mult of M .: p1,p2;
correctness ;

end;

:: deftheorem defines mlt FVSUM_1:def 7 :

theorem Th73: :: FVSUM_1:73

for i being Nat
for K being non empty HGrStr
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

proof end;

definition

let i be Nat;
let K be non empty HGrStr ;
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 by FINSEQ_2:140;

end;

theorem :: FVSUM_1:74

for j, i being Nat
for K being non empty HGrStr
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:75

for K being non empty HGrStr
for p being FinSequence of the carrier of K holds
( mlt (<*> the carrier of K),p = <*> the carrier of K & mlt p,(<*> the carrier of K) = <*> the carrier of K ) by FINSEQ_2:87;

theorem Th76: :: FVSUM_1:76

for K being non empty HGrStr
for a1, a2 being Element of K holds mlt <*a1*>,<*a2*> = <*(a1 * a2)*>

proof end;

Lm5: for i being Nat
for K being non empty HGrStr
for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K holds mlt (R1 ^ <*a1*>),(R2 ^ <*a2*>) = (mlt R1,R2) ^ <*(a1 * a2)*>

proof end;

Lm6: for K being non empty HGrStr
for a1, a2, b1, b2 being Element of K holds mlt <*a1,a2*>,<*b1,b2*> = <*(a1 * b1),(a2 * b2)*>

proof end;

theorem Th77: :: FVSUM_1:77

for i being Nat
for K being non empty commutative HGrStr
for R1, R2 being Element of i -tuples_on the carrier of K holds mlt R1,R2 = mlt R2,R1

proof end;

theorem Th78: :: FVSUM_1:78

for K being non empty commutative HGrStr
for p, q being FinSequence of the carrier of K holds mlt p,q = mlt q,p

proof end;

theorem :: FVSUM_1:79

for i being Nat
for K being non empty associative HGrStr
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

proof end;

theorem Th80: :: FVSUM_1:80

for i being Nat
for K being non empty associative commutative HGrStr
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:81

for i being Nat
for K being non empty associative commutative HGrStr
for a1, a2 being Element of K holds mlt (i |-> a1),(i |-> a2) = i |-> (a1 * a2)

proof end;

theorem Th82: :: FVSUM_1:82

for i being Nat
for K being non empty associative HGrStr
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

proof end;

theorem :: FVSUM_1:83

for i being Nat
for K being non empty associative commutative HGrStr
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:84

for i being Nat
for K being non empty associative commutative HGrStr
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 Th80;

registration

cluster non empty Abelian right_zeroed -> non empty left_zeroed LoopStr ;
coherence

proof end;

end;

definition

let K be non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
let p be FinSequence of the carrier of K;
redefine func Sum p equals :: FVSUM_1:def 8
the add of K $$ p;
compatibility

proof end;

end;

:: deftheorem defines Sum FVSUM_1:def 8 :

theorem :: FVSUM_1:85

canceled;

theorem :: FVSUM_1:86

canceled;

theorem :: FVSUM_1:87

for K being non empty add-associative right_zeroed right_complementable LoopStr
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:88

canceled;

theorem :: FVSUM_1:89

for K being non empty add-associative right_zeroed right_complementable LoopStr
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:90

canceled;

theorem :: FVSUM_1:91

canceled;

theorem :: FVSUM_1:92

for K being non empty Abelian add-associative right_zeroed right_complementable 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 end;

theorem :: FVSUM_1:93

for K being non empty LoopStr
for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K

proof end;

theorem :: FVSUM_1:94

for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p)

proof end;

theorem :: FVSUM_1:95

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 + R2) = (Sum R1) + (Sum R2)

proof end;

theorem :: FVSUM_1:96

for i being Nat
for K being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

proof end;

definition

let K be non empty HGrStr ;
let p be FinSequence of the carrier of K;
func Product p -> Element of K equals :: FVSUM_1:def 9
the mult of K $$ p;
coherence ;

end;

:: deftheorem defines Product FVSUM_1:def 9 :

theorem :: FVSUM_1:97

canceled;

theorem Th98: :: FVSUM_1:98

for K being non empty commutative left_unital doubleLoopStr holds Product (<*> the carrier of K) = 1. K

proof end;

theorem Th99: :: FVSUM_1:99

for K being non empty HGrStr
for a being Element of K holds Product <*a*> = a by FINSOP_1:12;

theorem Th100: :: FVSUM_1:100

for K being non empty commutative left_unital doubleLoopStr
for a being Element of K
for p being FinSequence of the carrier of K holds Product (p ^ <*a*>) = (Product p) * a

proof end;

theorem Th101: :: FVSUM_1:101

for K being non empty associative commutative left_unital doubleLoopStr
for p1, p2 being FinSequence of the carrier of K holds Product (p1 ^ p2) = (Product p1) * (Product p2)

proof end;

theorem :: FVSUM_1:102

for K being non empty associative commutative left_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 Th103: :: FVSUM_1:103

for K being non empty associative commutative left_unital doubleLoopStr
for a1, a2 being Element of K holds Product <*a1,a2*> = a1 * a2

proof end;

theorem :: FVSUM_1:104

for K being non empty associative commutative left_unital doubleLoopStr
for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3

proof end;

theorem :: FVSUM_1:105

for K being non empty associative commutative left_unital doubleLoopStr
for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K

proof end;

theorem :: FVSUM_1:106

for i being Nat
for K being non empty associative commutative left_unital doubleLoopStr holds Product (i |-> (1. K)) = 1. K

proof end;

theorem :: FVSUM_1:107

for K being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated 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:108

for i, j being Nat
for K being non empty associative commutative left_unital doubleLoopStr
for a being Element of K holds Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a))

proof end;

theorem :: FVSUM_1:109

for i, j being Nat
for K being non empty associative commutative left_unital doubleLoopStr
for a being Element of K holds Product ((i * j) |-> a) = Product (j |-> (Product (i |-> a)))

proof end;

theorem :: FVSUM_1:110

for i being Nat
for K being non empty associative commutative left_unital doubleLoopStr
for a1, a2 being Element of K holds Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2))

proof end;

theorem Th111: :: FVSUM_1:111

for i being Nat
for K being non empty associative commutative left_unital doubleLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Product (mlt R1,R2) = (Product R1) * (Product R2)

proof end;

theorem :: FVSUM_1:112

for i being Nat
for K being non empty associative commutative left_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 10
Sum (mlt p,q);
correctness ;

end;

:: deftheorem defines "*" FVSUM_1:def 10 :

theorem :: FVSUM_1:113

for K being non empty Abelian add-associative right_zeroed right_complementable associative commutative left_unital doubleLoopStr
for a, b being Element of K holds <*a*> "*" <*b*> = a * b

proof end;

theorem :: FVSUM_1:114

for K being non empty Abelian add-associative right_zeroed right_complementable associative commutative left_unital doubleLoopStr
for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)

proof end;

theorem :: FVSUM_1:115

for K being non empty associative commutative left_unital doubleLoopStr
for p, q being FinSequence of the carrier of K holds p "*" q = q "*" p by Th78;