theorem ThB: :: ABSRED_0:162

for S being non empty partial non-empty UAStr st S is Group-like holds
( arity (Den ((In (1,(dom the charact of S))),S)) = 0 & arity (Den ((In (2,(dom the charact of S))),S)) = 1 & arity (Den ((In (3,(dom the charact of S))),S)) = 2 )