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