let G be Group; for a, b, c being Element of G holds [.a,(b " ),c.] |^ b = [.([.a,(b " ).] |^ b),(c |^ b).]
let a, b, c be Element of G; [.a,(b " ),c.] |^ b = [.([.a,(b " ).] |^ b),(c |^ b).]
A1: [.a,(b " ),c.] |^ b =
((b " ) * ((((([.a,(b " ).] " ) * (1_ G)) * (c " )) * [.a,(b " ).]) * c)) * b
by GROUP_1:def 5
.=
((b " ) * ((((([.a,(b " ).] " ) * (b * (b " ))) * (c " )) * [.a,(b " ).]) * c)) * b
by GROUP_1:def 6
.=
((b " ) * (((((([.a,(b " ).] " ) * b) * (b " )) * (c " )) * [.a,(b " ).]) * c)) * b
by GROUP_1:def 4
.=
((b " ) * ((((([.a,(b " ).] " ) * b) * (b " )) * (c " )) * ([.a,(b " ).] * c))) * b
by GROUP_1:def 4
.=
((b " ) * (((([.a,(b " ).] " ) * b) * (b " )) * ((c " ) * ([.a,(b " ).] * c)))) * b
by GROUP_1:def 4
.=
((b " ) * ((([.a,(b " ).] " ) * b) * ((b " ) * ((c " ) * ([.a,(b " ).] * c))))) * b
by GROUP_1:def 4
.=
(((b " ) * (([.a,(b " ).] " ) * b)) * ((b " ) * ((c " ) * ([.a,(b " ).] * c)))) * b
by GROUP_1:def 4
.=
((([.a,(b " ).] " ) |^ b) * ((b " ) * ((c " ) * ([.a,(b " ).] * c)))) * b
by GROUP_1:def 4
.=
(([.a,(b " ).] " ) |^ b) * (((b " ) * ((c " ) * ([.a,(b " ).] * c))) * b)
by GROUP_1:def 4
.=
(([.a,(b " ).] " ) |^ b) * (([.a,(b " ).] |^ c) |^ b)
by GROUP_1:def 4
.=
([.(b " ),a.] |^ b) * (([.a,(b " ).] |^ c) |^ b)
by GROUP_5:25
.=
([.(b " ),a.] |^ b) * ([.a,(b " ).] |^ (c * b))
by GROUP_3:29
;
[.([.a,(b " ).] |^ b),(c |^ b).] =
((([.(b " ),a.] |^ b) * ((c |^ b) " )) * ([.a,(b " ).] |^ b)) * (c |^ b)
by Th4
.=
((([.(b " ),a.] |^ b) * ((c " ) |^ b)) * ([.a,(b " ).] |^ b)) * (c |^ b)
by GROUP_3:32
.=
((([.(b " ),a.] |^ b) * (((b " ) * (c " )) * b)) * (((b " ) * [.a,(b " ).]) * b)) * ((b " ) * (c * b))
by GROUP_1:def 4
.=
(([.(b " ),a.] |^ b) * (((b " ) * (c " )) * b)) * ((((b " ) * [.a,(b " ).]) * b) * ((b " ) * (c * b)))
by GROUP_1:def 4
.=
(([.(b " ),a.] |^ b) * (((b " ) * (c " )) * b)) * (((b " ) * [.a,(b " ).]) * (b * ((b " ) * (c * b))))
by GROUP_1:def 4
.=
(([.(b " ),a.] |^ b) * (((b " ) * (c " )) * b)) * (((b " ) * [.a,(b " ).]) * ((b * (b " )) * (c * b)))
by GROUP_1:def 4
.=
(([.(b " ),a.] |^ b) * (((b " ) * (c " )) * b)) * (((b " ) * [.a,(b " ).]) * ((1_ G) * (c * b)))
by GROUP_1:def 6
.=
(([.(b " ),a.] |^ b) * (((b " ) * (c " )) * b)) * (((b " ) * [.a,(b " ).]) * (c * b))
by GROUP_1:def 5
.=
([.(b " ),a.] |^ b) * ((((b " ) * (c " )) * b) * (((b " ) * [.a,(b " ).]) * (c * b)))
by GROUP_1:def 4
.=
([.(b " ),a.] |^ b) * (((b " ) * (c " )) * (b * (((b " ) * [.a,(b " ).]) * (c * b))))
by GROUP_1:def 4
.=
([.(b " ),a.] |^ b) * (((b " ) * (c " )) * ((b * ((b " ) * [.a,(b " ).])) * (c * b)))
by GROUP_1:def 4
.=
([.(b " ),a.] |^ b) * (((b " ) * (c " )) * (((b * (b " )) * [.a,(b " ).]) * (c * b)))
by GROUP_1:def 4
.=
([.(b " ),a.] |^ b) * (((b " ) * (c " )) * (((1_ G) * [.a,(b " ).]) * (c * b)))
by GROUP_1:def 6
.=
([.(b " ),a.] |^ b) * (((b " ) * (c " )) * ([.a,(b " ).] * (c * b)))
by GROUP_1:def 5
.=
([.(b " ),a.] |^ b) * ((((b " ) * (c " )) * [.a,(b " ).]) * (c * b))
by GROUP_1:def 4
.=
([.(b " ),a.] |^ b) * ([.a,(b " ).] |^ (c * b))
by GROUP_1:25
;
hence
[.a,(b " ),c.] |^ b = [.([.a,(b " ).] |^ b),(c |^ b).]
by A1; verum