let G be Group; :: thesis: for a, b being Element of G holds
( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )
let a, b be Element of G; :: thesis: ( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )
thus [.a,b,(1_ G).] = 1_ G by Th22; :: thesis: ( [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )
thus [.a,(1_ G),b.] = [.(1_ G),b.] by Th22
.= 1_ G by Th22 ; :: thesis: [.(1_ G),a,b.] = 1_ G
thus [.(1_ G),a,b.] = [.(1_ G),b.] by Th22
.= 1_ G by Th22 ; :: thesis: verum