let i be Element of NAT ; :: thesis: for K being non empty associative commutative well-unital doubleLoopStr
for a1, a2 being Element of K holds Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2))
let K be non empty associative commutative well-unital doubleLoopStr ; :: thesis: for a1, a2 being Element of K holds Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2))
let a1, a2 be Element of K; :: thesis: Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2))
thus Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2)) by SETWOP_2:36; :: thesis: verum