let i be natural Number ; :: thesis: for r being Real
for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)
let r be Real; :: 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 Th63
.= (Product (i |-> r)) * (Product R) by Th107 ; :: thesis: verum