let n be non zero square-free Nat; :: thesis: rng (pfexp n) c= 2
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pfexp n) or y in 2 )
assume y in rng (pfexp n) ; :: thesis: y in 2
then consider x being object such that
A1: ( x in dom (pfexp n) & y = (pfexp n) . x ) by FUNCT_1:def 3;
reconsider x = x as Prime by A1, NAT_3:33;
A2: y = x |-count n by A1, NAT_3:def 8;
reconsider y1 = y as Nat by A1;
( y = 0 or y = 1 ) by NAT_1:25, MOEBIUS1:24, A2;
hence y in 2 by CARD_1:50, TARSKI:def 2; :: thesis: verum