let L be non empty doubleLoopStr ; :: thesis: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) implies for a being Element of L st a <> 0. L holds
ex x being Element of L st x * a = 1. L )
assume that
A1: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) ) and
A2: for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L and
A3: ( ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) ) ; :: thesis: for a being Element of L st a <> 0. L holds
ex x being Element of L st x * a = 1. L
let a be Element of L; :: thesis: ( a <> 0. L implies ex x being Element of L st x * a = 1. L )
assume a <> 0. L ; :: thesis: ex x being Element of L st x * a = 1. L
then consider x being Element of L such that
A4: a * x = 1. L by A2;
x * a = 1. L by A1, A2, A3, A4, Lm6;
hence ex x being Element of L st x * a = 1. L ; :: thesis: verum