theorem Th21: :: COMPUT_1:22

for X being set
for f being homogeneous PartFunc of (X *),X holds
( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on X )