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;