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