:: deftheorem Def8 defines BinContinuous GROUP_1A:def 47 :
for G being TopSpace-like TopaddGrStr holds
( G is BinContinuous iff for f being Function of [:G,G:],G st f = the addF of G holds
f is continuous );