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