theorem :: PARTFUN2:43

for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f | Y is V8() holds
(f | X) | Y is V8()