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