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)) " )
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

let n be Element of 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 Def3
.= ((x ") |^ n) * (x ") by GROUP_1:def 8
.= (pow ((x "),n)) * (x ") by Def3
.= (((power L) . (x,n)) ") * (x ") by A3, Def3
.= (x * (x |^ n)) " by A2, A4, 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 A5: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;
let n be Element of NAT ; :: thesis: pow ((x "),n) = (pow (x,n)) "
pow ((x "),0) = 1. L by Th13
.= (1. L) * ((1. L) ") by A1, VECTSP_1:def 22
.= (1. L) " by VECTSP_1:def 19
.= (pow (x,0)) " by Th13 ;
then A6: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A5);
hence pow ((x "),n) = (pow (x,n)) " ; :: thesis: verum