let G be non empty almost_cancelable associative well-unital 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 Def27; :: thesis: a * (a " ) = 1. G
consider x being Element of G such that
A3: a * x = 1. G by A1, Def24;
((a " ) * a) * x = (a " ) * (1. G) by A3, GROUP_1:def 4;
then x = (a " ) * (1. G) by A2, VECTSP_1:def 19;
hence a * (a " ) = 1. G by A3, VECTSP_1:def 13; :: thesis: verum