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_{1}[ 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)) "

_{1}[n] holds

S_{1}[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_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A6, A5);

hence ( n is Element of NAT implies pow ((x "),n) = (pow (x,n)) " ) ; :: thesis: verum

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

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_{1}[n] holds

( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S_{1}[n + 1] )

then A5:
for n being Nat st S( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S

let n be Nat; :: thesis: ( S_{1}[n] implies ( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S_{1}[n + 1] ) )

assume A3: S_{1}[n]
; :: thesis: ( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S_{1}[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_{1}[n + 1]

hence S_{1}[n + 1]
; :: thesis: verum

end;assume A3: S

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

hence S

S

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

for n being Nat holds S

hence ( n is Element of NAT implies pow ((x "),n) = (pow (x,n)) " ) ; :: thesis: verum