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

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