let r be Real; :: thesis: for f being real-valued FinSequence

for i being Nat st i in dom f holds

Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)

let f be real-valued FinSequence; :: thesis: for i being Nat st i in dom f holds

Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)

let i be Nat; :: thesis: ( i in dom f implies Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2) )

assume A1: i in dom f ; :: thesis: Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)

reconsider fi = f . i as Element of REAL by XREAL_0:def 1;

set F = @ (@ f);

set G = (@ (@ f)) | (i -' 1);

set H = (@ (@ f)) /^ i;

A2: sqr <*fi*> = <*(fi ^2)*> by RVSUM_1:55;

@ (@ f) = (@ (@ f)) +* (i,fi) by FUNCT_7:35

.= (((@ (@ f)) | (i -' 1)) ^ <*fi*>) ^ ((@ (@ f)) /^ i) by A1, FUNCT_7:98 ;

then sqr (@ (@ f)) = (sqr (((@ (@ f)) | (i -' 1)) ^ <*fi*>)) ^ (sqr ((@ (@ f)) /^ i)) by RVSUM_1:144

.= ((sqr ((@ (@ f)) | (i -' 1))) ^ (sqr <*fi*>)) ^ (sqr ((@ (@ f)) /^ i)) by RVSUM_1:144 ;

then A3: Sum (sqr (@ (@ f))) = (Sum ((sqr ((@ (@ f)) | (i -' 1))) ^ (sqr <*fi*>))) + (Sum (sqr ((@ (@ f)) /^ i))) by RVSUM_1:75

.= ((Sum (sqr ((@ (@ f)) | (i -' 1)))) + (fi ^2)) + (Sum (sqr ((@ (@ f)) /^ i))) by A2, RVSUM_1:74 ;

reconsider R = r as Element of REAL by XREAL_0:def 1;

A4: sqr <*R*> = <*(R ^2)*> by RVSUM_1:55;

(@ (@ f)) +* (i,R) = (((@ (@ f)) | (i -' 1)) ^ <*R*>) ^ ((@ (@ f)) /^ i) by A1, FUNCT_7:98;

then sqr ((@ (@ f)) +* (i,R)) = (sqr (((@ (@ f)) | (i -' 1)) ^ <*R*>)) ^ (sqr ((@ (@ f)) /^ i)) by RVSUM_1:144

.= ((sqr ((@ (@ f)) | (i -' 1))) ^ (sqr <*R*>)) ^ (sqr ((@ (@ f)) /^ i)) by RVSUM_1:144 ;

then Sum (sqr ((@ (@ f)) +* (i,R))) = (Sum ((sqr ((@ (@ f)) | (i -' 1))) ^ (sqr <*R*>))) + (Sum (sqr ((@ (@ f)) /^ i))) by RVSUM_1:75

.= ((Sum (sqr ((@ (@ f)) | (i -' 1)))) + (R ^2)) + (Sum (sqr ((@ (@ f)) /^ i))) by A4, RVSUM_1:74 ;

hence Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2) by A3; :: thesis: verum

for i being Nat st i in dom f holds

Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)

let f be real-valued FinSequence; :: thesis: for i being Nat st i in dom f holds

Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)

let i be Nat; :: thesis: ( i in dom f implies Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2) )

assume A1: i in dom f ; :: thesis: Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2)

reconsider fi = f . i as Element of REAL by XREAL_0:def 1;

set F = @ (@ f);

set G = (@ (@ f)) | (i -' 1);

set H = (@ (@ f)) /^ i;

A2: sqr <*fi*> = <*(fi ^2)*> by RVSUM_1:55;

@ (@ f) = (@ (@ f)) +* (i,fi) by FUNCT_7:35

.= (((@ (@ f)) | (i -' 1)) ^ <*fi*>) ^ ((@ (@ f)) /^ i) by A1, FUNCT_7:98 ;

then sqr (@ (@ f)) = (sqr (((@ (@ f)) | (i -' 1)) ^ <*fi*>)) ^ (sqr ((@ (@ f)) /^ i)) by RVSUM_1:144

.= ((sqr ((@ (@ f)) | (i -' 1))) ^ (sqr <*fi*>)) ^ (sqr ((@ (@ f)) /^ i)) by RVSUM_1:144 ;

then A3: Sum (sqr (@ (@ f))) = (Sum ((sqr ((@ (@ f)) | (i -' 1))) ^ (sqr <*fi*>))) + (Sum (sqr ((@ (@ f)) /^ i))) by RVSUM_1:75

.= ((Sum (sqr ((@ (@ f)) | (i -' 1)))) + (fi ^2)) + (Sum (sqr ((@ (@ f)) /^ i))) by A2, RVSUM_1:74 ;

reconsider R = r as Element of REAL by XREAL_0:def 1;

A4: sqr <*R*> = <*(R ^2)*> by RVSUM_1:55;

(@ (@ f)) +* (i,R) = (((@ (@ f)) | (i -' 1)) ^ <*R*>) ^ ((@ (@ f)) /^ i) by A1, FUNCT_7:98;

then sqr ((@ (@ f)) +* (i,R)) = (sqr (((@ (@ f)) | (i -' 1)) ^ <*R*>)) ^ (sqr ((@ (@ f)) /^ i)) by RVSUM_1:144

.= ((sqr ((@ (@ f)) | (i -' 1))) ^ (sqr <*R*>)) ^ (sqr ((@ (@ f)) /^ i)) by RVSUM_1:144 ;

then Sum (sqr ((@ (@ f)) +* (i,R))) = (Sum ((sqr ((@ (@ f)) | (i -' 1))) ^ (sqr <*R*>))) + (Sum (sqr ((@ (@ f)) /^ i))) by RVSUM_1:75

.= ((Sum (sqr ((@ (@ f)) | (i -' 1)))) + (R ^2)) + (Sum (sqr ((@ (@ f)) /^ i))) by A4, RVSUM_1:74 ;

hence Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2) by A3; :: thesis: verum