:: deftheorem defines Den PUA2MSS1:def 1 :
for A being non-empty UAStr
for o being OperSymbol of A holds Den (o,A) = the charact of A . o;