for A being free Universal_Algebra
for o1, o2 being OperSymbol of A
for p1, p2 being FinSequence st p1 in dom (Den (o1,A)) & p2 in dom (Den (o2,A)) & (Den (o1,A)) . p1 = (Den (o2,A)) . p2 holds
( o1 = o2 & p1 = p2 )