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