let p be prime Nat; :: thesis: for a, b being non zero Integer holds p |-count (a * b) = (p |-count a) + (p |-count b)
let a, b be non zero Integer; :: thesis: p |-count (a * b) = (p |-count a) + (p |-count b)
reconsider k = |.a.|, l = |.b.| as non zero Nat ;
p |-count (a * b) = |.p.| |-count (|.a.| * |.b.|) by COMPLEX1:65
.= (|.p.| |-count k) + (|.p.| |-count l) by NAT_3:28 ;
hence p |-count (a * b) = (p |-count a) + (p |-count b) ; :: thesis: verum