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

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