theorem :: CFUNCT_1:67

for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX st f ^ is total holds
(f ^) /. c = (f /. c) " by Def2;