let i be Element of NAT ; :: thesis: for K being non empty associative commutative well-unital doubleLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Product (mlt R1,R2) = (Product R1) * (Product R2)
let K be non empty associative commutative well-unital doubleLoopStr ; :: thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds Product (mlt R1,R2) = (Product R1) * (Product R2)
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: Product (mlt R1,R2) = (Product R1) * (Product R2)
the multF of K is having_a_unity by Th11;
hence Product (mlt R1,R2) = (Product R1) * (Product R2) by SETWOP_2:46; :: thesis: verum