let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,the carrier of V holds
( f is total iff ||.f.|| is total )
let V be RealNormSpace; :: thesis: for f being PartFunc of C,the carrier of V holds
( f is total iff ||.f.|| is total )
let f be PartFunc of C,the carrier of V; :: 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 Def5; :: 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 Def5; :: according to PARTFUN1:def 4 :: thesis: verum