let X be non empty set ; :: thesis: for f being Function of X,COMPLEX st f | X is bounded holds
modetrans (f,X) = f
let f be Function of X,COMPLEX; :: thesis: ( f | X is bounded implies modetrans (f,X) = f )
assume f | X is bounded ; :: thesis: modetrans (f,X) = f
then f in ComplexBoundedFunctions X ;
hence modetrans (f,X) = f by Def7; :: thesis: verum