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