let G be Group; :: thesis: for a, b, c being Element of G holds [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.]
let a, b, c be Element of G; :: thesis: [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.]
([.a,c.] * [.a,b.]) * [.a,b,c.] = [.a,c.] * ([.a,b.] * [.[.a,b.],c.]) by GROUP_1:def 3
.= [.a,c.] * ((((a ") * (b ")) * (a * b)) * (((([.a,b.] ") * (c ")) * [.a,b.]) * c)) by Th16
.= [.a,c.] * ((((a ") * (b ")) * (a * b)) * ((([.b,a.] * (c ")) * [.a,b.]) * c)) by Th22
.= [.a,c.] * ((((a ") * (b ")) * (a * b)) * ((((((b ") * (a ")) * (b * a)) * (c ")) * [.a,b.]) * c)) by Th16
.= [.a,c.] * (((a ") * (b ")) * ((a * b) * ((((((b ") * (a ")) * (b * a)) * (c ")) * [.a,b.]) * c))) by GROUP_1:def 3
.= [.a,c.] * (((a ") * (b ")) * ((a * b) * (((((b ") * (a ")) * (b * a)) * (c ")) * ([.a,b.] * c)))) by GROUP_1:def 3
.= [.a,c.] * (((a ") * (b ")) * ((a * b) * ((((b ") * (a ")) * (b * a)) * ((c ") * ([.a,b.] * c))))) by GROUP_1:def 3
.= [.a,c.] * (((a ") * (b ")) * (((a * b) * (((b ") * (a ")) * (b * a))) * ((c ") * ([.a,b.] * c)))) by GROUP_1:def 3
.= [.a,c.] * (((a ") * (b ")) * ((((a * b) * ((b ") * (a "))) * (b * a)) * ((c ") * ([.a,b.] * c)))) by GROUP_1:def 3
.= [.a,c.] * (((a ") * (b ")) * ((((a * b) * ((a * b) ")) * (b * a)) * ((c ") * ([.a,b.] * c)))) by GROUP_1:17
.= [.a,c.] * (((a ") * (b ")) * (((1_ G) * (b * a)) * ((c ") * ([.a,b.] * c)))) by GROUP_1:def 5
.= [.a,c.] * (((a ") * (b ")) * ((b * a) * ((c ") * ([.a,b.] * c)))) by GROUP_1:def 4
.= [.a,c.] * ((((a ") * (b ")) * (b * a)) * ((c ") * ([.a,b.] * c))) by GROUP_1:def 3
.= [.a,c.] * ((((b * a) ") * (b * a)) * ((c ") * ([.a,b.] * c))) by GROUP_1:17
.= [.a,c.] * ((1_ G) * ((c ") * ([.a,b.] * c))) by GROUP_1:def 5
.= [.a,c.] * ((c ") * ([.a,b.] * c)) by GROUP_1:def 4
.= (((a ") * (c ")) * (a * c)) * ((c ") * ([.a,b.] * c)) by Th16
.= (((a ") * (c ")) * (a * c)) * ((c ") * (((a ") * (((b ") * a) * b)) * c)) by Th16
.= (((a ") * (c ")) * (a * c)) * (((c ") * ((a ") * (((b ") * a) * b))) * c) by GROUP_1:def 3
.= (((a ") * (c ")) * (a * c)) * ((((c ") * (a ")) * (((b ") * a) * b)) * c) by GROUP_1:def 3
.= (((a ") * (c ")) * (a * c)) * (((c ") * (a ")) * ((((b ") * a) * b) * c)) by GROUP_1:def 3
.= ((((a ") * (c ")) * (a * c)) * ((c ") * (a "))) * ((((b ") * a) * b) * c) by GROUP_1:def 3
.= (((a ") * (c ")) * ((a * c) * ((c ") * (a ")))) * ((((b ") * a) * b) * c) by GROUP_1:def 3
.= (((a ") * (c ")) * ((a * c) * ((a * c) "))) * ((((b ") * a) * b) * c) by GROUP_1:17
.= (((a ") * (c ")) * (1_ G)) * ((((b ") * a) * b) * c) by GROUP_1:def 5
.= ((a ") * (c ")) * ((((b ") * a) * b) * c) by GROUP_1:def 4
.= (((a ") * (c ")) * (((b ") * a) * b)) * c by GROUP_1:def 3
.= (((a ") * (c ")) * ((b ") * (a * b))) * c by GROUP_1:def 3
.= ((((a ") * (c ")) * (b ")) * (a * b)) * c by GROUP_1:def 3
.= (((a ") * ((c ") * (b "))) * (a * b)) * c by GROUP_1:def 3
.= ((a ") * ((c ") * (b "))) * ((a * b) * c) by GROUP_1:def 3
.= ((a ") * ((c ") * (b "))) * (a * (b * c)) by GROUP_1:def 3
.= ((a ") * ((b * c) ")) * (a * (b * c)) by GROUP_1:17 ;
hence [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.] by Th16; :: thesis: verum