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 5
.= a by Th24 ; :: thesis: (a |^ (b ")) |^ b = a
thus (a |^ (b ")) |^ b = a |^ ((b ") * b) by Th29
.= a |^ (1_ G) by GROUP_1:def 5
.= a by Th24 ; :: thesis: verum