theorem :: FUNCT_2:39

for Q, X, Y being set
for f being PartFunc of X,Y holds f " Q c= X ;