let C be non empty set ; :: thesis: for c being Element of C
for f being PartFunc of C,COMPLEX st f ^ is total holds
(f ^ ) /. c = (f /. c) "
let c be Element of C; :: thesis: for f being PartFunc of C,COMPLEX st f ^ is total holds
(f ^ ) /. c = (f /. c) "
let f be PartFunc of C,COMPLEX ; :: 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 4;
hence (f ^ ) /. c = (f /. c) " by Def2; :: thesis: verum