let L be non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; :: thesis: for i being Integer holds pow (1. L),i = 1. L
let i be Integer; :: thesis: pow (1. L),i = 1. L

per cases ( 0 <= i or 0 > i ) ;

suppose 0 <= i ; :: thesis: pow (1. L),i = 1. L

then i is Element of NAT by INT_1:16;
hence pow (1. L),i = 1. L by Lm5; :: thesis: verum

end;

suppose A1: 0 > i ; :: thesis: pow (1. L),i = 1. L

A2: ( 1. L <> 0. L & (1. L) * (1. L) = 1. L ) by VECTSP_1:def 13;
A3: pow (1. L),(abs i) = 1. L by Lm5;
pow (1. L),i = ((power L) . (1. L),(abs i)) " by A1, Def3
.= (1. L) " by A3, Def3 ;
hence pow (1. L),i = 1. L by A2, VECTSP_1:def 22; :: thesis: verum

end;

end;