:: deftheorem Def7 defines modetrans CC0SP1:def 7 :
for X being non empty set
for F being object st F in ComplexBoundedFunctions X holds
for b₃ being Function of X,COMPLEX holds
( b₃ = modetrans (F,X) iff ( b₃ = F & b₃ | X is bounded ) );