let i be Nat; :: thesis: for R1, R2 being Element of i -tuples_on REAL holds Product (mlt R1,R2) = (Product R1) * (Product R2)
let R1, R2 be Element of i -tuples_on REAL ; :: thesis: Product (mlt R1,R2) = (Product R1) * (Product R2)
thus Product (mlt R1,R2) = multreal . (multreal $$ R1),(multreal $$ R2) by SETWOP_2:46
.= (Product R1) * (Product R2) by Lm1 ; :: thesis: verum