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