let G be Group; :: thesis: (inverse_op G) * (inverse_op G) = id G
for x being Element of the carrier of G holds ((inverse_op G) * (inverse_op G)) . x = (id G) . x

proof

let x be Element of the carrier of G; :: thesis: ((inverse_op G) * (inverse_op G)) . x = (id G) . x
thus ((inverse_op G) * (inverse_op G)) . x = (inverse_op G) . ((inverse_op G) . x) by FUNCT_2:15
.= (inverse_op G) . (x ") by GROUP_1:def 6
.= (x ") " by GROUP_1:def 6
.= (id G) . x ; :: thesis: verum

end;

hence (inverse_op G) * (inverse_op G) = id G by FUNCT_2:def 8; :: thesis: verum