:: deftheorem defines total PARTFUN1:def 2 :
for X being set
for f being b₁ -defined Relation holds
( f is total iff dom f = X );