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