let p be Prime; :: thesis: for n being non zero Nat holds (PFactors (p |^ n)) * <*p*> = <*p*>
let n be non zero Nat; :: thesis: (PFactors (p |^ n)) * <*p*> = <*p*>
set s = p |^ n;
set f = <*p*>;
set g = PFactors (p |^ n);
A1: dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
A2: dom ((PFactors (p |^ n)) * <*p*>) = {1}

proof

thus dom ((PFactors (p |^ n)) * <*p*>) c= {1} by A1, FUNCT_1:11; :: according to XBOOLE_0:def 10 :: thesis: {1} c= dom ((PFactors (p |^ n)) * <*p*>)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in dom ((PFactors (p |^ n)) * <*p*>) )
assume A3: x in {1} ; :: thesis: x in dom ((PFactors (p |^ n)) * <*p*>)
then x = 1 by TARSKI:def 1;
then <*p*> . x = p ;
then <*p*> . x in SetPrimes by NEWTON:def 6;
then A4: <*p*> . x in dom (PFactors (p |^ n)) by PARTFUN1:def 2;
x in dom <*p*> by A3, FINSEQ_1:2, FINSEQ_1:38;
hence x in dom ((PFactors (p |^ n)) * <*p*>) by A4, FUNCT_1:11; :: thesis: verum

end;

A5: for x being object st x in dom ((PFactors (p |^ n)) * <*p*>) holds
((PFactors (p |^ n)) * <*p*>) . x = <*p*> . x

proof

let x be object ; :: thesis: ( x in dom ((PFactors (p |^ n)) * <*p*>) implies ((PFactors (p |^ n)) * <*p*>) . x = <*p*> . x )
(pfexp p) . p <> 0 by NAT_3:38;
then p in support (pfexp p) by PRE_POLY:def 7;
then A6: p in support (pfexp (p |^ n)) by NAT_3:48;
assume A7: x in dom ((PFactors (p |^ n)) * <*p*>) ; :: thesis: ((PFactors (p |^ n)) * <*p*>) . x = <*p*> . x
then A8: x = 1 by A2, TARSKI:def 1;
then ((PFactors (p |^ n)) * <*p*>) . 1 = (PFactors (p |^ n)) . (<*p*> . 1) by A7, FUNCT_1:12
.= (PFactors (p |^ n)) . p
.= p by A6, Def6
.= <*p*> . 1 ;
hence ((PFactors (p |^ n)) * <*p*>) . x = <*p*> . x by A8; :: thesis: verum

end;

dom ((PFactors (p |^ n)) * <*p*>) = dom <*p*> by A2, FINSEQ_1:2, FINSEQ_1:38;
hence (PFactors (p |^ n)) * <*p*> = <*p*> by A5, FUNCT_1:2; :: thesis: verum