let G be Group; :: thesis: for a, b, c being Element of G holds [.a,b.] |^ c = [.(a |^ c),(b |^ c).]
let a, b, c be Element of G; :: thesis: [.a,b.] |^ c = [.(a |^ c),(b |^ c).]
thus [.a,b.] |^ c = ((c ") * (((((a ") * (1_ G)) * (b ")) * a) * b)) * c by GROUP_1:def 4
.= ((c ") * (((((a ") * (c * (c "))) * (b ")) * a) * b)) * c by GROUP_1:def 5
.= ((c ") * ((((a ") * (c * (c "))) * (b ")) * (a * b))) * c by GROUP_1:def 3
.= ((c ") * (((a ") * (c * (c "))) * ((b ") * (a * b)))) * c by GROUP_1:def 3
.= ((c ") * ((a ") * ((c * (c ")) * ((b ") * (a * b))))) * c by GROUP_1:def 3
.= (((c ") * (a ")) * ((c * (c ")) * ((b ") * (a * b)))) * c by GROUP_1:def 3
.= (((c ") * (a ")) * (c * ((c ") * ((b ") * (a * b))))) * c by GROUP_1:def 3
.= (((a ") |^ c) * ((c ") * ((b ") * (a * b)))) * c by GROUP_1:def 3
.= (((a |^ c) ") * ((c ") * ((b ") * (a * b)))) * c by GROUP_3:26
.= (((a |^ c) ") * ((c ") * (((b ") * (1_ G)) * (a * b)))) * c by GROUP_1:def 4
.= (((a |^ c) ") * ((c ") * (((b ") * (c * (c "))) * (a * b)))) * c by GROUP_1:def 5
.= (((a |^ c) ") * ((c ") * ((b ") * ((c * (c ")) * (a * b))))) * c by GROUP_1:def 3
.= (((a |^ c) ") * (((c ") * (b ")) * ((c * (c ")) * (a * b)))) * c by GROUP_1:def 3
.= (((a |^ c) ") * (((c ") * (b ")) * (c * ((c ") * (a * b))))) * c by GROUP_1:def 3
.= (((a |^ c) ") * (((b ") |^ c) * ((c ") * (a * b)))) * c by GROUP_1:def 3
.= (((a |^ c) ") * (((b |^ c) ") * ((c ") * (a * b)))) * c by GROUP_3:26
.= (((a |^ c) ") * (((b |^ c) ") * ((c ") * ((a * (1_ G)) * b)))) * c by GROUP_1:def 4
.= (((a |^ c) ") * (((b |^ c) ") * ((c ") * ((a * (c * (c "))) * b)))) * c by GROUP_1:def 5
.= (((a |^ c) ") * (((b |^ c) ") * ((c ") * (a * ((c * (c ")) * b))))) * c by GROUP_1:def 3
.= (((a |^ c) ") * (((b |^ c) ") * (((c ") * a) * ((c * (c ")) * b)))) * c by GROUP_1:def 3
.= (((a |^ c) ") * (((b |^ c) ") * (((c ") * a) * (c * ((c ") * b))))) * c by GROUP_1:def 3
.= (((a |^ c) ") * (((b |^ c) ") * ((a |^ c) * ((c ") * b)))) * c by GROUP_1:def 3
.= ((a |^ c) ") * ((((b |^ c) ") * ((a |^ c) * ((c ") * b))) * c) by GROUP_1:def 3
.= ((a |^ c) ") * (((b |^ c) ") * (((a |^ c) * ((c ") * b)) * c)) by GROUP_1:def 3
.= ((a |^ c) ") * (((b |^ c) ") * ((a |^ c) * (b |^ c))) by GROUP_1:def 3
.= [.(a |^ c),(b |^ c).] by Th16 ; :: thesis: verum