for a, b being Element of (INT.Group 2) holds (inversions G) . (a * b) = ((inversions G) . a) * ((inversions G) . b)

proof

let a, b be Element of (INT.Group 2); :: thesis: (inversions G) . (a * b) = ((inversions G) . a) * ((inversions G) . b)
( a in INT.Group 2 & b in INT.Group 2 ) ;

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

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

hence ((inversions G) . a) * ((inversions G) . b) = (inversions G) . b by ThCommutationEq
.= (inversions G) . (a * b) by A1, ThMultTableINTGroup2 ;
:: thesis: verum

end;

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

hence ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a by ThCommutationEq
.= (inversions G) . (a * b) by A2, ThMultTableINTGroup2 ;
:: thesis: verum

end;

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

hence (inversions G) . (a * b) = ((inversions G) . a) * ((inversions G) . b) by ThCommutationEq2; :: thesis: verum

end;

end;

end;

hence inversions G is multiplicative by GROUP_6:def 6; :: thesis: verum