for x, y being Element of A holds (inverse_op A) . (x * y) = ((inverse_op A) . x) * ((inverse_op A) . y)

proof

let x, y be Element of A; :: thesis: (inverse_op A) . (x * y) = ((inverse_op A) . x) * ((inverse_op A) . y)
thus (inverse_op A) . (x * y) = (x * y) " by GROUP_1:def 6
.= (y ") * (x ") by GROUP_1:17
.= (x ") * ((inverse_op A) . y) by GROUP_1:def 6
.= ((inverse_op A) . x) * ((inverse_op A) . y) by GROUP_1:def 6 ; :: thesis: verum

end;

hence inverse_op A is multiplicative ; :: thesis: verum