let R1, R2 be FinSequence of REAL ; :: thesis: for n, i being Nat
for r being Real st i in dom R1 & R1 = n |-> 1 & R2 = R1 +* (i,r) holds
Product R2 = r
let n, i be Nat; :: thesis: for r being Real st i in dom R1 & R1 = n |-> 1 & R2 = R1 +* (i,r) holds
Product R2 = r
let r be Real; :: thesis: ( i in dom R1 & R1 = n |-> 1 & R2 = R1 +* (i,r) implies Product R2 = r )
assume that
A1: i in dom R1 and
A2: R1 = n |-> 1 and
A3: R2 = R1 +* (i,r) ; :: thesis: Product R2 = r
i in Seg n by A1, A2, FUNCT_2:def 1;
then A4: R1 . i = 1 by A2, FUNCOP_1:7;
A5: Product R1 = 1 by A2, RVSUM_1:102;
thus Product R2 = ((Product R1) * r) / (R1 . i) by A1, A2, A3, RVSUM_3:25
.= r by A4, A5 ; :: thesis: verum