:: deftheorem Def8 defines BinContinuous TOPGRP_1:def 8 :
for G being TopSpace-like TopGrStr holds
( G is BinContinuous iff for f being Function of [:G,G:],G st f = the multF of G holds
f is continuous );