deffunc H₁( Element of Sub U0) -> Subset of U0 = carr $1;
ex f being Function of Sub U0, bool the carrier of U0 st
for x being Element of Sub U0 holds f . x = H₁(x) from FUNCT_2:sch 4();
hence ex b₁ being Function of Sub U0, bool the carrier of U0 st
for u being Element of Sub U0 holds b₁ . u = carr u ; :: thesis: verum