ex f being Function st
( dom f = (dom f1) /\ (dom f2) & ( for x being object st x in (dom f1) /\ (dom f2) holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = (dom f1) /\ (dom f2) & ( for x being object st x in dom b₁ holds
b₁ . x = (f1 . x) + (f2 . x) ) ) ; :: thesis: verum