let f be real-valued positive FinSequence; :: thesis: for i being Nat
for a being Real st i in dom f holds
Product (f +* (i,a)) = ((Product f) * a) / (f . i)
let i be Nat; :: thesis: for a being Real st i in dom f holds
Product (f +* (i,a)) = ((Product f) * a) / (f . i)
let a be Real; :: thesis: ( i in dom f implies Product (f +* (i,a)) = ((Product f) * a) / (f . i) )
reconsider w = f as FinSequence of REAL by RVSUM_1:145;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
assume A1: i in dom f ; :: thesis: Product (f +* (i,a)) = ((Product f) * a) / (f . i)
then Z1: Product (w +* (i,a)) = Product (((w | (i -' 1)) ^ <*aa*>) ^ (w /^ i)) by CopyForValued
.= (Product ((w | (i -' 1)) ^ <*aa*>)) * (Product (w /^ i)) by RVSUM_1:97
.= ((Product (w | (i -' 1))) * (Product <*aa*>)) * (Product (w /^ i)) by RVSUM_1:97
.= aa * ((Product (w | (i -' 1))) * (Product (w /^ i)))
.= aa * (Product ((w | (i -' 1)) ^ (w /^ i))) by RVSUM_1:97 ;
reconsider fi = f . i as Real ;
ZZ: fi <> 0 by A1, PosDef;
( 1 <= i & i <= len w ) by A1, FINSEQ_3:25;
then zz: Product w = Product (((w | (i -' 1)) ^ <*(f . i)*>) ^ (w /^ i)) by FINSEQ_5:84
.= (Product ((w | (i -' 1)) ^ <*(f . i)*>)) * (Product (w /^ i)) by RVSUM_1:97
.= ((Product (w | (i -' 1))) * (Product <*(f . i)*>)) * (Product (w /^ i)) by RVSUM_1:97
.= fi * ((Product (w | (i -' 1))) * (Product (w /^ i)))
.= fi * (Product ((w | (i -' 1)) ^ (w /^ i))) by RVSUM_1:97 ;
Product (w +* (i,a)) = aa * ((Product w) / fi) by ZZ, XCMPLX_1:89, zz, Z1
.= aa * ((Product w) * (1 / fi)) by XCMPLX_1:99
.= ((Product w) * aa) * (1 / fi)
.= ((Product f) * a) / (f . i) by XCMPLX_1:99 ;
hence Product (f +* (i,a)) = ((Product f) * a) / (f . i) ; :: thesis: verum