dom X = [:I,J:] by PARTFUN1:def 2;
hence for b₁ being [:J,I:] -defined Function st b₁ = ~ X holds
b₁ is total by PARTFUN1:def 2, FUNCT_4:46; :: thesis: verum