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

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