let X be non empty set ; :: thesis: for Y being ComplexNormSpace
for f being bounded Function of X,the carrier of Y holds modetrans f,X,Y = f
let Y be ComplexNormSpace; :: thesis: 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; :: thesis: modetrans f,X,Y = f
f in ComplexBoundedFunctions X,Y by Def5;
hence modetrans f,X,Y = f by Def7; :: thesis: verum