let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; :: thesis: for x being Element of L
for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds
(x ") |^ m = 1. L
let x be Element of L; :: thesis: for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds
(x ") |^ m = 1. L
let m be Element of NAT ; :: thesis: ( x <> 0. L & x |^ m = 1. L implies (x ") |^ m = 1. L )
assume ( x <> 0. L & x |^ m = 1. L ) ; :: thesis: (x ") |^ m = 1. L
then (1. L) * ((x ") |^ m) = 1. L by Lm7;
hence (x ") |^ m = 1. L ; :: thesis: verum