let n be non zero Nat; :: thesis: TSqFactors n = (SqFactors n) |^ 2
A0: dom ((SqFactors n) |^ 2) = SetPrimes by PARTFUN1:def 2;
AA: ( dom (TSqFactors n) = SetPrimes & dom (SqFactors n) = SetPrimes ) by PARTFUN1:def 2;
for x being object st x in dom (TSqFactors n) holds
(TSqFactors n) . x = ((SqFactors n) |^ 2) . x

proof

let x be object ; :: thesis: ( x in dom (TSqFactors n) implies (TSqFactors n) . x = ((SqFactors n) |^ 2) . x )
assume x in dom (TSqFactors n) ; :: thesis: (TSqFactors n) . x = ((SqFactors n) |^ 2) . x
then reconsider p = x as Prime by AA, NEWTON:def 6;

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

suppose J1: x in support (pfexp n) ; :: thesis: (TSqFactors n) . x = ((SqFactors n) |^ 2) . x

hence (TSqFactors n) . x = p |^ (2 * ((p |-count n) div 2)) by TSqDef
.= (p |^ ((p |-count n) div 2)) |^ 2 by NEWTON:9
.= ((SqFactors n) . x) |^ 2 by SqDef, J1
.= ((SqFactors n) |^ 2) . x by NAT_3:def 6 ;
:: thesis: verum

end;

suppose J0: not x in support (pfexp n) ; :: thesis: (TSqFactors n) . x = ((SqFactors n) |^ 2) . x

then not x in support (TSqFactors n) by TSqDef;
then J3: (TSqFactors n) . x = 0 by PRE_POLY:def 7;
not x in support (SqFactors n) by J0, SqDef;
then (SqFactors n) . x = 0 by PRE_POLY:def 7;
then ((SqFactors n) . x) |^ 2 = 0 by NEWTON:11;
hence (TSqFactors n) . x = ((SqFactors n) |^ 2) . x by J3, NAT_3:def 6; :: thesis: verum

end;

end;

end;

hence TSqFactors n = (SqFactors n) |^ 2 by FUNCT_1:2, A0, PARTFUN1:def 2; :: thesis: verum