let R1, R2 be FinSequence of REAL ; 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; for r being Real st i in dom R1 & R1 = n |-> 1 & R2 = R1 +* (i,r) holds
Product R2 = r
let r be Real; ( 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)
; 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
; verum