:: deftheorem Def9 defines Mult-continuous RLTOPSP1:def 9 :
for X being non empty RLTopStruct holds
( X is Mult-continuous iff for a being Real
for x being Point of X
for V being Subset of X st V is open & a * x in V holds
ex r being positive Real ex W being Subset of X st
( W is open & x in W & ( for s being Real st |.(s - a).| < r holds
s * W c= V ) ) );