let n be non zero Nat; :: thesis: ( support (ppf n) = {} implies n = 1 )
assume support (ppf n) = {} ; :: thesis: n = 1
then support (pfexp n) = {} by Def9;
hence n = 1 by Th52; :: thesis: verum