deffunc H₁( Element of X1) -> Element of ExtREAL = Integral (M2,(ProjPMap1 (f,$1)));
ex IT being Function of X1,ExtREAL st
for x being Element of X1 holds IT . x = H₁(x) from FUNCT_2:sch 4();
hence ex b₁ being Function of X1,ExtREAL st
for x being Element of X1 holds b₁ . x = Integral (M2,(ProjPMap1 (f,x))) ; :: thesis: verum