:: deftheorem defines -undef AOFA_A00:def 15 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for B being UndefMSAlgebra over S holds
( B is A -undef iff ( B is undef-consequent & the undefined-map of B = the Sorts of A & ( for s being SortSymbol of S holds the Sorts of B . s = succ ( the Sorts of A . s) ) & ( for o being OperSymbol of S
for a being Element of Args (o,A) st Args (o,A) <> {} & (Den (o,B)) . a <> (Den (o,A)) . a holds
(Den (o,B)) . a = the undefined-map of B . (the_result_sort_of o) ) ) );