dom (f .. x) = (dom f) /\ (dom x) by Def17
.= I /\ (dom x) by PARTFUN1:def 2
.= I /\ I by PARTFUN1:def 2 ;
hence for b₁ being I -defined Function st b₁ = f .. x holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum