let n be non zero Nat; :: thesis: ( ( rng (pfexp n) c= {0,1} & card (support (pfexp n)) = 1 ) iff n is prime )

hereby :: thesis: ( n is prime implies ( rng (pfexp n) c= {0,1} & card (support (pfexp n)) = 1 ) )

assume A1: ( rng (pfexp n) c= {0,1} & card (support (pfexp n)) = 1 ) ; :: thesis: n is prime
then consider p being object such that
A2: support (pfexp n) = {p} by CARD_2:42;
p in {p} by TARSKI:def 1;
then reconsider p = p as Prime by A2, NAT_3:34;
A3: ( p in support (pfexp n) & support (pfexp n) c= dom (pfexp n) ) by A2, TARSKI:def 1, PRE_POLY:37;
then A4: (pfexp n) . p in rng (pfexp n) by FUNCT_1:def 3;
(pfexp n) . p <> 0 by A3, PRE_POLY:def 7;
then A5: (pfexp n) . p = 1 by A1, A4, TARSKI:def 2;
n = p |^ 1 by A5, A2, Th21;
hence n is prime ; :: thesis: verum

end;

assume A6: n is prime ; :: thesis: ( rng (pfexp n) c= {0,1} & card (support (pfexp n)) = 1 )
n = n |^ 1 ;
then A7: support (pfexp n) = {n} by A6, NAT_3:42;
thus rng (pfexp n) c= {0,1} :: thesis: card (support (pfexp n)) = 1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pfexp n) or y in {0,1} )
assume A8: ( y in rng (pfexp n) & not y in {0,1} ) ; :: thesis: contradiction
consider x being object such that
A9: ( x in dom (pfexp n) & (pfexp n) . x = y ) by A8, FUNCT_1:def 3;
( y <> 0 & y <> 1 ) by A8, TARSKI:def 2;
then x in support (pfexp n) by A9, PRE_POLY:def 7;
then x = n by A7, TARSKI:def 1;
then (pfexp n) . x = 1 by A6, NAT_3:41;
hence contradiction by A8, A9, TARSKI:def 2; :: thesis: verum

end;

thus card (support (pfexp n)) = 1 by A7, CARD_1:30; :: thesis: verum