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;
pow (1_ L),0 = (power L) . (1. L),0 by Def3;
then A1: S₁[ 0 ] by GROUP_1:def 8;

A2: now

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence pow (1. L),i = 1. L ; :: thesis: verum