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