let G be Group; :: thesis: for a, b, c being Element of G holds
( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) )
let a, b, c be Element of G; :: thesis: ( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) )
( <*a,b,c*> = <*a*> ^ <*b,c*> & <*a,b,c*> = <*a,b*> ^ <*c*> & Product <*a*> = a & Product <*c*> = c & Product <*a,b*> = a * b & Product <*b,c*> = b * c ) by FINSEQ_1:60, FINSOP_1:12, FINSOP_1:13;
hence ( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) ) by Th8; :: thesis: verum