let rr be Real; :: thesis: for n being Nat holds Product ((n + 1) |-> rr) = (Product (n |-> rr)) * rr
let n be Nat; :: thesis: Product ((n + 1) |-> rr) = (Product (n |-> rr)) * rr
thus Product ((n + 1) |-> rr) = (Product (n |-> rr)) * (Product (1 |-> rr)) by RVSUM_1:104
.= (Product (n |-> rr)) * rr by Th4 ; :: thesis: verum