dom (J --> y) = J by FUNCOP_1:19;
hence for b₁ being J -defined Function st b₁ = J => y holds
b₁ is total ; :: thesis: verum