:: RVSUM_1 semantic presentation

theorem Th1: :: RVSUM_1:1

canceled;

theorem Th2: :: RVSUM_1:2

canceled;

theorem Th3: :: RVSUM_1:3

0 is_a_unity_wrt addreal by BINOP_2:2, SETWISEO:22;

definition

redefine func diffreal -> M6([:REAL ,REAL :], REAL ) equals :Def1: :: RVSUM_1:def 1
addreal * (id REAL ),compreal ;
compatibility

proof end;

correctness ;

end;

:: deftheorem Def1 defines diffreal RVSUM_1:def 1 :

Lemma3: for b₁, b₂ being Element of REAL holds diffreal . b₁,b₂ = b₁ - b₂
by BINOP_2:def 10;

definition

func sqrreal -> UnOp of REAL means :Def2: :: RVSUM_1:def 2
for b₁ being Element of REAL holds a₁ . b₁ = b₁ ^2 ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines sqrreal RVSUM_1:def 2 :

theorem Th4: :: RVSUM_1:4

canceled;

theorem Th5: :: RVSUM_1:5

canceled;

theorem Th6: :: RVSUM_1:6

canceled;

theorem Th7: :: RVSUM_1:7

canceled;

theorem Th8: :: RVSUM_1:8

canceled;

theorem Th9: :: RVSUM_1:9

canceled;

theorem Th10: :: RVSUM_1:10

canceled;

theorem Th11: :: RVSUM_1:11

canceled;

theorem Th12: :: RVSUM_1:12

canceled;

theorem Th13: :: RVSUM_1:13

1 is_a_unity_wrt multreal by BINOP_2:7, SETWISEO:22;

theorem Th14: :: RVSUM_1:14

canceled;

theorem Th15: :: RVSUM_1:15

canceled;

theorem Th16: :: RVSUM_1:16

multreal is_distributive_wrt addreal

proof end;

theorem Th17: :: RVSUM_1:17

sqrreal is_distributive_wrt multreal

proof end;

definition

let c₁ be real number ;
func c₁ multreal -> UnOp of REAL equals :: RVSUM_1:def 3
multreal [;] a₁,(id REAL );
coherence

proof end;

end;

:: deftheorem Def3 defines multreal RVSUM_1:def 3 :

Lemma7: for b₁, b₂ being Element of REAL holds (multreal [;] b₁,(id REAL )) . b₂ = b₁ * b₂

proof end;

theorem Th18: :: RVSUM_1:18

canceled;

theorem Th19: :: RVSUM_1:19

for b₁, b₂ being Element of REAL holds (b₁ multreal ) . b₂ = b₁ * b₂ by Lemma7;

theorem Th20: :: RVSUM_1:20

for b₁ being Element of REAL holds b₁ multreal is_distributive_wrt addreal by Th16, FINSEQOP:55;

theorem Th21: :: RVSUM_1:21

compreal is_an_inverseOp_wrt addreal

proof end;

theorem Th22: :: RVSUM_1:22

addreal has_an_inverseOp by Th21, FINSEQOP:def 2;

theorem Th23: :: RVSUM_1:23

the_inverseOp_wrt addreal = compreal by Th21, Th22, FINSEQOP:def 3;

theorem Th24: :: RVSUM_1:24

compreal is_distributive_wrt addreal by Th22, Th23, FINSEQOP:67;

definition

let c₁, c₂ be FinSequence of REAL ;
func c₁ + c₂ -> FinSequence of REAL equals :: RVSUM_1:def 4
addreal .: a₁,a₂;
correctness ;
commutativity

proof end;

end;

:: deftheorem Def4 defines + RVSUM_1:def 4 :

theorem Th25: :: RVSUM_1:25

canceled;

theorem Th26: :: RVSUM_1:26

for b₁ being Nat
for b₂, b₃ being FinSequence of REAL st b₁ in dom (b₂ + b₃) holds
(b₂ + b₃) . b₁ = (b₂ . b₁) + (b₃ . b₁)

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on REAL ;
redefine func + as c₂ + c₃ -> Element of a₁ -tuples_on REAL ;
coherence by FINSEQ_2:140;

end;

theorem Th27: :: RVSUM_1:27

for b₁, b₂ being Nat
for b₃, b₄ being Element of b₁ -tuples_on REAL holds (b₃ + b₄) . b₂ = (b₃ . b₂) + (b₄ . b₂)

proof end;

theorem Th28: :: RVSUM_1:28

for b₁ being FinSequence of REAL holds (<*> REAL ) + b₁ = <*> REAL by FINSEQ_2:87;

theorem Th29: :: RVSUM_1:29

for b₁, b₂ being Element of REAL holds <*b₁*> + <*b₂*> = <*(b₁ + b₂)*>

proof end;

theorem Th30: :: RVSUM_1:30

for b₁ being Nat
for b₂, b₃ being Element of REAL holds (b₁ |-> b₂) + (b₁ |-> b₃) = b₁ |-> (b₂ + b₃)

proof end;

theorem Th31: :: RVSUM_1:31

canceled;

theorem Th32: :: RVSUM_1:32

for b₁ being Nat
for b₂, b₃, b₄ being Element of b₁ -tuples_on REAL holds b₂ + (b₃ + b₄) = (b₂ + b₃) + b₄ by FINSEQOP:29;

theorem Th33: :: RVSUM_1:33

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds b₂ + (b₁ |-> 0) = b₂ by BINOP_2:2, FINSEQOP:57;

definition

let c₁ be FinSequence of REAL ;
func - c₁ -> FinSequence of REAL equals :: RVSUM_1:def 5
compreal * a₁;
correctness ;
involutiveness

proof end;

end;

:: deftheorem Def5 defines - RVSUM_1:def 5 :

theorem Th34: :: RVSUM_1:34

for b₁ being FinSequence of REAL holds dom b₁ = dom (- b₁)

proof end;

theorem Th35: :: RVSUM_1:35

for b₁ being Nat
for b₂ being FinSequence of REAL holds (- b₂) . b₁ = - (b₂ . b₁)

proof end;

definition

let c₁ be Nat;
let c₂ be Element of c₁ -tuples_on REAL ;
redefine func - as - c₂ -> Element of a₁ -tuples_on REAL ;
coherence by FINSEQ_2:133;

end;

theorem Th36: :: RVSUM_1:36

for b₁, b₂ being Nat
for b₃ being Element of REAL
for b₄ being Element of b₁ -tuples_on REAL st b₃ = b₄ . b₂ holds
(- b₄) . b₂ = - b₃ by Th35;

theorem Th37: :: RVSUM_1:37

- (<*> REAL ) = <*> REAL by FINSEQ_2:38;

theorem Th38: :: RVSUM_1:38

for b₁ being Element of REAL holds - <*b₁*> = <*(- b₁)*>

proof end;

theorem Th39: :: RVSUM_1:39

for b₁ being Nat
for b₂ being Element of REAL holds - (b₁ |-> b₂) = b₁ |-> (- b₂)

proof end;

theorem Th40: :: RVSUM_1:40

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds b₂ + (- b₂) = b₁ |-> 0 by Th22, Th23, BINOP_2:2, FINSEQOP:77;

theorem Th41: :: RVSUM_1:41

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL st b₂ + b₃ = b₁ |-> 0 holds
b₂ = - b₃ by Th22, Th23, BINOP_2:2, FINSEQOP:78;

theorem Th42: :: RVSUM_1:42

canceled;

theorem Th43: :: RVSUM_1:43

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL st - b₂ = - b₃ holds
b₂ = b₃

proof end;

theorem Th44: :: RVSUM_1:44

for b₁ being Nat
for b₂, b₃, b₄ being Element of b₁ -tuples_on REAL st b₂ + b₃ = b₄ + b₃ holds
b₂ = b₄

proof end;

theorem Th45: :: RVSUM_1:45

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds - (b₂ + b₃) = (- b₂) + (- b₃)

proof end;

definition

let c₁, c₂ be FinSequence of REAL ;
func c₁ - c₂ -> FinSequence of REAL equals :: RVSUM_1:def 6
diffreal .: a₁,a₂;
correctness ;

end;

:: deftheorem Def6 defines - RVSUM_1:def 6 :

theorem Th46: :: RVSUM_1:46

canceled;

theorem Th47: :: RVSUM_1:47

for b₁ being Nat
for b₂, b₃ being FinSequence of REAL st b₁ in dom (b₂ - b₃) holds
(b₂ - b₃) . b₁ = (b₂ . b₁) - (b₃ . b₁)

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on REAL ;
redefine func - as c₂ - c₃ -> Element of a₁ -tuples_on REAL ;
coherence by FINSEQ_2:140;

end;

theorem Th48: :: RVSUM_1:48

for b₁, b₂ being Nat
for b₃, b₄ being Element of b₁ -tuples_on REAL holds (b₃ - b₄) . b₂ = (b₃ . b₂) - (b₄ . b₂)

proof end;

theorem Th49: :: RVSUM_1:49

for b₁ being FinSequence of REAL holds
( (<*> REAL ) - b₁ = <*> REAL & b₁ - (<*> REAL ) = <*> REAL ) by FINSEQ_2:87;

theorem Th50: :: RVSUM_1:50

for b₁, b₂ being Element of REAL holds <*b₁*> - <*b₂*> = <*(b₁ - b₂)*>

proof end;

theorem Th51: :: RVSUM_1:51

for b₁ being Nat
for b₂, b₃ being Element of REAL holds (b₁ |-> b₂) - (b₁ |-> b₃) = b₁ |-> (b₂ - b₃)

proof end;

theorem Th52: :: RVSUM_1:52

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds b₂ - b₃ = b₂ + (- b₃) by Def1, FINSEQOP:89;

theorem Th53: :: RVSUM_1:53

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds b₂ - (b₁ |-> 0) = b₂

proof end;

theorem Th54: :: RVSUM_1:54

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds (b₁ |-> 0) - b₂ = - b₂

proof end;

theorem Th55: :: RVSUM_1:55

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds b₂ - (- b₃) = b₂ + b₃

proof end;

theorem Th56: :: RVSUM_1:56

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds - (b₂ - b₃) = b₃ - b₂

proof end;

theorem Th57: :: RVSUM_1:57

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds - (b₂ - b₃) = (- b₂) + b₃

proof end;

theorem Th58: :: RVSUM_1:58

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds b₂ - b₂ = b₁ |-> 0

proof end;

theorem Th59: :: RVSUM_1:59

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL st b₂ - b₃ = b₁ |-> 0 holds
b₂ = b₃

proof end;

theorem Th60: :: RVSUM_1:60

for b₁ being Nat
for b₂, b₃, b₄ being Element of b₁ -tuples_on REAL holds (b₂ - b₃) - b₄ = b₂ - (b₃ + b₄)

proof end;

theorem Th61: :: RVSUM_1:61

for b₁ being Nat
for b₂, b₃, b₄ being Element of b₁ -tuples_on REAL holds b₂ + (b₃ - b₄) = (b₂ + b₃) - b₄

proof end;

theorem Th62: :: RVSUM_1:62

for b₁ being Nat
for b₂, b₃, b₄ being Element of b₁ -tuples_on REAL holds b₂ - (b₃ - b₄) = (b₂ - b₃) + b₄

proof end;

theorem Th63: :: RVSUM_1:63

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds b₂ = (b₂ + b₃) - b₃

proof end;

theorem Th64: :: RVSUM_1:64

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds b₂ = (b₂ - b₃) + b₃

proof end;

definition

let c₁ be real number ;
let c₂ be FinSequence of REAL ;
func c₁ * c₂ -> FinSequence of REAL equals :: RVSUM_1:def 7
(a₁ multreal ) * a₂;
correctness ;

end;

:: deftheorem Def7 defines * RVSUM_1:def 7 :

theorem Th65: :: RVSUM_1:65

for b₁ being Element of REAL
for b₂ being FinSequence of REAL holds dom (b₁ * b₂) = dom b₂

proof end;

theorem Th66: :: RVSUM_1:66

for b₁ being Nat
for b₂ being Element of REAL
for b₃ being FinSequence of REAL holds (b₂ * b₃) . b₁ = b₂ * (b₃ . b₁)

proof end;

definition

let c₁ be Nat;
let c₂ be real number ;
let c₃ be Element of c₁ -tuples_on REAL ;
redefine func * as c₂ * c₃ -> Element of a₁ -tuples_on REAL ;
coherence by FINSEQ_2:133;

end;

theorem Th67: :: RVSUM_1:67

for b₁, b₂ being Nat
for b₃ being Element of REAL
for b₄ being Element of b₁ -tuples_on REAL holds (b₃ * b₄) . b₂ = b₃ * (b₄ . b₂) by Th66;

theorem Th68: :: RVSUM_1:68

for b₁ being Element of REAL holds b₁ * (<*> REAL ) = <*> REAL by FINSEQ_2:38;

theorem Th69: :: RVSUM_1:69

for b₁, b₂ being Element of REAL holds b₁ * <*b₂*> = <*(b₁ * b₂)*>

proof end;

theorem Th70: :: RVSUM_1:70

for b₁ being Nat
for b₂, b₃ being Element of REAL holds b₂ * (b₁ |-> b₃) = b₁ |-> (b₂ * b₃)

proof end;

theorem Th71: :: RVSUM_1:71

for b₁ being Nat
for b₂, b₃ being Element of REAL
for b₄ being Element of b₁ -tuples_on REAL holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th72: :: RVSUM_1:72

for b₁ being Nat
for b₂, b₃ being Element of REAL
for b₄ being Element of b₁ -tuples_on REAL holds (b₂ + b₃) * b₄ = (b₂ * b₄) + (b₃ * b₄)

proof end;

theorem Th73: :: RVSUM_1:73

for b₁ being Nat
for b₂ being Element of REAL
for b₃, b₄ being Element of b₁ -tuples_on REAL holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄)

proof end;

theorem Th74: :: RVSUM_1:74

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds 1 * b₂ = b₂

proof end;

theorem Th75: :: RVSUM_1:75

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds 0 * b₂ = b₁ |-> 0

proof end;

theorem Th76: :: RVSUM_1:76

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds (- 1) * b₂ = - b₂

proof end;

definition

let c₁ be FinSequence of REAL ;
func sqr c₁ -> FinSequence of REAL equals :: RVSUM_1:def 8
sqrreal * a₁;
correctness ;

end;

:: deftheorem Def8 defines sqr RVSUM_1:def 8 :

theorem Th77: :: RVSUM_1:77

for b₁ being FinSequence of REAL holds dom (sqr b₁) = dom b₁

proof end;

theorem Th78: :: RVSUM_1:78

for b₁ being Nat
for b₂ being FinSequence of REAL holds (sqr b₂) . b₁ = (b₂ . b₁) ^2

proof end;

definition

let c₁ be Nat;
let c₂ be Element of c₁ -tuples_on REAL ;
redefine func sqr as sqr c₂ -> Element of a₁ -tuples_on REAL ;
coherence by FINSEQ_2:133;

end;

theorem Th79: :: RVSUM_1:79

for b₁, b₂ being Nat
for b₃ being Element of b₁ -tuples_on REAL holds (sqr b₃) . b₂ = (b₃ . b₂) ^2 by Th78;

theorem Th80: :: RVSUM_1:80

sqr (<*> REAL ) = <*> REAL by FINSEQ_2:38;

theorem Th81: :: RVSUM_1:81

for b₁ being Element of REAL holds sqr <*b₁*> = <*(b₁ ^2 )*>

proof end;

theorem Th82: :: RVSUM_1:82

for b₁ being Nat
for b₂ being Element of REAL holds sqr (b₁ |-> b₂) = b₁ |-> (b₂ ^2 )

proof end;

theorem Th83: :: RVSUM_1:83

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds sqr (- b₂) = sqr b₂

proof end;

theorem Th84: :: RVSUM_1:84

for b₁ being Nat
for b₂ being Element of REAL
for b₃ being Element of b₁ -tuples_on REAL holds sqr (b₂ * b₃) = (b₂ ^2 ) * (sqr b₃)

proof end;

definition

let c₁, c₂ be FinSequence of REAL ;
func mlt c₁,c₂ -> FinSequence of REAL equals :: RVSUM_1:def 9
multreal .: a₁,a₂;
correctness ;
commutativity

proof end;

end;

:: deftheorem Def9 defines mlt RVSUM_1:def 9 :

theorem Th85: :: RVSUM_1:85

canceled;

theorem Th86: :: RVSUM_1:86

for b₁ being Nat
for b₂, b₃ being FinSequence of REAL st b₁ in dom (mlt b₂,b₃) holds
(mlt b₂,b₃) . b₁ = (b₂ . b₁) * (b₃ . b₁)

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on REAL ;
redefine func mlt as mlt c₂,c₃ -> Element of a₁ -tuples_on REAL ;
coherence by FINSEQ_2:140;

end;

theorem Th87: :: RVSUM_1:87

for b₁, b₂ being Nat
for b₃, b₄ being Element of b₁ -tuples_on REAL holds (mlt b₃,b₄) . b₂ = (b₃ . b₂) * (b₄ . b₂)

proof end;

theorem Th88: :: RVSUM_1:88

for b₁ being FinSequence of REAL holds mlt (<*> REAL ),b₁ = <*> REAL by FINSEQ_2:87;

theorem Th89: :: RVSUM_1:89

for b₁, b₂ being Element of REAL holds mlt <*b₁*>,<*b₂*> = <*(b₁ * b₂)*>

proof end;

theorem Th90: :: RVSUM_1:90

canceled;

theorem Th91: :: RVSUM_1:91

for b₁ being Nat
for b₂, b₃, b₄ being Element of b₁ -tuples_on REAL holds mlt b₂,(mlt b₃,b₄) = mlt (mlt b₂,b₃),b₄ by FINSEQOP:29;

theorem Th92: :: RVSUM_1:92

for b₁ being Nat
for b₂ being Element of REAL
for b₃ being Element of b₁ -tuples_on REAL holds mlt (b₁ |-> b₂),b₃ = b₂ * b₃

proof end;

theorem Th93: :: RVSUM_1:93

for b₁ being Nat
for b₂, b₃ being Element of REAL holds mlt (b₁ |-> b₂),(b₁ |-> b₃) = b₁ |-> (b₂ * b₃)

proof end;

theorem Th94: :: RVSUM_1:94

for b₁ being Nat
for b₂ being Element of REAL
for b₃, b₄ being Element of b₁ -tuples_on REAL holds b₂ * (mlt b₃,b₄) = mlt (b₂ * b₃),b₄ by FINSEQOP:27;

theorem Th95: :: RVSUM_1:95

canceled;

theorem Th96: :: RVSUM_1:96

for b₁ being Nat
for b₂ being Element of REAL
for b₃ being Element of b₁ -tuples_on REAL holds b₂ * b₃ = mlt (b₁ |-> b₂),b₃ by Th92;

theorem Th97: :: RVSUM_1:97

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds sqr b₂ = mlt b₂,b₂

proof end;

theorem Th98: :: RVSUM_1:98

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds sqr (b₂ + b₃) = ((sqr b₂) + (2 * (mlt b₂,b₃))) + (sqr b₃)

proof end;

theorem Th99: :: RVSUM_1:99

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds sqr (b₂ - b₃) = ((sqr b₂) - (2 * (mlt b₂,b₃))) + (sqr b₃)

proof end;

theorem Th100: :: RVSUM_1:100

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds sqr (mlt b₂,b₃) = mlt (sqr b₂),(sqr b₃) by Th17, FINSEQOP:52;

definition

let c₁ be FinSequence of REAL ;
func Sum c₁ -> Real equals :: RVSUM_1:def 10
addreal $$ a₁;
coherence ;

end;

:: deftheorem Def10 defines Sum RVSUM_1:def 10 :

theorem Th101: :: RVSUM_1:101

canceled;

theorem Th102: :: RVSUM_1:102

Sum (<*> REAL ) = 0 by BINOP_2:2, FINSOP_1:11;

theorem Th103: :: RVSUM_1:103

for b₁ being Element of REAL holds Sum <*b₁*> = b₁ by FINSOP_1:12;

theorem Th104: :: RVSUM_1:104

for b₁ being Element of REAL
for b₂ being FinSequence of REAL holds Sum (b₂ ^ <*b₁*>) = (Sum b₂) + b₁

proof end;

theorem Th105: :: RVSUM_1:105

for b₁, b₂ being FinSequence of REAL holds Sum (b₁ ^ b₂) = (Sum b₁) + (Sum b₂)

proof end;

theorem Th106: :: RVSUM_1:106

for b₁ being Element of REAL
for b₂ being FinSequence of REAL holds Sum (<*b₁*> ^ b₂) = b₁ + (Sum b₂)

proof end;

theorem Th107: :: RVSUM_1:107

for b₁, b₂ being Element of REAL holds Sum <*b₁,b₂*> = b₁ + b₂

proof end;

theorem Th108: :: RVSUM_1:108

for b₁, b₂, b₃ being Element of REAL holds Sum <*b₁,b₂,b₃*> = (b₁ + b₂) + b₃

proof end;

theorem Th109: :: RVSUM_1:109

for b₁ being Element of 0 -tuples_on REAL holds Sum b₁ = 0 by Th102, FINSEQ_2:113;

theorem Th110: :: RVSUM_1:110

for b₁ being Nat
for b₂ being Element of REAL holds Sum (b₁ |-> b₂) = b₁ * b₂

proof end;

theorem Th111: :: RVSUM_1:111

for b₁ being Nat holds Sum (b₁ |-> 0) = 0

proof end;

theorem Th112: :: RVSUM_1:112

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL st ( for b₄ being Nat st b₄ in Seg b₁ holds
b₂ . b₄ <= b₃ . b₄ ) holds
Sum b₂ <= Sum b₃

proof end;

theorem Th113: :: RVSUM_1:113

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL st ( for b₄ being Nat st b₄ in Seg b₁ holds
b₂ . b₄ <= b₃ . b₄ ) & ex b₄ being Nat st
( b₄ in Seg b₁ & b₂ . b₄ < b₃ . b₄ ) holds
Sum b₂ < Sum b₃

proof end;

theorem Th114: :: RVSUM_1:114

for b₁ being FinSequence of REAL st ( for b₂ being Nat st b₂ in dom b₁ holds
0 <= b₁ . b₂ ) holds
0 <= Sum b₁

proof end;

theorem Th115: :: RVSUM_1:115

for b₁ being FinSequence of REAL st ( for b₂ being Nat st b₂ in dom b₁ holds
0 <= b₁ . b₂ ) & ex b₂ being Nat st
( b₂ in dom b₁ & 0 < b₁ . b₂ ) holds
0 < Sum b₁

proof end;

theorem Th116: :: RVSUM_1:116

for b₁ being FinSequence of REAL holds 0 <= Sum (sqr b₁)

proof end;

theorem Th117: :: RVSUM_1:117

for b₁ being Element of REAL
for b₂ being FinSequence of REAL holds Sum (b₁ * b₂) = b₁ * (Sum b₂)

proof end;

theorem Th118: :: RVSUM_1:118

for b₁ being FinSequence of REAL holds Sum (- b₁) = - (Sum b₁)

proof end;

theorem Th119: :: RVSUM_1:119

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds Sum (b₂ + b₃) = (Sum b₂) + (Sum b₃)

proof end;

theorem Th120: :: RVSUM_1:120

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds Sum (b₂ - b₃) = (Sum b₂) - (Sum b₃)

proof end;

theorem Th121: :: RVSUM_1:121

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL st Sum (sqr b₂) = 0 holds
b₂ = b₁ |-> 0

proof end;

theorem Th122: :: RVSUM_1:122

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds (Sum (mlt b₂,b₃)) ^2 <= (Sum (sqr b₂)) * (Sum (sqr b₃))

proof end;

definition

let c₁ be FinSequence of REAL ;
func Product c₁ -> Real equals :: RVSUM_1:def 11
multreal $$ a₁;
coherence ;

end;

:: deftheorem Def11 defines Product RVSUM_1:def 11 :

theorem Th123: :: RVSUM_1:123

canceled;

theorem Th124: :: RVSUM_1:124

Product (<*> REAL ) = 1 by BINOP_2:7, FINSOP_1:11;

theorem Th125: :: RVSUM_1:125

for b₁ being Element of REAL holds Product <*b₁*> = b₁ by FINSOP_1:12;

theorem Th126: :: RVSUM_1:126

for b₁ being Element of REAL
for b₂ being FinSequence of REAL holds Product (b₂ ^ <*b₁*>) = (Product b₂) * b₁

proof end;

theorem Th127: :: RVSUM_1:127

for b₁, b₂ being FinSequence of REAL holds Product (b₁ ^ b₂) = (Product b₁) * (Product b₂)

proof end;

theorem Th128: :: RVSUM_1:128

for b₁ being Element of REAL
for b₂ being FinSequence of REAL holds Product (<*b₁*> ^ b₂) = b₁ * (Product b₂)

proof end;

theorem Th129: :: RVSUM_1:129

for b₁, b₂ being Element of REAL holds Product <*b₁,b₂*> = b₁ * b₂

proof end;

theorem Th130: :: RVSUM_1:130

for b₁, b₂, b₃ being Element of REAL holds Product <*b₁,b₂,b₃*> = (b₁ * b₂) * b₃

proof end;

theorem Th131: :: RVSUM_1:131

for b₁ being Element of 0 -tuples_on REAL holds Product b₁ = 1 by Th124, FINSEQ_2:113;

theorem Th132: :: RVSUM_1:132

for b₁ being Nat holds Product (b₁ |-> 1) = 1 by BINOP_2:7, SETWOP_2:35;

theorem Th133: :: RVSUM_1:133

for b₁ being FinSequence of REAL holds
( ex b₂ being Nat st
( b₂ in dom b₁ & b₁ . b₂ = 0 ) iff Product b₁ = 0 )

proof end;

theorem Th134: :: RVSUM_1:134

for b₁, b₂ being Nat
for b₃ being Element of REAL holds Product ((b₁ + b₂) |-> b₃) = (Product (b₁ |-> b₃)) * (Product (b₂ |-> b₃))

proof end;

theorem Th135: :: RVSUM_1:135

for b₁, b₂ being Nat
for b₃ being Element of REAL holds Product ((b₁ * b₂) |-> b₃) = Product (b₂ |-> (Product (b₁ |-> b₃))) by SETWOP_2:38;

theorem Th136: :: RVSUM_1:136

for b₁ being Nat
for b₂, b₃ being Element of REAL holds Product (b₁ |-> (b₂ * b₃)) = (Product (b₁ |-> b₂)) * (Product (b₁ |-> b₃))

proof end;

theorem Th137: :: RVSUM_1:137

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on REAL holds Product (mlt b₂,b₃) = (Product b₂) * (Product b₃)

proof end;

theorem Th138: :: RVSUM_1:138

for b₁ being Nat
for b₂ being Element of REAL
for b₃ being Element of b₁ -tuples_on REAL holds Product (b₂ * b₃) = (Product (b₁ |-> b₂)) * (Product b₃)

proof end;

theorem Th139: :: RVSUM_1:139

for b₁ being Nat
for b₂ being Element of b₁ -tuples_on REAL holds Product (sqr b₂) = (Product b₂) ^2

proof end;