deffunc H₁( Nat) -> set = (pfexp $1) | ((Seg p) /\ SetPrimes);
A0: for x being Element of FreeGen p holds H₁(x) in BoolePrime p

proof

let x be Element of FreeGen p; :: thesis: H₁(x) in BoolePrime p
dom (pfexp x) = SetPrimes by PARTFUN1:def 2;
then J1: dom ((pfexp x) | ((Seg p) /\ SetPrimes)) = SetPrimes /\ ((Seg p) /\ SetPrimes) by RELAT_1:61
.= (Seg p) /\ SetPrimes by XBOOLE_1:17, XBOOLE_1:28 ;
set SP = (Seg p) /\ SetPrimes;
rng ((pfexp x) | ((Seg p) /\ SetPrimes)) c= 2

proof

( x is square-free & ( for i being Prime st i divides x holds
i <= p ) ) by FG;
then l1: rng (pfexp x) c= 2 by LmRng, MOEBIUS1:21;
rng ((pfexp x) | ((Seg p) /\ SetPrimes)) c= rng (pfexp x) by RELAT_1:70;
hence rng ((pfexp x) | ((Seg p) /\ SetPrimes)) c= 2 by l1; :: thesis: verum

end;

then (pfexp x) | ((Seg p) /\ SetPrimes) is Function of ((Seg p) /\ SetPrimes),2 by J1, FUNCT_2:2;
hence H₁(x) in BoolePrime p by FUNCT_2:8; :: thesis: verum

end;

consider f being Function of (FreeGen p),(BoolePrime p) such that
A1: for x being Element of FreeGen p holds f . x = H₁(x) from FUNCT_2:sch 8(A0);
thus ex b₁ being Function of (FreeGen p),(BoolePrime p) st
for x being Element of FreeGen p holds b₁ . x = (pfexp x) | ((Seg p) /\ SetPrimes) by A1; :: thesis: verum