:: deftheorem defines modetrans C0SP3:def 5 :
for S, T being RealNormSpace
for f being object st f in ContinuousFunctions (S,T) holds
for b₄ being Function of S,T holds
( b₄ = modetrans (f,S,T) iff ( b₄ = f & b₄ is_continuous_on the carrier of S ) );