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 (i |-> a)) * (Product (j |-> a))
let K be non empty associative commutative well-unital doubleLoopStr ; :: thesis: for a being Element of K holds Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a))
let a be Element of K; :: thesis: Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a))
thus Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a)) by SETWOP_2:26; :: thesis: verum