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 4
.= a * (1_ G) by GROUP_1:def 6
.= a by GROUP_1:def 5 ; :: 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 4
.= a * (1_ G) by GROUP_1:def 6
.= a by GROUP_1:def 5 ; :: 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 6
.= a by GROUP_1:def 5 ; :: 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 6
.= a by GROUP_1:def 5 ; :: 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 4; :: thesis: verum