theorem Th162: :: MATGRP_0:142

for G being Group holds inverse_op G = inverse_op multMagma(# the carrier of G, the multF of G #)