let L be non empty non degenerated almost_left_invertible associative commutative well-unital distributive 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 A1: ( x <> 0. L & (x " ) |^ i = 1. L ) ; :: thesis: x |^ i = 1. L
A2: 1_ L = x |^ 0 by BINOM:8;
((x " ) |^ i) * (1. L) = 1. L by A1, VECTSP_1:def 13;
then ((x " ) |^ i) * (x |^ 0 ) = ((x " ) |^ i) * (x |^ i) by A1, A2, Lm7;
hence x |^ i = 1. L by A1, A2, VECTSP_1:33; :: thesis: verum