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 S1[ Nat] means <%x%> `^ $1 = <%(power (x,$1))%>;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume <%x%> `^ n = <%(power (x,n))%> ; :: thesis: S1[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: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A2, A1); :: thesis: verum