:: deftheorem Def6 defines multiplicative BCIALG_6:def 6 :
for X, X9 being non empty BCIStr_0
for f being Function of X,X9 holds
( f is multiplicative iff for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b) );