set f = I --> A;
dom (I --> A) = I by FUNCOP_1:19;
hence for b₁ being I -defined Function st b₁ = I --> A holds
b₁ is total by PARTFUN1:def 4; :: thesis: verum