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