theorem Th18: :: VFUNCT_1:18

for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds 1 (#) f = f