let p be Prime; :: thesis: for n being non zero Nat st p |-count n = 0 holds
(TSqFactors n) . p = 0
let n be non zero Nat; :: thesis: ( p |-count n = 0 implies (TSqFactors n) . p = 0 )
assume p |-count n = 0 ; :: thesis: (TSqFactors n) . p = 0
then (pfexp n) . p = 0 by NAT_3:def 8;
then not p in support (pfexp n) by PRE_POLY:def 7;
then not p in support (TSqFactors n) by TSqDef;
hence (TSqFactors n) . p = 0 by PRE_POLY:def 7; :: thesis: verum