let i be natural Number ; :: thesis: for r1, r2 being Real holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))
let r1, r2 be Real; :: thesis: Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))
reconsider i = i as Nat by TARSKI:1;
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;
reconsider ss = s1 * s2 as Element of REAL ;
Product (i |-> ss) = multreal $$ (i |-> (multreal . (s1,s2))) by BINOP_2:def 11
.= multreal . ((multreal $$ (i |-> s1)),(multreal $$ (i |-> s2))) by SETWOP_2:36
.= (Product (i |-> s1)) * (Product (i |-> s2)) by BINOP_2:def 11 ;
hence Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2)) ; :: thesis: verum