let X be non empty set ; for Y being RealNormSpace
for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
let Y be RealNormSpace; for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
let f be bounded Function of X, the carrier of Y; modetrans (f,X,Y) = f
f in BoundedFunctions (X,Y)
by Def5;
hence
modetrans (f,X,Y) = f
by Def7; verum