let n be non zero Nat; :: thesis: PrimeDivisorsFS n = sort_a (canFS (support (ppf n)))
PrimeDivisorsFS n = sort_a (canFS (support (pfexp n))) by Th51;
hence PrimeDivisorsFS n = sort_a (canFS (support (ppf n))) by NAT_3:def 9; :: thesis: verum