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₁[ Nat] means for n being Nat holds a |^ (n + $1) = (a |^ n) * (a |^ $1);
A1: S₁[ 0 ]

proof

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;

A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: for n being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: S₁[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;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
hence a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: verum