let L be non empty non degenerated right_complementable almost_left_invertible left-distributive well-unital add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for k being Element of NAT

for x being Element of L st x <> 0. L holds

(x ") |^ k = (x |^ k) "

let k be Element of NAT ; :: thesis: for x being Element of L st x <> 0. L holds

(x ") |^ k = (x |^ k) "

let x be Element of L; :: thesis: ( x <> 0. L implies (x ") |^ k = (x |^ k) " )

A1: 1. L <> 0. L ;

defpred S_{1}[ Nat] means (x ") |^ $1 = (x |^ $1) " ;

assume A2: x <> 0. L ; :: thesis: (x ") |^ k = (x |^ k) "

.= (1. L) * ((1. L) ") by A1, VECTSP_1:def 10

.= (1_ L) "

.= (x |^ 0) " by BINOM:8 ;

then A6: S_{1}[ 0 ]
;

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

hence (x ") |^ k = (x |^ k) " ; :: thesis: verum

for x being Element of L st x <> 0. L holds

(x ") |^ k = (x |^ k) "

let k be Element of NAT ; :: thesis: for x being Element of L st x <> 0. L holds

(x ") |^ k = (x |^ k) "

let x be Element of L; :: thesis: ( x <> 0. L implies (x ") |^ k = (x |^ k) " )

A1: 1. L <> 0. L ;

defpred S

assume A2: x <> 0. L ; :: thesis: (x ") |^ k = (x |^ k) "

A3: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

(x ") |^ 0 =
1_ L
by BINOM:8
S

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

A5: x |^ n <> 0. L by A2, Th1;

(x ") |^ (n + 1) = ((x ") |^ n) * (x ") by GROUP_1:def 7

.= (x * (x |^ n)) " by A2, A4, A5, Th2

.= ((x |^ 1) * (x |^ n)) " by BINOM:8

.= (x |^ (n + 1)) " by BINOM:10 ;

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

end;assume A4: S

A5: x |^ n <> 0. L by A2, Th1;

(x ") |^ (n + 1) = ((x ") |^ n) * (x ") by GROUP_1:def 7

.= (x * (x |^ n)) " by A2, A4, A5, Th2

.= ((x |^ 1) * (x |^ n)) " by BINOM:8

.= (x |^ (n + 1)) " by BINOM:10 ;

hence S

.= (1. L) * ((1. L) ") by A1, VECTSP_1:def 10

.= (1_ L) "

.= (x |^ 0) " by BINOM:8 ;

then A6: S

for n being Nat holds S

hence (x ") |^ k = (x |^ k) " ; :: thesis: verum