theorem Th18: :: VFUNCT_2:18

for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds 1r (#) f = f