theorem :: ALGSTR_1:13

for G being multGroup
for a being Element of G holds
( (a ") * a = 1. G & a * (a ") = 1. G )