let x be object ; :: according to VALUED_0:def 12 :: thesis: ( not x in dom (pfexp n) or not (pfexp n) . x is V35() )
set f = pfexp n;
assume x in dom (pfexp n) ; :: thesis: (pfexp n) . x is V35()
then reconsider x = x as Prime by Th33;
(pfexp n) . x = x |-count n by Def8;
hence (pfexp n) . x is V35() ; :: thesis: verum