theorem Th9: :: RFUNCT_3:9

for D being non empty set
for F being PartFunc of D,REAL holds (abs F) " {0} = F " {0}