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