let m, n be non zero Nat; :: thesis: ( pfexp m = pfexp n implies m = n )
K1: dom (pfexp m) = SetPrimes by PARTFUN1:def 2
.= dom (ppf m) by PARTFUN1:def 2 ;
K2: dom (pfexp n) = SetPrimes by PARTFUN1:def 2
.= dom (ppf n) by PARTFUN1:def 2 ;
assume SS: pfexp m = pfexp n ; :: thesis: m = n
for x being object st x in dom (ppf m) holds
(ppf m) . x = (ppf n) . x

proof

let x be object ; :: thesis: ( x in dom (ppf m) implies (ppf m) . x = (ppf n) . x )
assume x in dom (ppf m) ; :: thesis: (ppf m) . x = (ppf n) . x
then reconsider y = x as Prime by K1, NAT_3:33;

per cases ( ( y in support (pfexp m) & y in support (pfexp n) ) or ( not y in support (pfexp m) & y in support (pfexp n) ) or ( y in support (pfexp m) & not y in support (pfexp n) ) or ( not y in support (pfexp m) & not y in support (pfexp n) ) ) ;

suppose B1: ( y in support (pfexp m) & y in support (pfexp n) ) ; :: thesis: (ppf m) . x = (ppf n) . x

then B2: (ppf m) . y = y |^ (y |-count m) by NAT_3:def 9;
y |-count m = (pfexp m) . y by NAT_3:def 8
.= y |-count n by NAT_3:def 8, SS ;
hence (ppf m) . x = (ppf n) . x by B2, B1, NAT_3:def 9; :: thesis: verum

end;

suppose ( not y in support (pfexp m) & y in support (pfexp n) ) ; :: thesis: (ppf m) . x = (ppf n) . x

hence (ppf m) . x = (ppf n) . x by SS; :: thesis: verum

end;

suppose ( y in support (pfexp m) & not y in support (pfexp n) ) ; :: thesis: (ppf m) . x = (ppf n) . x

hence (ppf m) . x = (ppf n) . x by SS; :: thesis: verum

end;

suppose ( not y in support (pfexp m) & not y in support (pfexp n) ) ; :: thesis: (ppf m) . x = (ppf n) . x

then KS: ( not y in support (ppf m) & not y in support (ppf n) ) by NAT_3:def 9;
hence (ppf m) . x = 0 by PRE_POLY:def 7
.= (ppf n) . x by KS, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

then ppf m = ppf n by SS, K1, K2, FUNCT_1:2;
then m = Product (ppf n) by NAT_3:61;
hence m = n by NAT_3:61; :: thesis: verum