let i be Nat; :: thesis: for r being real number
for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)
let r be real number ; :: thesis: for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)
let R be Element of i -tuples_on REAL ; :: thesis: Product (r * R) = (Product (i |-> r)) * (Product R)
reconsider s = r as Element of REAL by XREAL_0:def 1;
thus Product (r * R) = Product (mlt (i |-> s),R) by Th92
.= (Product (i |-> r)) * (Product R) by Th137 ; :: thesis: verum