:: FVSUM_1 semantic presentation

theorem Th1: :: FVSUM_1:1

canceled;

theorem Th2: :: FVSUM_1:2

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

proof end;

theorem Th3: :: FVSUM_1:3

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

proof end;

theorem Th4: :: FVSUM_1:4

for b₁ being non empty commutative HGrStr holds the mult of b₁ is commutative

proof end;

theorem Th5: :: FVSUM_1:5

canceled;

theorem Th6: :: FVSUM_1:6

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

proof end;

theorem Th7: :: FVSUM_1:7

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

proof end;

theorem Th8: :: FVSUM_1:8

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

proof end;

theorem Th9: :: FVSUM_1:9

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

proof end;

theorem Th10: :: FVSUM_1:10

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

proof end;

theorem Th11: :: FVSUM_1:11

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

proof end;

theorem Th12: :: FVSUM_1:12

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

proof end;

definition

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

end;

:: deftheorem Def1 defines multfield FVSUM_1:def 1 :

definition

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

end;

:: deftheorem Def2 defines diffield FVSUM_1:def 2 :

theorem Th13: :: FVSUM_1:13

canceled;

theorem Th14: :: FVSUM_1:14

for b₁ being non empty LoopStr
for b₂, b₃ being Element of b₁ holds (diffield b₁) . b₂,b₃ = b₂ - b₃

proof end;

Lemma12: for b₁ being non empty HGrStr
for b₂, b₃ being Element of b₁ holds (the mult of b₁ [;] b₃,(id the carrier of b₁)) . b₂ = b₃ * b₂

proof end;

theorem Th15: :: FVSUM_1:15

for b₁ being non empty distributive doubleLoopStr
for b₂ being Element of b₁ holds b₂ multfield is_distributive_wrt the add of b₁

proof end;

theorem Th16: :: FVSUM_1:16

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

proof end;

theorem Th17: :: FVSUM_1:17

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

proof end;

theorem Th18: :: FVSUM_1:18

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

proof end;

theorem Th19: :: FVSUM_1:19

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

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be FinSequence of the carrier of c₁;
func c₂ + c₃ -> FinSequence of the carrier of a₁ equals :: FVSUM_1:def 3
the add of a₁ .: a₂,a₃;
correctness ;

end;

:: deftheorem Def3 defines + FVSUM_1:def 3 :

theorem Th20: :: FVSUM_1:20

canceled;

theorem Th21: :: FVSUM_1:21

for b₁ being non empty LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁
for b₄, b₅ being Element of b₁
for b₆ being Nat st b₆ in dom (b₂ + b₃) & b₄ = b₂ . b₆ & b₅ = b₃ . b₆ holds
(b₂ + b₃) . b₆ = b₄ + b₅

proof end;

definition

let c₁ be Nat;
let c₂ be non empty LoopStr ;
let c₃, c₄ be Element of c₁ -tuples_on the carrier of c₂;
redefine func + as c₃ + c₄ -> Element of a₁ -tuples_on the carrier of a₂;
coherence by FINSEQ_2:140;

end;

theorem Th22: :: FVSUM_1:22

for b₁, b₂ being Nat
for b₃ being non empty LoopStr
for b₄, b₅ being Element of b₃
for b₆, b₇ being Element of b₁ -tuples_on the carrier of b₃ st b₂ in Seg b₁ & b₄ = b₆ . b₂ & b₅ = b₇ . b₂ holds
(b₆ + b₇) . b₂ = b₄ + b₅

proof end;

theorem Th23: :: FVSUM_1:23

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

theorem Th24: :: FVSUM_1:24

for b₁ being non empty LoopStr
for b₂, b₃ being Element of b₁ holds <*b₂*> + <*b₃*> = <*(b₂ + b₃)*>

proof end;

theorem Th25: :: FVSUM_1:25

for b₁ being Nat
for b₂ being non empty LoopStr
for b₃, b₄ being Element of b₂ holds (b₁ |-> b₃) + (b₁ |-> b₄) = b₁ |-> (b₃ + b₄)

proof end;

theorem Th26: :: FVSUM_1:26

for b₁ being Nat
for b₂ being non empty Abelian LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ + b₄ = b₄ + b₃

proof end;

theorem Th27: :: FVSUM_1:27

for b₁ being Nat
for b₂ being non empty add-associative LoopStr
for b₃, b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ + (b₄ + b₅) = (b₃ + b₄) + b₅

proof end;

Lemma20: for b₁ being Nat
for b₂ being non empty right_zeroed left_zeroed LoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ + (b₁ |-> (0. b₂)) = b₃

proof end;

theorem Th28: :: FVSUM_1:28

for b₁ being Nat
for b₂ being non empty Abelian right_zeroed left_zeroed LoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds
( b₃ + (b₁ |-> (0. b₂)) = b₃ & b₃ = (b₁ |-> (0. b₂)) + b₃ )

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be FinSequence of the carrier of c₁;
func - c₂ -> FinSequence of the carrier of a₁ equals :: FVSUM_1:def 4
(comp a₁) * a₂;
correctness ;

end;

:: deftheorem Def4 defines - FVSUM_1:def 4 :

theorem Th29: :: FVSUM_1:29

canceled;

theorem Th30: :: FVSUM_1:30

for b₁ being Nat
for b₂ being non empty LoopStr
for b₃ being Element of b₂
for b₄ being FinSequence of the carrier of b₂ st b₁ in dom (- b₄) & b₃ = b₄ . b₁ holds
(- b₄) . b₁ = - b₃

proof end;

definition

let c₁ be Nat;
let c₂ be non empty LoopStr ;
let c₃ be Element of c₁ -tuples_on the carrier of c₂;
redefine func - as - c₃ -> Element of a₁ -tuples_on the carrier of a₂;
coherence by FINSEQ_2:133;

end;

theorem Th31: :: FVSUM_1:31

for b₁, b₂ being Nat
for b₃ being non empty LoopStr
for b₄ being Element of b₃
for b₅ being Element of b₂ -tuples_on the carrier of b₃ st b₁ in Seg b₂ & b₄ = b₅ . b₁ holds
(- b₅) . b₁ = - b₄

proof end;

theorem Th32: :: FVSUM_1:32

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

theorem Th33: :: FVSUM_1:33

for b₁ being non empty LoopStr
for b₂ being Element of b₁ holds - <*b₂*> = <*(- b₂)*>

proof end;

theorem Th34: :: FVSUM_1:34

for b₁ being Nat
for b₂ being non empty LoopStr
for b₃ being Element of b₂ holds - (b₁ |-> b₃) = b₁ |-> (- b₃)

proof end;

Lemma24: for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ + (- b₃) = b₁ |-> (0. b₂)

proof end;

theorem Th35: :: FVSUM_1:35

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds
( b₃ + (- b₃) = b₁ |-> (0. b₂) & (- b₃) + b₃ = b₁ |-> (0. b₂) )

proof end;

theorem Th36: :: FVSUM_1:36

for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ st b₃ + b₄ = b₁ |-> (0. b₂) holds
( b₃ = - b₄ & b₄ = - b₃ )

proof end;

theorem Th37: :: FVSUM_1:37

for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds - (- b₃) = b₃

proof end;

theorem Th38: :: FVSUM_1:38

for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ st - b₃ = - b₄ holds
b₃ = b₄

proof end;

Lemma28: for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for b₃, b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ st b₃ + b₄ = b₅ + b₄ holds
b₃ = b₅

proof end;

theorem Th39: :: FVSUM_1:39

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ st ( b₄ + b₃ = b₅ + b₃ or b₄ + b₃ = b₃ + b₅ ) holds
b₄ = b₅

proof end;

theorem Th40: :: FVSUM_1:40

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds - (b₃ + b₄) = (- b₃) + (- b₄)

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be FinSequence of the carrier of c₁;
func c₂ - c₃ -> FinSequence of the carrier of a₁ equals :: FVSUM_1:def 5
(diffield a₁) .: a₂,a₃;
correctness ;

end;

:: deftheorem Def5 defines - FVSUM_1:def 5 :

theorem Th41: :: FVSUM_1:41

canceled;

theorem Th42: :: FVSUM_1:42

for b₁ being Nat
for b₂ being non empty LoopStr
for b₃, b₄ being Element of b₂
for b₅, b₆ being FinSequence of the carrier of b₂ st b₁ in dom (b₅ - b₆) & b₃ = b₅ . b₁ & b₄ = b₆ . b₁ holds
(b₅ - b₆) . b₁ = b₃ - b₄

proof end;

definition

let c₁ be Nat;
let c₂ be non empty LoopStr ;
let c₃, c₄ be Element of c₁ -tuples_on the carrier of c₂;
redefine func - as c₃ - c₄ -> Element of a₁ -tuples_on the carrier of a₂;
coherence by FINSEQ_2:140;

end;

theorem Th43: :: FVSUM_1:43

for b₁, b₂ being Nat
for b₃ being non empty LoopStr
for b₄, b₅ being Element of b₃
for b₆, b₇ being Element of b₂ -tuples_on the carrier of b₃ st b₁ in Seg b₂ & b₄ = b₆ . b₁ & b₅ = b₇ . b₁ holds
(b₆ - b₇) . b₁ = b₄ - b₅

proof end;

theorem Th44: :: FVSUM_1:44

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

theorem Th45: :: FVSUM_1:45

for b₁ being non empty LoopStr
for b₂, b₃ being Element of b₁ holds <*b₂*> - <*b₃*> = <*(b₂ - b₃)*>

proof end;

theorem Th46: :: FVSUM_1:46

for b₁ being Nat
for b₂ being non empty LoopStr
for b₃, b₄ being Element of b₂ holds (b₁ |-> b₃) - (b₁ |-> b₄) = b₁ |-> (b₃ - b₄)

proof end;

theorem Th47: :: FVSUM_1:47

for b₁ being Nat
for b₂ being non empty LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ - b₄ = b₃ + (- b₄) by FINSEQOP:89;

theorem Th48: :: FVSUM_1:48

for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ - (b₁ |-> (0. b₂)) = b₃

proof end;

theorem Th49: :: FVSUM_1:49

for b₁ being Nat
for b₂ being non empty Abelian right_zeroed left_zeroed LoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds (b₁ |-> (0. b₂)) - b₃ = - b₃

proof end;

theorem Th50: :: FVSUM_1:50

for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable left_zeroed LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ - (- b₄) = b₃ + b₄

proof end;

theorem Th51: :: FVSUM_1:51

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds - (b₃ - b₄) = b₄ - b₃

proof end;

theorem Th52: :: FVSUM_1:52

proof end;

theorem Th53: :: FVSUM_1:53

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ - b₃ = b₁ |-> (0. b₂)

proof end;

theorem Th54: :: FVSUM_1:54

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ st b₃ - b₄ = b₁ |-> (0. b₂) holds
b₃ = b₄

proof end;

theorem Th55: :: FVSUM_1:55

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ holds (b₃ - b₄) - b₅ = b₃ - (b₄ + b₅)

proof end;

theorem Th56: :: FVSUM_1:56

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ + (b₄ - b₅) = (b₃ + b₄) - b₅

proof end;

theorem Th57: :: FVSUM_1:57

proof end;

theorem Th58: :: FVSUM_1:58

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ = (b₃ + b₄) - b₄

proof end;

theorem Th59: :: FVSUM_1:59

proof end;

theorem Th60: :: FVSUM_1:60

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

proof end;

theorem Th61: :: FVSUM_1:61

for b₁ being non empty HGrStr
for b₂, b₃ being Element of b₁ holds (b₂ multfield ) . b₃ = b₂ * b₃ by Th60;

definition

let c₁ be non empty HGrStr ;
let c₂ be FinSequence of the carrier of c₁;
let c₃ be Element of c₁;
func c₃ * c₂ -> FinSequence of the carrier of a₁ equals :: FVSUM_1:def 6
(a₃ multfield ) * a₂;
correctness ;

end;

:: deftheorem Def6 defines * FVSUM_1:def 6 :

theorem Th62: :: FVSUM_1:62

for b₁ being Nat
for b₂ being non empty HGrStr
for b₃, b₄ being Element of b₂
for b₅ being FinSequence of the carrier of b₂ st b₁ in dom (b₃ * b₅) & b₄ = b₅ . b₁ holds
(b₃ * b₅) . b₁ = b₃ * b₄

proof end;

definition

let c₁ be Nat;
let c₂ be non empty HGrStr ;
let c₃ be Element of c₁ -tuples_on the carrier of c₂;
let c₄ be Element of c₂;
redefine func * as c₄ * c₃ -> Element of a₁ -tuples_on the carrier of a₂;
coherence by FINSEQ_2:133;

end;

theorem Th63: :: FVSUM_1:63

for b₁, b₂ being Nat
for b₃ being non empty HGrStr
for b₄, b₅ being Element of b₃
for b₆ being Element of b₂ -tuples_on the carrier of b₃ st b₁ in Seg b₂ & b₄ = b₆ . b₁ holds
(b₅ * b₆) . b₁ = b₅ * b₄

proof end;

theorem Th64: :: FVSUM_1:64

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

theorem Th65: :: FVSUM_1:65

for b₁ being non empty HGrStr
for b₂, b₃ being Element of b₁ holds b₂ * <*b₃*> = <*(b₂ * b₃)*>

proof end;

theorem Th66: :: FVSUM_1:66

for b₁ being Nat
for b₂ being non empty HGrStr
for b₃, b₄ being Element of b₂ holds b₃ * (b₁ |-> b₄) = b₁ |-> (b₃ * b₄)

proof end;

theorem Th67: :: FVSUM_1:67

for b₁ being Nat
for b₂ being non empty associative HGrStr
for b₃, b₄ being Element of b₂
for b₅ being Element of b₁ -tuples_on the carrier of b₂ holds (b₃ * b₄) * b₅ = b₃ * (b₄ * b₅)

proof end;

theorem Th68: :: FVSUM_1:68

for b₁ being Nat
for b₂ being non empty distributive doubleLoopStr
for b₃, b₄ being Element of b₂
for b₅ being Element of b₁ -tuples_on the carrier of b₂ holds (b₃ + b₄) * b₅ = (b₃ * b₅) + (b₄ * b₅)

proof end;

theorem Th69: :: FVSUM_1:69

for b₁ being Nat
for b₂ being non empty distributive doubleLoopStr
for b₃ being Element of b₂
for b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ * (b₄ + b₅) = (b₃ * b₄) + (b₃ * b₅)

proof end;

theorem Th70: :: FVSUM_1:70

for b₁ being Nat
for b₂ being non empty commutative distributive left_unital doubleLoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds (1. b₂) * b₃ = b₃

proof end;

theorem Th71: :: FVSUM_1:71

for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds (0. b₂) * b₃ = b₁ |-> (0. b₂)

proof end;

theorem Th72: :: FVSUM_1:72

for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable commutative distributive left_unital doubleLoopStr
for b₃ being Element of b₁ -tuples_on the carrier of b₂ holds (- (1. b₂)) * b₃ = - b₃

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be FinSequence of the carrier of c₁;
func mlt c₂,c₃ -> FinSequence of the carrier of a₁ equals :: FVSUM_1:def 7
the mult of a₁ .: a₂,a₃;
correctness ;

end;

:: deftheorem Def7 defines mlt FVSUM_1:def 7 :

theorem Th73: :: FVSUM_1:73

for b₁ being Nat
for b₂ being non empty HGrStr
for b₃, b₄ being Element of b₂
for b₅, b₆ being FinSequence of the carrier of b₂ st b₁ in dom (mlt b₅,b₆) & b₃ = b₅ . b₁ & b₄ = b₆ . b₁ holds
(mlt b₅,b₆) . b₁ = b₃ * b₄

proof end;

definition

let c₁ be Nat;
let c₂ be non empty HGrStr ;
let c₃, c₄ be Element of c₁ -tuples_on the carrier of c₂;
redefine func mlt as mlt c₃,c₄ -> Element of a₁ -tuples_on the carrier of a₂;
coherence by FINSEQ_2:140;

end;

theorem Th74: :: FVSUM_1:74

for b₁, b₂ being Nat
for b₃ being non empty HGrStr
for b₄, b₅ being Element of b₃
for b₆, b₇ being Element of b₂ -tuples_on the carrier of b₃ st b₁ in Seg b₂ & b₄ = b₆ . b₁ & b₅ = b₇ . b₁ holds
(mlt b₆,b₇) . b₁ = b₄ * b₅

proof end;

theorem Th75: :: FVSUM_1:75

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

theorem Th76: :: FVSUM_1:76

for b₁ being non empty HGrStr
for b₂, b₃ being Element of b₁ holds mlt <*b₂*>,<*b₃*> = <*(b₂ * b₃)*>

proof end;

Lemma40: for b₁ being Nat
for b₂ being non empty HGrStr
for b₃, b₄ being Element of b₂
for b₅, b₆ being Element of b₁ -tuples_on the carrier of b₂ holds mlt (b₅ ^ <*b₃*>),(b₆ ^ <*b₄*>) = (mlt b₅,b₆) ^ <*(b₃ * b₄)*>

proof end;

Lemma41: for b₁ being non empty HGrStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds mlt <*b₂,b₃*>,<*b₄,b₅*> = <*(b₂ * b₄),(b₃ * b₅)*>

proof end;

theorem Th77: :: FVSUM_1:77

for b₁ being Nat
for b₂ being non empty commutative HGrStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds mlt b₃,b₄ = mlt b₄,b₃

proof end;

theorem Th78: :: FVSUM_1:78

for b₁ being non empty commutative HGrStr
for b₂, b₃ being FinSequence of the carrier of b₁ holds mlt b₂,b₃ = mlt b₃,b₂

proof end;

theorem Th79: :: FVSUM_1:79

for b₁ being Nat
for b₂ being non empty associative HGrStr
for b₃, b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ holds mlt b₃,(mlt b₄,b₅) = mlt (mlt b₃,b₄),b₅

proof end;

theorem Th80: :: FVSUM_1:80

for b₁ being Nat
for b₂ being non empty associative commutative HGrStr
for b₃ being Element of b₂
for b₄ being Element of b₁ -tuples_on the carrier of b₂ holds
( mlt (b₁ |-> b₃),b₄ = b₃ * b₄ & mlt b₄,(b₁ |-> b₃) = b₃ * b₄ )

proof end;

theorem Th81: :: FVSUM_1:81

for b₁ being Nat
for b₂ being non empty associative commutative HGrStr
for b₃, b₄ being Element of b₂ holds mlt (b₁ |-> b₃),(b₁ |-> b₄) = b₁ |-> (b₃ * b₄)

proof end;

theorem Th82: :: FVSUM_1:82

for b₁ being Nat
for b₂ being non empty associative HGrStr
for b₃ being Element of b₂
for b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ * (mlt b₄,b₅) = mlt (b₃ * b₄),b₅

proof end;

theorem Th83: :: FVSUM_1:83

for b₁ being Nat
for b₂ being non empty associative commutative HGrStr
for b₃ being Element of b₂
for b₄, b₅ being Element of b₁ -tuples_on the carrier of b₂ holds
( b₃ * (mlt b₄,b₅) = mlt (b₃ * b₄),b₅ & b₃ * (mlt b₄,b₅) = mlt b₄,(b₃ * b₅) )

proof end;

theorem Th84: :: FVSUM_1:84

for b₁ being Nat
for b₂ being non empty associative commutative HGrStr
for b₃ being Element of b₂
for b₄ being Element of b₁ -tuples_on the carrier of b₂ holds b₃ * b₄ = mlt (b₁ |-> b₃),b₄ by Th80;

registration

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

proof end;

end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
let c₂ be FinSequence of the carrier of c₁;
redefine func Sum c₂ -> Element of the carrier of a₁ equals :: FVSUM_1:def 8
the add of a₁ $$ a₂;
compatibility

proof end;

end;

:: deftheorem Def8 defines Sum FVSUM_1:def 8 :

theorem Th85: :: FVSUM_1:85

canceled;

theorem Th86: :: FVSUM_1:86

canceled;

theorem Th87: :: FVSUM_1:87

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Sum (b₃ ^ <*b₂*>) = (Sum b₃) + b₂

proof end;

theorem Th88: :: FVSUM_1:88

canceled;

theorem Th89: :: FVSUM_1:89

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Sum (<*b₂*> ^ b₃) = b₂ + (Sum b₃)

proof end;

theorem Th90: :: FVSUM_1:90

canceled;

theorem Th91: :: FVSUM_1:91

canceled;

theorem Th92: :: FVSUM_1:92

for b₁ being non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Sum (b₂ * b₃) = b₂ * (Sum b₃)

proof end;

theorem Th93: :: FVSUM_1:93

for b₁ being non empty LoopStr
for b₂ being Element of 0 -tuples_on the carrier of b₁ holds Sum b₂ = 0. b₁

proof end;

theorem Th94: :: FVSUM_1:94

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

proof end;

theorem Th95: :: FVSUM_1:95

for b₁ being Nat
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds Sum (b₃ + b₄) = (Sum b₃) + (Sum b₄)

proof end;

theorem Th96: :: FVSUM_1:96

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂ be FinSequence of the carrier of c₁;
func Product c₂ -> Element of a₁ equals :: FVSUM_1:def 9
the mult of a₁ $$ a₂;
coherence ;

end;

:: deftheorem Def9 defines Product FVSUM_1:def 9 :

theorem Th97: :: FVSUM_1:97

canceled;

theorem Th98: :: FVSUM_1:98

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

proof end;

theorem Th99: :: FVSUM_1:99

for b₁ being non empty HGrStr
for b₂ being Element of b₁ holds Product <*b₂*> = b₂ by FINSOP_1:12;

theorem Th100: :: FVSUM_1:100

for b₁ being non empty commutative left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Product (b₃ ^ <*b₂*>) = (Product b₃) * b₂

proof end;

theorem Th101: :: FVSUM_1:101

for b₁ being non empty associative commutative left_unital doubleLoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ holds Product (b₂ ^ b₃) = (Product b₂) * (Product b₃)

proof end;

theorem Th102: :: FVSUM_1:102

for b₁ being non empty associative commutative left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Product (<*b₂*> ^ b₃) = b₂ * (Product b₃)

proof end;

theorem Th103: :: FVSUM_1:103

for b₁ being non empty associative commutative left_unital doubleLoopStr
for b₂, b₃ being Element of b₁ holds Product <*b₂,b₃*> = b₂ * b₃

proof end;

theorem Th104: :: FVSUM_1:104

for b₁ being non empty associative commutative left_unital doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ holds Product <*b₂,b₃,b₄*> = (b₂ * b₃) * b₄

proof end;

theorem Th105: :: FVSUM_1:105

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

proof end;

theorem Th106: :: FVSUM_1:106

for b₁ being Nat
for b₂ being non empty associative commutative left_unital doubleLoopStr holds Product (b₁ |-> (1. b₂)) = 1. b₂

proof end;

theorem Th107: :: FVSUM_1:107

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr
for b₂ being FinSequence of the carrier of b₁ holds
( ex b₃ being Nat st
( b₃ in dom b₂ & b₂ . b₃ = 0. b₁ ) iff Product b₂ = 0. b₁ )

proof end;

theorem Th108: :: FVSUM_1:108

for b₁, b₂ being Nat
for b₃ being non empty associative commutative left_unital doubleLoopStr
for b₄ being Element of b₃ holds Product ((b₁ + b₂) |-> b₄) = (Product (b₁ |-> b₄)) * (Product (b₂ |-> b₄))

proof end;

theorem Th109: :: FVSUM_1:109

for b₁, b₂ being Nat
for b₃ being non empty associative commutative left_unital doubleLoopStr
for b₄ being Element of b₃ holds Product ((b₁ * b₂) |-> b₄) = Product (b₂ |-> (Product (b₁ |-> b₄)))

proof end;

theorem Th110: :: FVSUM_1:110

for b₁ being Nat
for b₂ being non empty associative commutative left_unital doubleLoopStr
for b₃, b₄ being Element of b₂ holds Product (b₁ |-> (b₃ * b₄)) = (Product (b₁ |-> b₃)) * (Product (b₁ |-> b₄))

proof end;

theorem Th111: :: FVSUM_1:111

for b₁ being Nat
for b₂ being non empty associative commutative left_unital doubleLoopStr
for b₃, b₄ being Element of b₁ -tuples_on the carrier of b₂ holds Product (mlt b₃,b₄) = (Product b₃) * (Product b₄)

proof end;

theorem Th112: :: FVSUM_1:112

for b₁ being Nat
for b₂ being non empty associative commutative left_unital doubleLoopStr
for b₃ being Element of b₂
for b₄ being Element of b₁ -tuples_on the carrier of b₂ holds Product (b₃ * b₄) = (Product (b₁ |-> b₃)) * (Product b₄)

proof end;

definition

let c₁ be non empty doubleLoopStr ;
let c₂, c₃ be FinSequence of the carrier of c₁;
func c₂ "*" c₃ -> Element of a₁ equals :: FVSUM_1:def 10
Sum (mlt a₂,a₃);
correctness ;

end;

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

theorem Th113: :: FVSUM_1:113

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

proof end;

theorem Th114: :: FVSUM_1:114

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative commutative left_unital doubleLoopStr
for b₂, b₃, b₄, b₅ being Element of b₁ holds <*b₂,b₃*> "*" <*b₄,b₅*> = (b₂ * b₄) + (b₃ * b₅)

proof end;

theorem Th115: :: FVSUM_1:115

for b₁ being non empty associative commutative left_unital doubleLoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ holds b₂ "*" b₃ = b₃ "*" b₂ by Th78;