[#] X0 c= [#] X by PRE_TOPC:def 4;
hence for b₁ being Function of X0,Y holds
( b₁ = f | X0 iff b₁ = f | the carrier of X0 ) by Def3; :: thesis: verum