A1: support (SqFactors n) c= support (pfexp n) by SqDef;
rng (SqFactors n) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (SqFactors n) or y in NAT )
assume y in rng (SqFactors n) ; :: thesis: y in NAT
then consider x being object such that
C1: ( x in dom (SqFactors n) & y = (SqFactors n) . x ) by FUNCT_1:def 3;
dom (SqFactors 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 (SqFactors n) . p = p |^ ((p |-count n) div 2) by SqDef;
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 (SqFactors n) by SqDef;
then (SqFactors n) . p = 0 by PRE_POLY:def 7;
hence y in NAT by C1; :: thesis: verum

end;

end;

end;

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