let a be prime Nat; :: thesis: for b being non zero Integer
for c being Nat holds a |-count (b |^ c) = c * (a |-count b)
let b be non zero Integer; :: thesis: for c being Nat holds a |-count (b |^ c) = c * (a |-count b)
let c be Nat; :: thesis: a |-count (b |^ c) = c * (a |-count b)
a |-count (b |^ c) = a |-count (|.b.| |^ c) by TAYLOR_2:1
.= c * (a |-count |.b.|) by NAT_3:32 ;
hence a |-count (b |^ c) = c * (a |-count b) ; :: thesis: verum