theorem :: CFUNCT_1:26

for f being complex-valued Function holds 1 (#) f = f by T1;