let L be non empty non degenerated almost_left_invertible well-unital distributive associative commutative 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:3;
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 ) ;
A3: pow ((1. L),|.i.|) = 1. L by Lm5;
pow ((1. L),i) = ((power L) . ((1. L),|.i.|)) " by A1, Def2
.= (1. L) " by A3, Def2 ;
hence pow ((1. L),i) = 1. L by A2, VECTSP_1:def 10; :: thesis: verum

end;

end;