let G be Group; 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; [.(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; verum