let K be non empty associative commutative well-unital doubleLoopStr ; :: thesis: for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3
let a1, a2, a3 be Element of K; :: thesis: Product <*a1,a2,a3*> = (a1 * a2) * a3
thus Product <*a1,a2,a3*> = Product (<*a1,a2*> ^ <*a3*>) by FINSEQ_1:60
.= (Product <*a1,a2*>) * a3 by GROUP_4:9
.= (a1 * a2) * a3 by FINSOP_1:13 ; :: thesis: verum