let G be Group; :: thesis: for a, b being Element of G holds
( (a * b) * (b ") = a & (a * (b ")) * b = a & ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
let a, b be Element of G; :: thesis: ( (a * b) * (b ") = a & (a * (b ")) * b = a & ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
thus A1: (a * b) * (b ") = a * (b * (b ")) by GROUP_1:def 3
.= a * (1_ G) by GROUP_1:def 5
.= a by GROUP_1:def 4 ; :: thesis: ( (a * (b ")) * b = a & ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
thus A2: (a * (b ")) * b = a * ((b ") * b) by GROUP_1:def 3
.= a * (1_ G) by GROUP_1:def 5
.= a by GROUP_1:def 4 ; :: thesis: ( ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
thus A3: ((b ") * b) * a = (1_ G) * a by GROUP_1:def 5
.= a by GROUP_1:def 4 ; :: thesis: ( (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
thus (b * (b ")) * a = (1_ G) * a by GROUP_1:def 5
.= a by GROUP_1:def 4 ; :: thesis: ( a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )
hence ( a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a ) by A1, A2, A3, GROUP_1:def 3; :: thesis: verum