set G = doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #);

now :: thesis: for a being Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) st a <> 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) holds
a is left_invertible

let a be Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #); :: thesis: ( a <> 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) implies a is left_invertible )
assume A: a <> 0. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) ; :: thesis: a is left_invertible
reconsider x = a as Element of L ;
x <> 0. L by A;
then x is left_invertible by ALGSTR_0:def 39;
then consider y being Element of L such that
B: y * x = 1. L ;
reconsider b = y as Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) ;
b * a = 1. doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) by B;
hence a is left_invertible ; :: thesis: verum

end;

hence doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is almost_left_invertible ; :: thesis: verum