let G be Group; :: thesis: for a, b being Element of G holds
( [.a,b.] = (((a ") * (b ")) * a) * b & [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
let a, b be Element of G; :: thesis: ( [.a,b.] = (((a ") * (b ")) * a) * b & [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
thus [.a,b.] = (((a ") * (b ")) * a) * b ; :: thesis: ( [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
thus [.a,b.] = ((a ") * ((b ") * a)) * b by GROUP_1:def 3; :: thesis: ( [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
hence [.a,b.] = (a ") * (((b ") * a) * b) by GROUP_1:def 3; :: thesis: ( [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
hence [.a,b.] = (a ") * ((b ") * (a * b)) by GROUP_1:def 3; :: thesis: [.a,b.] = ((a ") * (b ")) * (a * b)
thus [.a,b.] = ((a ") * (b ")) * (a * b) by GROUP_1:def 3; :: thesis: verum