let G be strict commutative Group; :: thesis: for a, b being Element of (INT.Group 2) st b = 0 holds
( ((inversions G) . b) * ((inversions G) . a) = (inversions G) . a & ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a )
let a, b be Element of (INT.Group 2); :: thesis: ( b = 0 implies ( ((inversions G) . b) * ((inversions G) . a) = (inversions G) . a & ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a ) )
assume b = 0 ; :: thesis: ( ((inversions G) . b) * ((inversions G) . a) = (inversions G) . a & ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a )
then A1: (inversions G) . b = id G by DefInversions;
a in INT.Group 2 ;

per cases then ( a = 0 or a = 1 ) by EltsOfINTGroup2;

suppose a = 0 ; :: thesis: ( ((inversions G) . b) * ((inversions G) . a) = (inversions G) . a & ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a )

then A2: (inversions G) . a = id G by DefInversions;
thus ((inversions G) . b) * ((inversions G) . a) = (id G) * (id G) by A1, A2, AUTGROUP:8
.= (inversions G) . a by A2, FUNCT_2:17 ; :: thesis: ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a
thus ((inversions G) . a) * ((inversions G) . b) = (id G) * (id G) by A1, A2, AUTGROUP:8
.= (inversions G) . a by A2, FUNCT_2:17 ; :: thesis: verum

end;

suppose a = 1 ; :: thesis: ( ((inversions G) . b) * ((inversions G) . a) = (inversions G) . a & ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a )

then A3: (inversions G) . a = inverse_op G by DefInversions;
hence ((inversions G) . b) * ((inversions G) . a) = (id G) * (inverse_op G) by A1, AUTGROUP:8
.= (inversions G) . a by A3, FUNCT_2:17 ;
:: thesis: ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a
thus ((inversions G) . a) * ((inversions G) . b) = (inverse_op G) * (id G) by A1, A3, AUTGROUP:8
.= (inversions G) . a by A3, FUNCT_2:17 ; :: thesis: verum

end;

end;