theorem Th7: :: RFUNCT_3:7

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