let L be non empty right_complementable add-associative right_zeroed distributive associative doubleLoopStr ; :: thesis: for k being odd Element of NAT
for x being Element of L holds (power L) . ((- x),k) = - ((power L) . (x,k))
let k be odd Element of NAT ; :: thesis: for x being Element of L holds (power L) . ((- x),k) = - ((power L) . (x,k))
let x be Element of L; :: thesis: (power L) . ((- x),k) = - ((power L) . (x,k))

per cases ( k = 0 or k >= 1 ) by NAT_1:14;

suppose k = 0 ; :: thesis: (power L) . ((- x),k) = - ((power L) . (x,k))

hence (power L) . ((- x),k) = - ((power L) . (x,k)) ; :: thesis: verum

end;

suppose k >= 1 ; :: thesis: (power L) . ((- x),k) = - ((power L) . (x,k))

then reconsider k1 = k - 1 as Element of NAT by INT_1:5;
A1: k1 + 1 = k ;
reconsider a = (power L) . ((- x),k1) as Element of L ;
reconsider b = (power L) . (x,k1) as Element of L ;
(power L) . ((- x),k1) = (power L) . (x,k1) by Th3;
hence (power L) . ((- x),k) = b * (- x) by A1, GROUP_1:def 7
.= - (b * x) by VECTSP_1:8
.= - ((power L) . (x,k)) by A1, GROUP_1:def 7 ;
:: thesis: verum

end;

end;