let C be non empty set ; :: thesis: for c being Element of C
for f being PartFunc of C,REAL st f ^ is total holds
(f ^) . c = (f . c) "
let c be Element of C; :: thesis: for f being PartFunc of C,REAL st f ^ is total holds
(f ^) . c = (f . c) "
let f be PartFunc of C,REAL; :: thesis: ( f ^ is total implies (f ^) . c = (f . c) " )
assume f ^ is total ; :: thesis: (f ^) . c = (f . c) "
then dom (f ^) = C by PARTFUN1:def 2;
hence (f ^) . c = (f . c) " by Def8; :: thesis: verum