let R be non empty unital associative multMagma ; :: thesis: for a being Element of R
for n, m being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m)
let a be Element of R; :: thesis: for n, m being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m)
let n, m be Nat; :: thesis: a |^ (n + m) = (a |^ n) * (a |^ m)
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
a |^ (n1 + m1) = (a |^ n1) * (a |^ m1) by Lm3;
hence a |^ (n + m) = (a |^ n) * (a |^ m) ; :: thesis: verum