let G be Group; for a, b, c being Element of G holds [.a,(b * c).] = [.a,c.] * ([.a,b.] |^ c)
let a, b, c be Element of G; [.a,(b * c).] = [.a,c.] * ([.a,b.] |^ c)
thus [.a,(b * c).] =
((a ") * ((b * c) ")) * (a * (b * c))
by Th16
.=
((a ") * ((c ") * (b "))) * (a * (b * c))
by GROUP_1:17
.=
((a ") * (((c ") * (1_ G)) * (b "))) * (a * (b * c))
by GROUP_1:def 4
.=
((a ") * (((c ") * (a * (a "))) * (b "))) * (a * (b * c))
by GROUP_1:def 5
.=
((a ") * (((c ") * ((a * (1_ G)) * (a "))) * (b "))) * (a * (b * c))
by GROUP_1:def 4
.=
((a ") * (((c ") * ((a * (c * (c "))) * (a "))) * (b "))) * (a * (b * c))
by GROUP_1:def 5
.=
((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)) * ((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)) * ((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.] * (((c ") * (((a ") * (b ")) * (a * b))) * c)
by Th16
.=
[.a,c.] * ([.a,b.] |^ c)
by Th16
; verum