let G be Group; :: thesis: for a, b being Element of G holds
( [.(a " ),(b " ).] = [.a,b.] |^ ((a * b) " ) & [.(a " ),(b " ).] = [.a,b.] |^ ((b * a) " ) )
let a, b be Element of G; :: thesis: ( [.(a " ),(b " ).] = [.a,b.] |^ ((a * b) " ) & [.(a " ),(b " ).] = [.a,b.] |^ ((b * a) " ) )
thus [.(a " ),(b " ).] = [.(b " ),a.] |^ (a " ) by Th30
.= ([.a,b.] |^ (b " )) |^ (a " ) by Th30
.= [.a,b.] |^ ((b " ) * (a " )) by GROUP_3:29
.= [.a,b.] |^ ((a * b) " ) by GROUP_1:25 ; :: thesis: [.(a " ),(b " ).] = [.a,b.] |^ ((b * a) " )
thus [.(a " ),(b " ).] = [.b,(a " ).] |^ (b " ) by Th31
.= ([.a,b.] |^ (a " )) |^ (b " ) by Th31
.= [.a,b.] |^ ((a " ) * (b " )) by GROUP_3:29
.= [.a,b.] |^ ((b * a) " ) by GROUP_1:25 ; :: thesis: verum