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 4
.= [.a,c.] * ((((a " ) * (b " )) * (a * b)) * (((([.a,b.] " ) * (c " )) * [.a,b.]) * c)) by Th19
.= [.a,c.] * ((((a " ) * (b " )) * (a * b)) * ((([.b,a.] * (c " )) * [.a,b.]) * c)) by Th25
.= [.a,c.] * ((((a " ) * (b " )) * (a * b)) * ((((((b " ) * (a " )) * (b * a)) * (c " )) * [.a,b.]) * c)) by Th19
.= [.a,c.] * (((a " ) * (b " )) * ((a * b) * ((((((b " ) * (a " )) * (b * a)) * (c " )) * [.a,b.]) * c))) by GROUP_1:def 4
.= [.a,c.] * (((a " ) * (b " )) * ((a * b) * (((((b " ) * (a " )) * (b * a)) * (c " )) * ([.a,b.] * c)))) by GROUP_1:def 4
.= [.a,c.] * (((a " ) * (b " )) * ((a * b) * ((((b " ) * (a " )) * (b * a)) * ((c " ) * ([.a,b.] * c))))) by GROUP_1:def 4
.= [.a,c.] * (((a " ) * (b " )) * (((a * b) * (((b " ) * (a " )) * (b * a))) * ((c " ) * ([.a,b.] * c)))) by GROUP_1:def 4
.= [.a,c.] * (((a " ) * (b " )) * ((((a * b) * ((b " ) * (a " ))) * (b * a)) * ((c " ) * ([.a,b.] * c)))) by GROUP_1:def 4
.= [.a,c.] * (((a " ) * (b " )) * ((((a * b) * ((a * b) " )) * (b * a)) * ((c " ) * ([.a,b.] * c)))) by GROUP_1:25
.= [.a,c.] * (((a " ) * (b " )) * (((1_ G) * (b * a)) * ((c " ) * ([.a,b.] * c)))) by GROUP_1:def 6
.= [.a,c.] * (((a " ) * (b " )) * ((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.] * ((((b * a) " ) * (b * a)) * ((c " ) * ([.a,b.] * c))) by GROUP_1:25
.= [.a,c.] * ((1_ G) * ((c " ) * ([.a,b.] * c))) by GROUP_1:def 6
.= [.a,c.] * ((c " ) * ([.a,b.] * c)) by GROUP_1:def 5
.= (((a " ) * (c " )) * (a * c)) * ((c " ) * ([.a,b.] * c)) by Th19
.= (((a " ) * (c " )) * (a * c)) * ((c " ) * (((a " ) * (((b " ) * a) * b)) * c)) by Th19
.= (((a " ) * (c " )) * (a * c)) * (((c " ) * ((a " ) * (((b " ) * a) * b))) * c) by GROUP_1:def 4
.= (((a " ) * (c " )) * (a * c)) * ((((c " ) * (a " )) * (((b " ) * a) * b)) * c) by GROUP_1:def 4
.= (((a " ) * (c " )) * (a * c)) * (((c " ) * (a " )) * ((((b " ) * a) * b) * c)) by GROUP_1:def 4
.= ((((a " ) * (c " )) * (a * c)) * ((c " ) * (a " ))) * ((((b " ) * a) * b) * c) by GROUP_1:def 4
.= (((a " ) * (c " )) * ((a * c) * ((c " ) * (a " )))) * ((((b " ) * a) * b) * c) by GROUP_1:def 4
.= (((a " ) * (c " )) * ((a * c) * ((a * c) " ))) * ((((b " ) * a) * b) * c) by GROUP_1:25
.= (((a " ) * (c " )) * (1_ G)) * ((((b " ) * a) * b) * c) by GROUP_1:def 6
.= ((a " ) * (c " )) * ((((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 4
.= ((((a " ) * (c " )) * (b " )) * (a * b)) * c by GROUP_1:def 4
.= (((a " ) * ((c " ) * (b " ))) * (a * b)) * c by GROUP_1:def 4
.= ((a " ) * ((c " ) * (b " ))) * ((a * b) * c) by GROUP_1:def 4
.= ((a " ) * ((c " ) * (b " ))) * (a * (b * c)) by GROUP_1:def 4
.= ((a " ) * ((b * c) " )) * (a * (b * c)) by GROUP_1:25 ;
hence [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.] by Th19; :: thesis: verum