let n, m be Nat; :: thesis: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr

for a being Element of K holds a |^ (n + m) = (a |^ n) * (a |^ m)

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K holds a |^ (n + m) = (a |^ n) * (a |^ m)

let a be Element of K; :: thesis: a |^ (n + m) = (a |^ n) * (a |^ m)

defpred S_{1}[ Nat] means for n being Nat holds a |^ (n + $1) = (a |^ n) * (a |^ $1);

A1: S_{1}[ 0 ]
_{1}[m] holds

S_{1}[m + 1]
_{1}[m]
from NAT_1:sch 2(A1, A2);

hence a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: verum

for a being Element of K holds a |^ (n + m) = (a |^ n) * (a |^ m)

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K holds a |^ (n + m) = (a |^ n) * (a |^ m)

let a be Element of K; :: thesis: a |^ (n + m) = (a |^ n) * (a |^ m)

defpred S

A1: S

proof

A2:
for m being Nat st S
let n be Nat; :: thesis: a |^ (n + 0) = (a |^ n) * (a |^ 0)

thus a |^ (n + 0) = (a |^ n) * (1_ K)

.= (a |^ n) * (a |^ 0) by GROUP_1:def 7 ; :: thesis: verum

end;thus a |^ (n + 0) = (a |^ n) * (1_ K)

.= (a |^ n) * (a |^ 0) by GROUP_1:def 7 ; :: thesis: verum

S

proof

for m being Nat holds S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A3: for n being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: S_{1}[m + 1]

let n be Nat; :: thesis: a |^ (n + (m + 1)) = (a |^ n) * (a |^ (m + 1))

thus a |^ (n + (m + 1)) = a |^ ((n + m) + 1)

.= (a |^ (n + m)) * a by Lm2

.= ((a |^ n) * (a |^ m)) * a by A3

.= (a |^ n) * ((a |^ m) * a) by GROUP_1:def 3

.= (a |^ n) * (a |^ (m + 1)) by Lm2 ; :: thesis: verum

end;assume A3: for n being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: S

let n be Nat; :: thesis: a |^ (n + (m + 1)) = (a |^ n) * (a |^ (m + 1))

thus a |^ (n + (m + 1)) = a |^ ((n + m) + 1)

.= (a |^ (n + m)) * a by Lm2

.= ((a |^ n) * (a |^ m)) * a by A3

.= (a |^ n) * ((a |^ m) * a) by GROUP_1:def 3

.= (a |^ n) * (a |^ (m + 1)) by Lm2 ; :: thesis: verum

hence a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: verum