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 S1[ Nat] means for n being Nat holds a |^ (n + \$1) = (a |^ n) * (a |^ \$1);
A1: S1[ 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 S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A3: for n being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: S1[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 S1[m] from NAT_1:sch 2(A1, A2);
hence a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: verum