for X being set
for C, D being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d )