:: deftheorem Def8 defines inheriting_operations MSAFREE4:def 8 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms MSAlgebra over S holds
( A is inheriting_operations iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of A . (the_result_sort_of o) holds
( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) );