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;
end;
end;
hence TSqFactors n = (SqFactors n) |^ 2 by FUNCT_1:2, A0, PARTFUN1:def 2; :: thesis: verum