let n be non zero Nat; :: thesis: PrimeDivisorsFS n = sort_a (canFS (support (pfexp n)))
set X = PrimeDivisors n;
set P = PrimeDivisorsFS n;
set f = canFS (support (pfexp n));
set S = sort_a (canFS (support (pfexp n)));
A1: PrimeDivisorsFS n is FinSequence of REAL by FINSEQ_1:106;
canFS (support (pfexp n)) is FinSequence of REAL by FINSEQ_1:106;
then A2: sort_a (canFS (support (pfexp n))) is one-to-one by EUCLID_7:13;
A3: rng (PrimeDivisorsFS n) = PrimeDivisors n by FINSEQ_1:def 14;
rng (canFS (support (pfexp n))) = support (pfexp n) by FUNCT_2:def 3;
then rng (sort_a (canFS (support (pfexp n)))) = support (pfexp n) by CLASSES1:75, RFINSEQ2:def 6;
hence PrimeDivisorsFS n = sort_a (canFS (support (pfexp n))) by A1, A2, A3, Th48, INTEGRA3:6; :: thesis: verum