theorem Th5: :: PDIFF_9:5

for i being Element of NAT
for Z being set
for f being PartFunc of (REAL i),REAL holds <>* (f | Z) = (<>* f) | Z