theorem :: CFUNCT_1:26

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