let L be non empty non degenerated almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; :: thesis: for x being Element of L
for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds
x |^ i = 1. L
let x be Element of L; :: thesis: for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds
x |^ i = 1. L
let i be Element of NAT ; :: thesis: ( x <> 0. L & (x ") |^ i = 1. L implies x |^ i = 1. L )
assume that
A1: x <> 0. L and
A2: (x ") |^ i = 1. L ; :: thesis: x |^ i = 1. L
A3: 1_ L = x |^ 0 by BINOM:8;
((x ") |^ i) * (1. L) = 1. L by A2;
then ((x ") |^ i) * (x |^ 0) = ((x ") |^ i) * (x |^ i) by A1, A3, Lm7;
hence x |^ i = 1. L by A1, A2, A3, VECTSP_1:5; :: thesis: verum