deffunc H₁( set ) -> set = proj1 (f . $1);
ex F being Function st
( dom F = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
F . x = H₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b₁ . x = proj1 (f . x) ) ) ; :: thesis: verum