let p be Prime; :: thesis: (PFactors p) * <*p*> = <*p*>
set f = <*p*>;
set g = PFactors p;
A1: dom ((PFactors p) * <*p*>) = {1}
proof
thus dom ((PFactors p) * <*p*>) c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= dom ((PFactors p) * <*p*>)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((PFactors p) * <*p*>) or x in {1} )
assume x in dom ((PFactors p) * <*p*>) ; :: thesis: x in {1}
then x in dom <*p*> by FUNCT_1:11;
hence x in {1} by FINSEQ_1:2, FINSEQ_1:38; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in dom ((PFactors p) * <*p*>) )
assume A2: x in {1} ; :: thesis: x in dom ((PFactors p) * <*p*>)
then x = 1 by TARSKI:def 1;
then <*p*> . x = p by FINSEQ_1:def 8;
then <*p*> . x in SetPrimes by NEWTON:def 6;
then A3: <*p*> . x in dom (PFactors p) by PARTFUN1:def 2;
x in dom <*p*> by A2, FINSEQ_1:2, FINSEQ_1:38;
hence x in dom ((PFactors p) * <*p*>) by A3, FUNCT_1:11; :: thesis: verum
end;
A4: for x being object st x in dom ((PFactors p) * <*p*>) holds
((PFactors p) * <*p*>) . x = <*p*> . x
proof
let x be object ; :: thesis: ( x in dom ((PFactors p) * <*p*>) implies ((PFactors p) * <*p*>) . x = <*p*> . x )
(pfexp p) . p <> 0 by NAT_3:38;
then A5: p in support (pfexp p) by PRE_POLY:def 7;
assume A6: x in dom ((PFactors p) * <*p*>) ; :: thesis: ((PFactors p) * <*p*>) . x = <*p*> . x
then A7: x = 1 by A1, TARSKI:def 1;
then ((PFactors p) * <*p*>) . 1 = (PFactors p) . (<*p*> . 1) by A6, FUNCT_1:12
.= (PFactors p) . p by FINSEQ_1:def 8
.= p by A5, Def6
.= <*p*> . 1 by FINSEQ_1:def 8 ;
hence ((PFactors p) * <*p*>) . x = <*p*> . x by A7; :: thesis: verum
end;
dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
hence (PFactors p) * <*p*> = <*p*> by A1, A4, FUNCT_1:2; :: thesis: verum