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