let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; :: thesis: for m being Element of NAT

for x being Element of L st x <> 0. L holds

(x |^ m) * ((x ") |^ m) = 1. L

let m be Element of NAT ; :: thesis: for x being Element of L st x <> 0. L holds

(x |^ m) * ((x ") |^ m) = 1. L

let x be Element of L; :: thesis: ( x <> 0. L implies (x |^ m) * ((x ") |^ m) = 1. L )

assume A1: x <> 0. L ; :: thesis: (x |^ m) * ((x ") |^ m) = 1. L

(x |^ m) * ((x ") |^ m) = (x * (x ")) |^ m by BINOM:9

.= (1. L) |^ m by A1, VECTSP_1:def 10

.= 1. L by Lm6 ;

hence (x |^ m) * ((x ") |^ m) = 1. L ; :: thesis: verum

for x being Element of L st x <> 0. L holds

(x |^ m) * ((x ") |^ m) = 1. L

let m be Element of NAT ; :: thesis: for x being Element of L st x <> 0. L holds

(x |^ m) * ((x ") |^ m) = 1. L

let x be Element of L; :: thesis: ( x <> 0. L implies (x |^ m) * ((x ") |^ m) = 1. L )

assume A1: x <> 0. L ; :: thesis: (x |^ m) * ((x ") |^ m) = 1. L

(x |^ m) * ((x ") |^ m) = (x * (x ")) |^ m by BINOM:9

.= (1. L) |^ m by A1, VECTSP_1:def 10

.= 1. L by Lm6 ;

hence (x |^ m) * ((x ") |^ m) = 1. L ; :: thesis: verum