let G be multGroup; :: thesis: for a being Element of holds
( (a " ) * a = 1. G & a * (a " ) = 1. G )
let a be Element of ; :: 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 holds (a * b) * c = a * (b * c) by Th22;
( ( for a being Element of holds a * (1. G) = a ) & ( for a being Element of ex x being Element of st a * x = 1. G ) ) by Th22;
hence a * (a " ) = 1. G by A1, A2, Lm11; :: thesis: verum