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