let L be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for x being Element of L
for n being Nat holds <%x%> `^ n = <%(power (x,n))%>
let x be Element of L; :: thesis: for n being Nat holds <%x%> `^ n = <%(power (x,n))%>
defpred S₁[ Nat] means <%x%> `^ $1 = <%(power (x,$1))%>;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume <%x%> `^ n = <%(power (x,n))%> ; :: thesis: S<sub>1</sub>[n + 1]
hence <%x%> `^ (n + 1) = <%((power L) . (x,n))%> *' <%x%> by Th19
.= <%(((power L) . (x,n)) * x)%> by Th35
.= <%(power (x,(n + 1)))%> by GROUP_1:def 7 ;
:: thesis: verum

end;

<%x%> `^ 0 = 1_. L by Th15
.= (1. L) * (1_. L) by Th27
.= <%(1_ L)%> by Th29
.= <%((power L) . (x,0))%> by GROUP_1:def 7 ;
then A2: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1); :: thesis: verum