let G be Group; :: thesis: 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; :: thesis: [.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 4
.= ((b ") * ((((([.a,(b ").] ") * (b * (b "))) * (c ")) * [.a,(b ").]) * c)) * b by GROUP_1:def 5
.= ((b ") * (((((([.a,(b ").] ") * b) * (b ")) * (c ")) * [.a,(b ").]) * c)) * b by GROUP_1:def 3
.= ((b ") * ((((([.a,(b ").] ") * b) * (b ")) * (c ")) * ([.a,(b ").] * c))) * b by GROUP_1:def 3
.= ((b ") * (((([.a,(b ").] ") * b) * (b ")) * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def 3
.= ((b ") * ((([.a,(b ").] ") * b) * ((b ") * ((c ") * ([.a,(b ").] * c))))) * b by GROUP_1:def 3
.= (((b ") * (([.a,(b ").] ") * b)) * ((b ") * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def 3
.= ((([.a,(b ").] ") |^ b) * ((b ") * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def 3
.= (([.a,(b ").] ") |^ b) * (((b ") * ((c ") * ([.a,(b ").] * c))) * b) by GROUP_1:def 3
.= (([.a,(b ").] ") |^ b) * (([.a,(b ").] |^ c) |^ b) by GROUP_1:def 3
.= ([.(b "),a.] |^ b) * (([.a,(b ").] |^ c) |^ b) by GROUP_5:22
.= ([.(b "),a.] |^ b) * ([.a,(b ").] |^ (c * b)) by GROUP_3:24 ;
[.([.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:26
.= ((([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * b)) * ((b ") * (c * b)) by GROUP_1:def 3
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * ((((b ") * [.a,(b ").]) * b) * ((b ") * (c * b))) by GROUP_1:def 3
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * (b * ((b ") * (c * b)))) by GROUP_1:def 3
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * ((b * (b ")) * (c * b))) by GROUP_1:def 3
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * ((1_ G) * (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 3
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (b * (((b ") * [.a,(b ").]) * (c * b)))) by GROUP_1:def 3
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * ((b * ((b ") * [.a,(b ").])) * (c * b))) by GROUP_1:def 3
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (((b * (b ")) * [.a,(b ").]) * (c * b))) by GROUP_1:def 3
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (((1_ G) * [.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) * ((((b ") * (c ")) * [.a,(b ").]) * (c * b)) by GROUP_1:def 3
.= ([.(b "),a.] |^ b) * ([.a,(b ").] |^ (c * b)) by GROUP_1:17 ;
hence [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] by A1; :: thesis: verum