:: deftheorem defines undef-consequent AOFA_A00:def 14 :
for S being non empty non void ManySortedSign
for A being UndefMSAlgebra over S holds
( A is undef-consequent iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) & ex i being Nat ex s being SortSymbol of S ex a being Element of A,s st
( i in dom (the_arity_of o) & s = (the_arity_of o) . i & a = p . i & a is undefined ) holds
for b being Element of A,(the_result_sort_of o) st b = (Den (o,A)) . p holds
b is undefined );