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 * ((a |^ (s - 1)) * (a |^ (z - 1)))) ;
hence a divides (a |^ s) * (a |^ z) ; :: thesis: verum