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₁[ Nat] means (x ") |^ $1 = (x |^ $1) " ;
assume A2: x <> 0. L ; :: thesis: (x ") |^ k = (x |^ k) "

A3: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[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₁[n + 1] ; :: thesis: verum

end;

(x ") |^ 0 = 1_ L by BINOM:8
.= (1. L) * ((1. L) ") by A1, VECTSP_1:def 10
.= (1_ L) "
.= (x |^ 0) " by BINOM:8 ;
then A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A3);
hence (x ") |^ k = (x |^ k) " ; :: thesis: verum