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) )
A1: ( Product <*a*> = a & Product <*c*> = c ) by FINSOP_1:11;
A2: ( Product <*a,b*> = a * b & Product <*b,c*> = b * c ) by FINSOP_1:12;
( <*a,b,c*> = <*a*> ^ <*b,c*> & <*a,b,c*> = <*a,b*> ^ <*c*> ) by FINSEQ_1:43;
hence ( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) ) by A1, A2, FINSOP_1:5; :: thesis: verum