let p be Prime; :: thesis: for f being FinSequence of NAT st f = {} holds
p |-count f = {}
let f be FinSequence of NAT ; :: thesis: ( f = {} implies p |-count f = {} )
assume f = {} ; :: thesis: p |-count f = {}
then len (p |-count f) = len {} by Def1;
hence p |-count f = {} ; :: thesis: verum