let r be Real; :: thesis: for n being Element of NAT holds Product ((n + 1) |-> r) = (Product (n |-> r)) * r
let n be Element of NAT ; :: thesis: Product ((n + 1) |-> r) = (Product (n |-> r)) * r
thus Product ((n + 1) |-> r) = (Product (n |-> r)) * (Product (1 |-> r)) by RVSUM_1:104
.= (Product (n |-> r)) * r by Th10 ; :: thesis: verum