let a be Nat; :: thesis: for s, z being non zero Nat holds a divides (a |^ s) + (a |^ z)
let s, z be non zero Nat; :: thesis: a divides (a |^ s) + (a |^ z)
( a |^ ((s - 1) + 1) = (a |^ (s - 1)) * a & a |^ ((z - 1) + 1) = (a |^ (z - 1)) * a ) by NEWTON:6;
then (a |^ s) + (a |^ z) = a * ((a |^ (s - 1)) + (a |^ (z - 1))) ;
hence a divides (a |^ s) + (a |^ z) ; :: thesis: verum