let f be real-valued positive FinSequence; :: thesis: for i, j being Nat
for a, b being positive Real st i in dom f & j in dom f & i <> j holds
Product (Replace (f,i,j,a,b)) = (((Product f) * a) * b) / ((f . i) * (f . j))
let i, j be Nat; :: thesis: for a, b being positive Real st i in dom f & j in dom f & i <> j holds
Product (Replace (f,i,j,a,b)) = (((Product f) * a) * b) / ((f . i) * (f . j))
let a, b be positive Real; :: thesis: ( i in dom f & j in dom f & i <> j implies Product (Replace (f,i,j,a,b)) = (((Product f) * a) * b) / ((f . i) * (f . j)) )
for n being Nat st n in dom (f +* (i,a)) holds
(f +* (i,a)) . n > 0

proof

let n be Nat; :: thesis: ( n in dom (f +* (i,a)) implies (f +* (i,a)) . n > 0 )
assume n in dom (f +* (i,a)) ; :: thesis: (f +* (i,a)) . n > 0
then A2: n in dom f by FUNCT_7:30;

per cases ( n = i or n <> i ) ;

suppose n = i ; :: thesis: (f +* (i,a)) . n > 0

hence (f +* (i,a)) . n > 0 by A2, FUNCT_7:31; :: thesis: verum

end;

suppose n <> i ; :: thesis: (f +* (i,a)) . n > 0

then (f +* (i,a)) . n = f . n by FUNCT_7:32;
hence (f +* (i,a)) . n > 0 by PosDef, A2; :: thesis: verum

end;

end;

end;

then S1: f +* (i,a) is positive ;
assume A0: ( i in dom f & j in dom f & i <> j ) ; :: thesis: Product (Replace (f,i,j,a,b)) = (((Product f) * a) * b) / ((f . i) * (f . j))
A1: j in dom (f +* (i,a)) by A0, FUNCT_7:30;
Product (Replace (f,i,j,a,b)) = ((Product (f +* (i,a))) * b) / ((f +* (i,a)) . j) by A1, ProductA, S1
.= ((Product (f +* (i,a))) * b) / (f . j) by FUNCT_7:32, A0
.= ((((Product f) * a) / (f . i)) * b) / (f . j) by A0, ProductA
.= ((((Product f) * a) * (1 / (f . i))) * b) / (f . j) by XCMPLX_1:99
.= ((((Product f) * a) * b) * (1 / (f . i))) * (1 / (f . j)) by XCMPLX_1:99
.= ((((Product f) * a) * b) / (f . i)) * (1 / (f . j)) by XCMPLX_1:99
.= ((((Product f) * a) * b) / (f . i)) / (f . j) by XCMPLX_1:99
.= (((Product f) * a) * b) / ((f . i) * (f . j)) by XCMPLX_1:78 ;
hence Product (Replace (f,i,j,a,b)) = (((Product f) * a) * b) / ((f . i) * (f . j)) ; :: thesis: verum