let i, j be Nat; :: thesis: for r being real number holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))
let r be real number ; :: thesis: Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))
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:37
.= (Product (i |-> s)) * (Product (j |-> s)) by BINOP_2:def 11 ;
hence Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r)) ; :: thesis: verum