let G be multGroup; :: thesis: for a being Element of G holds
( (a ") * a = 1. G & a * (a ") = 1. G )
let a be Element of G; :: thesis: ( (a ") * a = 1. G & a * (a ") = 1. G )
thus A1: (a ") * a = 1. G by ALGSTR_0:def 30; :: thesis: a * (a ") = 1. G
A2: for a, b, c being Element of G holds (a * b) * c = a * (b * c) by Th11;
( ( for a being Element of G holds a * (1. G) = a ) & ( for a being Element of G ex x being Element of G st a * x = 1. G ) ) by Th11;
hence a * (a ") = 1. G by A1, A2, Lm11; :: thesis: verum