let i be natural Number ; :: 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)
i is Nat by TARSKI:1;
hence Product (mlt (R1,R2)) = multreal . ((multreal $$ R1),(multreal $$ R2)) by SETWOP_2:35
.= (Product R1) * (Product R2) by BINOP_2:def 11 ;
:: thesis: verum