let i, j be natural Number ; :: thesis: for r being Real holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))
let r be Real; :: thesis: Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))
reconsider i = i, j = j as Nat by TARSKI:1;
reconsider s = r as Element of REAL by XREAL_0:def 1;
Product ((i + j) |-> s) = multreal . ((multreal $$ (i |-> s)),(multreal $$ (j |-> s))) by SETWOP_2:26
.= (Product (i |-> s)) * (Product (j |-> s)) by BINOP_2:def 11 ;
hence Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r)) ; :: thesis: verum