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