let G be non empty almost_cancelable well-unital associative almost_invertible multLoopStr_0 ; :: thesis: for a being Element of G st a <> 0. G holds
( (a ") * a = 1. G & a * (a ") = 1. G )
let a be Element of G; :: thesis: ( a <> 0. G implies ( (a ") * a = 1. G & a * (a ") = 1. G ) )
assume A1: a <> 0. G ; :: thesis: ( (a ") * a = 1. G & a * (a ") = 1. G )
hence A2: (a ") * a = 1. G by Def10; :: thesis: a * (a ") = 1. G
consider x being Element of G such that
A3: a * x = 1. G by A1, Def8;
((a ") * a) * x = (a ") * (1. G) by A3, GROUP_1:def 3;
then x = (a ") * (1. G) by A2;
hence a * (a ") = 1. G by A3; :: thesis: verum