let G be Group; :: thesis: for a, b being Element of G holds
( (a |^ b) |^ (b " ) = a & (a |^ (b " )) |^ b = a )
let a, b be Element of G; :: thesis: ( (a |^ b) |^ (b " ) = a & (a |^ (b " )) |^ b = a )
thus (a |^ b) |^ (b " ) = a |^ (b * (b " )) by Th29
.= a |^ (1_ G) by GROUP_1:def 6
.= a by Th24 ; :: thesis: (a |^ (b " )) |^ b = a
thus (a |^ (b " )) |^ b = a |^ ((b " ) * b) by Th29
.= a |^ (1_ G) by GROUP_1:def 6
.= a by Th24 ; :: thesis: verum