:: deftheorem defines <*> BSPACE:def 1 :
for S being 1-sorted holds <*> S = <*> ([#] S);