let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; :: thesis: for i being Element of NAT holds pow ((1. L),i) = 1. L
let i be Element of NAT ; :: thesis: pow ((1. L),i) = 1. L
defpred S₁[ Nat] means pow ((1. L),$1) = 1. L;

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
pow ((1. L),(k + 1)) = (power L) . ((1. L),(k + 1)) by Def2
.= ((power L) . ((1. L),k)) * (1. L) by GROUP_1:def 7
.= (1. L) * (1. L) by A2, Def2
.= 1. L ;
hence S₁[k + 1] ; :: thesis: verum

end;

pow ((1_ L),0) = (power L) . ((1. L),0) by Def2;
then A3: S₁[ 0 ] by GROUP_1:def 7;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1);
hence pow ((1. L),i) = 1. L ; :: thesis: verum