theorem :: PARTFUN2:42

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