:: deftheorem defines Product_S BCIALG_4:def 8 :
for X being non empty BCIStr_1
for F being FinSequence of the carrier of X holds Product_S F = the ExternalDiff of X "**" F;