set X = FreeGen p;
defpred S₁[ non zero Nat, object ] means c₂ = (pfexp p) | ((Seg p) /\ SetPrimes);
set f = canHom p;
for x1, x2 being object st x1 in FreeGen p & x2 in FreeGen p & (canHom p) . x1 = (canHom p) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in FreeGen p & x2 in FreeGen p & (canHom p) . x1 = (canHom p) . x2 implies x1 = x2 )
assume I0: ( x1 in FreeGen p & x2 in FreeGen p & (canHom p) . x1 = (canHom p) . x2 ) ; :: thesis: x1 = x2
then reconsider m1 = x1, m2 = x2 as non zero Nat by MOEBIUS1:21;
II: ( S₁[m1,(canHom p) . x1] & S₁[m2,(canHom p) . x2] ) by I0, canH;
u1: ( dom (pfexp m1) = SetPrimes & dom (pfexp m2) = SetPrimes ) by PARTFUN1:def 2;
ki: ( support (pfexp m1) c= Seg p & support (pfexp m2) c= Seg p ) by Lm1, I0;
kk: support (pfexp m1) = support (pfexp m2)

proof

assume not support (pfexp m1) = support (pfexp m2) ; :: thesis: contradiction
then consider z being object such that
JJ: ( ( z in support (pfexp m1) & not z in support (pfexp m2) ) or ( z in support (pfexp m2) & not z in support (pfexp m1) ) ) by TARSKI:2;

per cases ( ( z in support (pfexp m1) & not z in support (pfexp m2) ) or ( z in support (pfexp m2) & not z in support (pfexp m1) ) ) by JJ;

suppose he: ( z in support (pfexp m1) & not z in support (pfexp m2) ) ; :: thesis: contradiction

then hh: ( (pfexp m1) . z <> 0 & (pfexp m2) . z = 0 ) by PRE_POLY:def 7;
xk: z in SetPrimes /\ (Seg p) by XBOOLE_0:def 4, he, ki;
then ((pfexp m1) | (SetPrimes /\ (Seg p))) . z = (pfexp m1) . z by FUNCT_1:49;
hence contradiction by xk, FUNCT_1:49, I0, II, hh; :: thesis: verum

end;

suppose he: ( z in support (pfexp m2) & not z in support (pfexp m1) ) ; :: thesis: contradiction

then hh: ( (pfexp m2) . z <> 0 & (pfexp m1) . z = 0 ) by PRE_POLY:def 7;
xk: z in SetPrimes /\ (Seg p) by XBOOLE_0:def 4, he, ki;
then ((pfexp m2) | (SetPrimes /\ (Seg p))) . z <> 0 by hh, FUNCT_1:49;
hence contradiction by hh, xk, FUNCT_1:49, I0, II; :: thesis: verum

end;

end;

end;

for x being object st x in dom (pfexp m1) holds
(pfexp m1) . x = (pfexp m2) . x

proof

let x be object ; :: thesis: ( x in dom (pfexp m1) implies (pfexp m1) . x = (pfexp m2) . x )
assume x in dom (pfexp m1) ; :: thesis: (pfexp m1) . x = (pfexp m2) . x

per cases ( x in SetPrimes /\ (Seg p) or not x in SetPrimes /\ (Seg p) ) ;

suppose GG: x in SetPrimes /\ (Seg p) ; :: thesis: (pfexp m1) . x = (pfexp m2) . x

hence (pfexp m1) . x = ((pfexp m1) | (SetPrimes /\ (Seg p))) . x by FUNCT_1:49
.= (pfexp m2) . x by FUNCT_1:49, GG, I0, II ;
:: thesis: verum

end;

suppose not x in SetPrimes /\ (Seg p) ; :: thesis: (pfexp m1) . x = (pfexp m2) . x

then zo: not x in support (pfexp m1) by ki, XBOOLE_0:def 4;
then (pfexp m1) . x = 0 by PRE_POLY:def 7;
hence (pfexp m1) . x = (pfexp m2) . x by PRE_POLY:def 7, kk, zo; :: thesis: verum

end;

end;

end;

hence x1 = x2 by WOW, FUNCT_1:2, u1; :: thesis: verum

end;

hence canHom p is one-to-one by FUNCT_2:19; :: thesis: verum