let p be Prime; :: thesis: for a, b being non zero Nat holds p |^ (p |-count (a * b)) = (p |^ (p |-count a)) * (p |^ (p |-count b))
let a, b be non zero Nat; :: thesis: p |^ (p |-count (a * b)) = (p |^ (p |-count a)) * (p |^ (p |-count b))
set x = p |-count a;
set y = p |-count b;
thus p |^ (p |-count (a * b)) = p |^ ((p |-count a) + (p |-count b)) by Th28
.= (p |^ (p |-count a)) * (p |^ (p |-count b)) by NEWTON:8 ; :: thesis: verum