let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds
( f is total iff r (#) f is total )
let f be PartFunc of C,COMPLEX; :: thesis: for r being Element of COMPLEX holds
( f is total iff r (#) f is total )
let r be Element of COMPLEX ; :: thesis: ( f is total iff r (#) f is total )
thus ( f is total implies r (#) f is total ) :: thesis: ( r (#) f is total implies f is total )

proof

assume f is total ; :: thesis: r (#) f is total
then dom f = C by PARTFUN1:def 2;
hence dom (r (#) f) = C by Th7; :: according to PARTFUN1:def 2 :: thesis: verum

end;

assume r (#) f is total ; :: thesis: f is total
then dom (r (#) f) = C by PARTFUN1:def 2;
hence dom f = C by Th7; :: according to PARTFUN1:def 2 :: thesis: verum