let L be non empty almost_left_invertible associative commutative well-unital distributive 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₁[ Element of NAT ] means pow ((1. L),$1) = 1. L;

A1: now

let k be Element of 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 Def3
.= ((power L) . ((1. L),k)) * (1. L) by GROUP_1:def 7
.= (1. L) * (1. L) by A2, Def3
.= 1. L by VECTSP_1:def 8 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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