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

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