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

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