let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for f being continuous PartFunc of REAL,Y st dom f = X holds
modetrans (f,X,Y) = f
let Y be RealNormSpace; :: thesis: for f being continuous PartFunc of REAL,Y st dom f = X holds
modetrans (f,X,Y) = f
let f be continuous PartFunc of REAL,Y; :: thesis: ( dom f = X implies modetrans (f,X,Y) = f )
assume dom f = X ; :: thesis: modetrans (f,X,Y) = f
then f in ContinuousFunctions (X,Y) by Def2;
hence modetrans (f,X,Y) = f by Def5; :: thesis: verum