theorem :: RFUNCT_1:59

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