:: deftheorem defines * BCIALG_4:def 1 :
for A being BCIStr_1
for x, y being Element of A holds x * y = the ExternalDiff of A . (x,y);