let i be Nat; :: thesis: for K being non empty associative commutative well-unital doubleLoopStr
for a being Element of K
for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)
let K be non empty associative commutative well-unital doubleLoopStr ; :: thesis: for a being Element of K
for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)
let a be Element of K; :: thesis: for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)
let R1 be Element of i -tuples_on the carrier of K; :: thesis: Product (a * R1) = (Product (i |-> a)) * (Product R1)
thus Product (a * R1) = Product (mlt ((i |-> a),R1)) by Th66
.= (Product (i |-> a)) * (Product R1) by Th86 ; :: thesis: verum