let p be Prime; :: thesis: (Bnumber_of_divisors p) * <*p*> = <*2*>
set f = <*p*>;
set g = Bnumber_of_divisors p;
set z = <*2*>;
A1: dom ((Bnumber_of_divisors p) * <*p*>) = {1}

proof

thus dom ((Bnumber_of_divisors p) * <*p*>) c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= dom ((Bnumber_of_divisors p) * <*p*>)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((Bnumber_of_divisors p) * <*p*>) or x in {1} )
assume x in dom ((Bnumber_of_divisors 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 ((Bnumber_of_divisors p) * <*p*>) )
assume A2: x in {1} ; :: thesis: x in dom ((Bnumber_of_divisors p) * <*p*>)
then x = 1 by TARSKI:def 1;
then <*p*> . x in SetPrimes by NEWTON:def 6;
then A3: <*p*> . x in dom (Bnumber_of_divisors p) by PARTFUN1:def 2;
x in dom <*p*> by A2, FINSEQ_1:2, FINSEQ_1:38;
hence x in dom ((Bnumber_of_divisors p) * <*p*>) by A3, FUNCT_1:11; :: thesis: verum

end;

A4: for x being object st x in dom ((Bnumber_of_divisors p) * <*p*>) holds
((Bnumber_of_divisors p) * <*p*>) . x = <*2*> . x

proof

let x be object ; :: thesis: ( x in dom ((Bnumber_of_divisors p) * <*p*>) implies ((Bnumber_of_divisors p) * <*p*>) . x = <*2*> . x )
(pfexp p) . p <> 0 by NAT_3:38;
then A5: p in support (pfexp p) by PRE_POLY:def 7;
SX: p > 1 by INT_2:def 4;
assume A6: x in dom ((Bnumber_of_divisors p) * <*p*>) ; :: thesis: ((Bnumber_of_divisors p) * <*p*>) . x = <*2*> . x
then A7: x = 1 by A1, TARSKI:def 1;
then ((Bnumber_of_divisors p) * <*p*>) . 1 = (Bnumber_of_divisors p) . (<*p*> . 1) by A6, FUNCT_1:12
.= (p |-count p) + 1 by A5, BDef
.= 1 + 1 by SX, NAT_3:22
.= <*2*> . 1 ;
hence ((Bnumber_of_divisors p) * <*p*>) . x = <*2*> . x by A7; :: thesis: verum

end;

dom <*2*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
hence (Bnumber_of_divisors p) * <*p*> = <*2*> by A1, A4, FUNCT_1:2; :: thesis: verum