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