theorem :: PARTFUN2:38

for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f | X is constant & Y c= X holds
f | Y is constant