let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for x being Element of L st x <> 0. L holds
for n being Element of NAT holds pow (x " ),n = (pow x,n) "
let x be Element of L; :: thesis: ( x <> 0. L implies for n being Element of NAT holds pow (x " ),n = (pow x,n) " )
assume A1: x <> 0. L ; :: thesis: for n being Element of NAT holds pow (x " ),n = (pow x,n) "
let n be Element of NAT ; :: thesis: pow (x " ),n = (pow x,n) "
A2: 1. L <> 0. L ;
defpred S₁[ Nat] means pow (x " ),$1 = (pow x,$1) " ;
pow (x " ),0 = 1. L by Th13
.= (1. L) * ((1. L) " ) by A2, VECTSP_1:def 22
.= (1. L) " by VECTSP_1:def 19
.= (pow x,0 ) " by Th13 ;
then A3: S₁[ 0 ] ;

now

let n be Element of NAT ; :: thesis: ( S₁[n] implies ( pow (x " ),(n + 1) = (pow x,(n + 1)) " & S₁[n + 1] ) )
assume A4: S₁[n] ; :: thesis: ( pow (x " ),(n + 1) = (pow x,(n + 1)) " & S₁[n + 1] )
A5: x |^ n <> 0. L by A1, Th1;
thus pow (x " ),(n + 1) = (x " ) |^ (n + 1) by Def3
.= ((x " ) |^ n) * (x " ) by GROUP_1:def 8
.= (pow (x " ),n) * (x " ) by Def3
.= (((power L) . x,n) " ) * (x " ) by A4, Def3
.= (x * (x |^ n)) " by A1, A5, Th2
.= ((x |^ 1) * (x |^ n)) " by BINOM:8
.= (x |^ (n + 1)) " by BINOM:11
.= (pow x,(n + 1)) " by Def3 ; :: thesis: S₁[n + 1]
hence S₁[n + 1] ; :: thesis: verum

end;

then A6: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A6);
hence pow (x " ),n = (pow x,n) " ; :: thesis: verum