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

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