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