deffunc H1( Nat) -> set = (pfexp $1) | ((Seg p) /\ SetPrimes);
A0: for x being Element of FreeGen p holds H1(x) in BoolePrime p
proof
let x be Element of FreeGen p; :: thesis: H1(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 H1(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 = H1(x) from FUNCT_2:sch 8(A0);
 thus ex b1 being Function of (FreeGen p),(BoolePrime p) st
for x being Element of FreeGen p holds b1 . x = (pfexp x) | ((Seg p) /\ SetPrimes) by A1; :: thesis: verum