a2: support (TSqFactors n) c= support (pfexp n) by TSqDef;
rng (TSqFactors n) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (TSqFactors n) or y in NAT )
assume y in rng (TSqFactors n) ; :: thesis: y in NAT
then consider x being object such that
C1: ( x in dom (TSqFactors n) & y = (TSqFactors n) . x ) by FUNCT_1:def 3;
dom (TSqFactors n) = SetPrimes by PARTFUN1:def 2;
then reconsider p = x as Nat by C1;

per cases ( p in support (pfexp n) or not p in support (pfexp n) ) ;

suppose p in support (pfexp n) ; :: thesis: y in NAT

then (TSqFactors n) . p = p |^ (2 * ((p |-count n) div 2)) by TSqDef;
hence y in NAT by C1, ORDINAL1:def 12; :: thesis: verum

end;

suppose not p in support (pfexp n) ; :: thesis: y in NAT

then not p in support (TSqFactors n) by TSqDef;
then (TSqFactors n) . p = 0 by PRE_POLY:def 7;
hence y in NAT by C1; :: thesis: verum

end;

end;

end;

hence ( TSqFactors n is finite-support & TSqFactors n is natural-valued ) by PRE_POLY:def 8, a2, VALUED_0:def 6; :: thesis: verum