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

proof

assume f is total ; :: thesis: |.f.| is total
then dom f = C by PARTFUN1:def 4;
hence dom |.f.| = C by VALUED_1:def 11; :: according to PARTFUN1:def 4 :: thesis: verum

end;

assume |.f.| is total ; :: thesis: f is total
then dom |.f.| = C by PARTFUN1:def 4;
hence dom f = C by VALUED_1:def 11; :: according to PARTFUN1:def 4 :: thesis: verum