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 4; :: 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 4; :: thesis: ( [.a,b.] = (a " ) * ((b " ) * (a * b)) & [.a,b.] = ((a " ) * (b " )) * (a * b) )
hence [.a,b.] = (a " ) * ((b " ) * (a * b)) by GROUP_1:def 4; :: thesis: [.a,b.] = ((a " ) * (b " )) * (a * b)
thus [.a,b.] = ((a " ) * (b " )) * (a * b) by GROUP_1:def 4; :: thesis: verum