let G be Group; :: thesis: inverse_op G = inverse_op multMagma(# the carrier of G, the multF of G #)
set UMG = the carrier of multMagma(# the carrier of G, the multF of G #);
set UG = the carrier of G;
reconsider H = multMagma(# the carrier of G, the multF of G #) as Subgroup of G by Th161;
thus inverse_op multMagma(# the carrier of G, the multF of G #) = inverse_op H
.= (inverse_op G) | the carrier of multMagma(# the carrier of G, the multF of G #) by GROUP_2:49
.= inverse_op G ; :: thesis: verum