theorem Th40: :: PARTFUN1:40

for X, Y being set
for f being Function st <:f,X,Y:> is total holds
X c= dom f by Th23;