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