let L be non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed 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) " )
assume A1: x <> 0. L ; :: thesis: (x " ) |^ k = (x |^ k) "
A2: 1. L <> 0. L ;
defpred S₁[ Element of NAT ] means (x " ) |^ $1 = (x |^ $1) " ;
(x " ) |^ 0 = 1_ L by BINOM:8
.= (1. L) * ((1. L) " ) by A2, VECTSP_1:def 22
.= (1_ L) " by VECTSP_1:def 19
.= (x |^ 0 ) " by BINOM:8 ;
then A3: S₁[ 0 ] ;

A4: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: x |^ n <> 0. L by A1, Th1;
(x " ) |^ (n + 1) = ((x " ) |^ n) * (x " ) by GROUP_1:def 8
.= (x * (x |^ n)) " by A1, A5, A6, Th2
.= ((x |^ 1) * (x |^ n)) " by BINOM:8
.= (x |^ (n + 1)) " by BINOM:11 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
hence (x " ) |^ k = (x |^ k) " ; :: thesis: verum