let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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)) " )
A1: 1. L <> 0. L ;
defpred S₁[ Nat] means pow ((x "),$1) = (pow (x,$1)) " ;
assume A2: x <> 0. L ; :: thesis: for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) "

now :: thesis: for n being Nat st S₁[n] holds
( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S₁[n + 1] )

let n be Nat; :: thesis: ( S₁[n] implies ( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S₁[n + 1] ) )
assume A3: S₁[n] ; :: thesis: ( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S₁[n + 1] )
A4: x |^ n <> 0. L by A2, Th1;
thus pow ((x "),(n + 1)) = (x ") |^ (n + 1) by Def2
.= ((x ") |^ n) * (x ") by GROUP_1:def 7
.= (pow ((x "),n)) * (x ") by Def2
.= (((power L) . (x,n)) ") * (x ") by A3, Def2
.= (x * (x |^ n)) " by A2, A4, Th2
.= ((x |^ 1) * (x |^ n)) " by BINOM:8
.= (x |^ (n + 1)) " by BINOM:10
.= (pow (x,(n + 1))) " by Def2 ; :: thesis: S₁[n + 1]
hence S₁[n + 1] ; :: thesis: verum

end;

then A5: for n being Nat st S₁[n] holds
S₁[n + 1] ;
let n be Nat; :: thesis: ( n is Element of NAT implies pow ((x "),n) = (pow (x,n)) " )
pow ((x "),0) = 1. L by Th13
.= (1. L) * ((1. L) ") by A1, VECTSP_1:def 10
.= (1. L) "
.= (pow (x,0)) " by Th13 ;
then A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A5);
hence ( n is Element of NAT implies pow ((x "),n) = (pow (x,n)) " ) ; :: thesis: verum