:: RVSUM_1 semantic presentation

theorem :: RVSUM_1:1

canceled;

theorem :: 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 equals :Def1: :: RVSUM_1:def 1
addreal * (id REAL ),compreal ;
compatibility

proof end;

correctness ;

end;

:: deftheorem Def1 defines diffreal RVSUM_1:def 1 :

Lm1: for r1, r2 being Element of REAL holds diffreal . r1,r2 = r1 - r2
by BINOP_2:def 10;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines sqrreal RVSUM_1:def 2 :

theorem :: RVSUM_1:4

canceled;

theorem :: RVSUM_1:5

canceled;

theorem :: RVSUM_1:6

canceled;

theorem :: RVSUM_1:7

canceled;

theorem :: RVSUM_1:8

canceled;

theorem :: RVSUM_1:9

canceled;

theorem :: RVSUM_1:10

canceled;

theorem :: RVSUM_1:11

canceled;

theorem :: RVSUM_1:12

canceled;

theorem :: RVSUM_1:13

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

theorem :: RVSUM_1:14

canceled;

theorem :: 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 x be real number ;
func x multreal -> UnOp of REAL equals :: RVSUM_1:def 3
multreal [;] x,(id REAL );
coherence

proof end;

end;

:: deftheorem defines multreal RVSUM_1:def 3 :

Lm2: for r, x being Element of REAL holds (multreal [;] r,(id REAL )) . x = r * x

proof end;

theorem :: RVSUM_1:18

canceled;

theorem :: RVSUM_1:19

for r, x being Element of REAL holds (r multreal ) . x = r * x by Lm2;

theorem Th20: :: RVSUM_1:20

for r being Element of REAL holds r 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 :: RVSUM_1:24

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

definition

let F1, F2 be FinSequence of REAL ;
func F1 + F2 -> FinSequence of REAL equals :: RVSUM_1:def 4
addreal .: F1,F2;
correctness ;
commutativity

proof end;

end;

:: deftheorem defines + RVSUM_1:def 4 :

theorem :: RVSUM_1:25

canceled;

theorem Th26: :: RVSUM_1:26

for i being Nat
for F1, F2 being FinSequence of REAL st i in dom (F1 + F2) holds
(F1 + F2) . i = (F1 . i) + (F2 . i)

proof end;

definition

let i be Nat;
let R1, R2 be Element of i -tuples_on REAL ;
:: original: +
redefine func R1 + R2 -> Element of i -tuples_on REAL ;
coherence by FINSEQ_2:140;

end;

theorem Th27: :: RVSUM_1:27

for i, j being Nat
for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . j = (R1 . j) + (R2 . j)

proof end;

theorem :: RVSUM_1:28

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

theorem :: RVSUM_1:29

for r1, r2 being Element of REAL holds <*r1*> + <*r2*> = <*(r1 + r2)*>

proof end;

theorem :: RVSUM_1:30

for i being Nat
for r1, r2 being Element of REAL holds (i |-> r1) + (i |-> r2) = i |-> (r1 + r2)

proof end;

theorem :: RVSUM_1:31

canceled;

theorem Th32: :: RVSUM_1:32

for i being Nat
for R1, R2, R3 being Element of i -tuples_on REAL holds R1 + (R2 + R3) = (R1 + R2) + R3 by FINSEQOP:29;

theorem Th33: :: RVSUM_1:33

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

definition

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

proof end;

end;

:: deftheorem defines - RVSUM_1:def 5 :

theorem Th34: :: RVSUM_1:34

for F being FinSequence of REAL holds dom F = dom (- F)

proof end;

theorem Th35: :: RVSUM_1:35

for i being Nat
for F being FinSequence of REAL holds (- F) . i = - (F . i)

proof end;

definition

let i be Nat;
let R be Element of i -tuples_on REAL ;
:: original: -
redefine func - R -> Element of i -tuples_on REAL ;
coherence by FINSEQ_2:133;

end;

theorem :: RVSUM_1:36

for i, j being Nat
for r being Element of REAL
for R being Element of i -tuples_on REAL st r = R . j holds
(- R) . j = - r by Th35;

theorem :: RVSUM_1:37

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

theorem :: RVSUM_1:38

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

proof end;

theorem Th39: :: RVSUM_1:39

for i being Nat
for r being Element of REAL holds - (i |-> r) = i |-> (- r)

proof end;

theorem Th40: :: RVSUM_1:40

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

theorem Th41: :: RVSUM_1:41

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st R1 + R2 = i |-> 0 holds
R1 = - R2 by Th22, Th23, BINOP_2:2, FINSEQOP:78;

theorem :: RVSUM_1:42

canceled;

theorem :: RVSUM_1:43

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st - R1 = - R2 holds
R1 = R2

proof end;

theorem :: RVSUM_1:44

for i being Nat
for R1, R, R2 being Element of i -tuples_on REAL st R1 + R = R2 + R holds
R1 = R2

proof end;

theorem Th45: :: RVSUM_1:45

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds - (R1 + R2) = (- R1) + (- R2)

proof end;

definition

let F1, F2 be FinSequence of REAL ;
func F1 - F2 -> FinSequence of REAL equals :: RVSUM_1:def 6
diffreal .: F1,F2;
correctness ;

end;

:: deftheorem defines - RVSUM_1:def 6 :

theorem :: RVSUM_1:46

canceled;

theorem Th47: :: RVSUM_1:47

for i being Nat
for F1, F2 being FinSequence of REAL st i in dom (F1 - F2) holds
(F1 - F2) . i = (F1 . i) - (F2 . i)

proof end;

definition

let i be Nat;
let R1, R2 be Element of i -tuples_on REAL ;
:: original: -
redefine func R1 - R2 -> Element of i -tuples_on REAL ;
coherence by FINSEQ_2:140;

end;

theorem :: RVSUM_1:48

for i, j being Nat
for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . j = (R1 . j) - (R2 . j)

proof end;

theorem :: RVSUM_1:49

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

theorem :: RVSUM_1:50

for r1, r2 being Element of REAL holds <*r1*> - <*r2*> = <*(r1 - r2)*>

proof end;

theorem :: RVSUM_1:51

for i being Nat
for r1, r2 being Element of REAL holds (i |-> r1) - (i |-> r2) = i |-> (r1 - r2)

proof end;

theorem Th52: :: RVSUM_1:52

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds R1 - R2 = R1 + (- R2) by Def1, FINSEQOP:89;

theorem :: RVSUM_1:53

for i being Nat
for R being Element of i -tuples_on REAL holds R - (i |-> 0) = R

proof end;

theorem :: RVSUM_1:54

for i being Nat
for R being Element of i -tuples_on REAL holds (i |-> 0) - R = - R

proof end;

theorem :: RVSUM_1:55

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds R1 - (- R2) = R1 + R2

proof end;

theorem :: RVSUM_1:56

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds - (R1 - R2) = R2 - R1

proof end;

theorem Th57: :: RVSUM_1:57

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds - (R1 - R2) = (- R1) + R2

proof end;

theorem Th58: :: RVSUM_1:58

for i being Nat
for R being Element of i -tuples_on REAL holds R - R = i |-> 0

proof end;

theorem :: RVSUM_1:59

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st R1 - R2 = i |-> 0 holds
R1 = R2

proof end;

theorem :: RVSUM_1:60

for i being Nat
for R1, R2, R3 being Element of i -tuples_on REAL holds (R1 - R2) - R3 = R1 - (R2 + R3)

proof end;

theorem Th61: :: RVSUM_1:61

for i being Nat
for R1, R2, R3 being Element of i -tuples_on REAL holds R1 + (R2 - R3) = (R1 + R2) - R3

proof end;

theorem :: RVSUM_1:62

for i being Nat
for R1, R2, R3 being Element of i -tuples_on REAL holds R1 - (R2 - R3) = (R1 - R2) + R3

proof end;

theorem :: RVSUM_1:63

for i being Nat
for R1, R being Element of i -tuples_on REAL holds R1 = (R1 + R) - R

proof end;

theorem :: RVSUM_1:64

for i being Nat
for R1, R being Element of i -tuples_on REAL holds R1 = (R1 - R) + R

proof end;

definition

let r be real number ;
let F be FinSequence of REAL ;
func r * F -> FinSequence of REAL equals :: RVSUM_1:def 7
(r multreal ) * F;
correctness ;

end;

:: deftheorem defines * RVSUM_1:def 7 :

theorem Th65: :: RVSUM_1:65

for r being Element of REAL
for F being FinSequence of REAL holds dom (r * F) = dom F

proof end;

theorem Th66: :: RVSUM_1:66

for i being Nat
for r being Element of REAL
for F being FinSequence of REAL holds (r * F) . i = r * (F . i)

proof end;

definition

let i be Nat;
let r be real number ;
let R be Element of i -tuples_on REAL ;
:: original: *
redefine func r * R -> Element of i -tuples_on REAL ;
coherence by FINSEQ_2:133;

end;

theorem :: RVSUM_1:67

for i, j being Nat
for r being Element of REAL
for R being Element of i -tuples_on REAL holds (r * R) . j = r * (R . j) by Th66;

theorem :: RVSUM_1:68

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

theorem :: RVSUM_1:69

for r, r1 being Element of REAL holds r * <*r1*> = <*(r * r1)*>

proof end;

theorem Th70: :: RVSUM_1:70

for i being Nat
for r1, r2 being Element of REAL holds r1 * (i |-> r2) = i |-> (r1 * r2)

proof end;

theorem Th71: :: RVSUM_1:71

for i being Nat
for r1, r2 being Element of REAL
for R being Element of i -tuples_on REAL holds (r1 * r2) * R = r1 * (r2 * R)

proof end;

theorem :: RVSUM_1:72

for i being Nat
for r1, r2 being Element of REAL
for R being Element of i -tuples_on REAL holds (r1 + r2) * R = (r1 * R) + (r2 * R)

proof end;

theorem :: RVSUM_1:73

for i being Nat
for r being Element of REAL
for R1, R2 being Element of i -tuples_on REAL holds r * (R1 + R2) = (r * R1) + (r * R2)

proof end;

theorem :: RVSUM_1:74

for i being Nat
for R being Element of i -tuples_on REAL holds 1 * R = R

proof end;

theorem :: RVSUM_1:75

for i being Nat
for R being Element of i -tuples_on REAL holds 0 * R = i |-> 0

proof end;

theorem Th76: :: RVSUM_1:76

for i being Nat
for R being Element of i -tuples_on REAL holds (- 1) * R = - R

proof end;

definition

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

end;

:: deftheorem defines sqr RVSUM_1:def 8 :

theorem Th77: :: RVSUM_1:77

for F being FinSequence of REAL holds dom (sqr F) = dom F

proof end;

theorem Th78: :: RVSUM_1:78

for i being Nat
for F being FinSequence of REAL holds (sqr F) . i = (F . i) ^2

proof end;

definition

let i be Nat;
let R be Element of i -tuples_on REAL ;
:: original: sqr
redefine func sqr R -> Element of i -tuples_on REAL ;
coherence by FINSEQ_2:133;

end;

theorem :: RVSUM_1:79

for i, j being Nat
for R being Element of i -tuples_on REAL holds (sqr R) . j = (R . j) ^2 by Th78;

theorem :: RVSUM_1:80

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

theorem :: RVSUM_1:81

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

proof end;

theorem :: RVSUM_1:82

for i being Nat
for r being Element of REAL holds sqr (i |-> r) = i |-> (r ^2 )

proof end;

theorem Th83: :: RVSUM_1:83

for i being Nat
for R being Element of i -tuples_on REAL holds sqr (- R) = sqr R

proof end;

theorem Th84: :: RVSUM_1:84

for i being Nat
for r being Element of REAL
for R being Element of i -tuples_on REAL holds sqr (r * R) = (r ^2 ) * (sqr R)

proof end;

definition

let F1, F2 be FinSequence of REAL ;
func mlt F1,F2 -> FinSequence of REAL equals :: RVSUM_1:def 9
multreal .: F1,F2;
correctness ;
commutativity

proof end;

end;

:: deftheorem defines mlt RVSUM_1:def 9 :

theorem :: RVSUM_1:85

canceled;

theorem Th86: :: RVSUM_1:86

for i being Nat
for F1, F2 being FinSequence of REAL st i in dom (mlt F1,F2) holds
(mlt F1,F2) . i = (F1 . i) * (F2 . i)

proof end;

definition

let i be Nat;
let R1, R2 be Element of i -tuples_on REAL ;
:: original: mlt
redefine func mlt R1,R2 -> Element of i -tuples_on REAL ;
coherence by FINSEQ_2:140;

end;

theorem Th87: :: RVSUM_1:87

for i, j being Nat
for R1, R2 being Element of i -tuples_on REAL holds (mlt R1,R2) . j = (R1 . j) * (R2 . j)

proof end;

theorem :: RVSUM_1:88

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

theorem :: RVSUM_1:89

for r1, r2 being Element of REAL holds mlt <*r1*>,<*r2*> = <*(r1 * r2)*>

proof end;

theorem :: RVSUM_1:90

canceled;

theorem :: RVSUM_1:91

for i being Nat
for R1, R2, R3 being Element of i -tuples_on REAL holds mlt R1,(mlt R2,R3) = mlt (mlt R1,R2),R3 by FINSEQOP:29;

theorem Th92: :: RVSUM_1:92

for i being Nat
for r being Element of REAL
for R being Element of i -tuples_on REAL holds mlt (i |-> r),R = r * R

proof end;

theorem :: RVSUM_1:93

for i being Nat
for r1, r2 being Element of REAL holds mlt (i |-> r1),(i |-> r2) = i |-> (r1 * r2)

proof end;

theorem Th94: :: RVSUM_1:94

for i being Nat
for r being Element of REAL
for R1, R2 being Element of i -tuples_on REAL holds r * (mlt R1,R2) = mlt (r * R1),R2 by FINSEQOP:27;

theorem :: RVSUM_1:95

canceled;

theorem :: RVSUM_1:96

for i being Nat
for r being Element of REAL
for R being Element of i -tuples_on REAL holds r * R = mlt (i |-> r),R by Th92;

theorem Th97: :: RVSUM_1:97

for i being Nat
for R being Element of i -tuples_on REAL holds sqr R = mlt R,R

proof end;

theorem Th98: :: RVSUM_1:98

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds sqr (R1 + R2) = ((sqr R1) + (2 * (mlt R1,R2))) + (sqr R2)

proof end;

theorem Th99: :: RVSUM_1:99

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds sqr (R1 - R2) = ((sqr R1) - (2 * (mlt R1,R2))) + (sqr R2)

proof end;

theorem :: RVSUM_1:100

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds sqr (mlt R1,R2) = mlt (sqr R1),(sqr R2) by Th17, FINSEQOP:52;

definition

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

end;

:: deftheorem defines Sum RVSUM_1:def 10 :

theorem :: 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 r being Element of REAL holds Sum <*r*> = r by FINSOP_1:12;

theorem Th104: :: RVSUM_1:104

for r being Element of REAL
for F being FinSequence of REAL holds Sum (F ^ <*r*>) = (Sum F) + r

proof end;

theorem Th105: :: RVSUM_1:105

for F1, F2 being FinSequence of REAL holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)

proof end;

theorem :: RVSUM_1:106

for r being Element of REAL
for F being FinSequence of REAL holds Sum (<*r*> ^ F) = r + (Sum F)

proof end;

theorem Th107: :: RVSUM_1:107

for r1, r2 being Element of REAL holds Sum <*r1,r2*> = r1 + r2

proof end;

theorem :: RVSUM_1:108

for r1, r2, r3 being Element of REAL holds Sum <*r1,r2,r3*> = (r1 + r2) + r3

proof end;

theorem :: RVSUM_1:109

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

theorem Th110: :: RVSUM_1:110

for i being Nat
for r being Element of REAL holds Sum (i |-> r) = i * r

proof end;

theorem Th111: :: RVSUM_1:111

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

proof end;

theorem Th112: :: RVSUM_1:112

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2

proof end;

theorem Th113: :: RVSUM_1:113

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg i & R1 . j < R2 . j ) holds
Sum R1 < Sum R2

proof end;

theorem Th114: :: RVSUM_1:114

for F being FinSequence of REAL st ( for i being Nat st i in dom F holds
0 <= F . i ) holds
0 <= Sum F

proof end;

theorem Th115: :: RVSUM_1:115

for F being FinSequence of REAL st ( for i being Nat st i in dom F holds
0 <= F . i ) & ex i being Nat st
( i in dom F & 0 < F . i ) holds
0 < Sum F

proof end;

theorem Th116: :: RVSUM_1:116

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

proof end;

theorem Th117: :: RVSUM_1:117

for r being Element of REAL
for F being FinSequence of REAL holds Sum (r * F) = r * (Sum F)

proof end;

theorem :: RVSUM_1:118

for F being FinSequence of REAL holds Sum (- F) = - (Sum F)

proof end;

theorem Th119: :: RVSUM_1:119

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2)

proof end;

theorem Th120: :: RVSUM_1:120

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

proof end;

theorem :: RVSUM_1:121

for i being Nat
for R being Element of i -tuples_on REAL st Sum (sqr R) = 0 holds
R = i |-> 0

proof end;

theorem :: RVSUM_1:122

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt R1,R2)) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))

proof end;

definition

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

end;

:: deftheorem defines Product RVSUM_1:def 11 :

theorem :: 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 r being Element of REAL holds Product <*r*> = r by FINSOP_1:12;

theorem Th126: :: RVSUM_1:126

for r being Element of REAL
for F being FinSequence of REAL holds Product (F ^ <*r*>) = (Product F) * r

proof end;

theorem Th127: :: RVSUM_1:127

for F1, F2 being FinSequence of REAL holds Product (F1 ^ F2) = (Product F1) * (Product F2)

proof end;

theorem :: RVSUM_1:128

for r being Element of REAL
for F being FinSequence of REAL holds Product (<*r*> ^ F) = r * (Product F)

proof end;

theorem Th129: :: RVSUM_1:129

for r1, r2 being Element of REAL holds Product <*r1,r2*> = r1 * r2

proof end;

theorem :: RVSUM_1:130

for r1, r2, r3 being Element of REAL holds Product <*r1,r2,r3*> = (r1 * r2) * r3

proof end;

theorem :: RVSUM_1:131

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

theorem :: RVSUM_1:132

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

theorem :: RVSUM_1:133

for F being FinSequence of REAL holds
( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 )

proof end;

theorem :: RVSUM_1:134

for i, j being Nat
for r being Element of REAL holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))

proof end;

theorem :: RVSUM_1:135

for i, j being Nat
for r being Element of REAL holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) by SETWOP_2:38;

theorem :: RVSUM_1:136

for i being Nat
for r1, r2 being Element of REAL holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))

proof end;

theorem Th137: :: RVSUM_1:137

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Product (mlt R1,R2) = (Product R1) * (Product R2)

proof end;

theorem :: RVSUM_1:138

for i being Nat
for r being Element of REAL
for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)

proof end;

theorem :: RVSUM_1:139

for i being Nat
for R being Element of i -tuples_on REAL holds Product (sqr R) = (Product R) ^2

proof end;