reconsider f = chi (I,I) as PartFunc of I,REAL by Th11;
f is integrable by INTEGRA4:2;
hence ex b₁ being Function of I,REAL st b₁ is integrable ; :: thesis: verum