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

( (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