:: deftheorem CNST defines -constant MSAFREE5:def 29 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s
for h being ManySortedFunction of (Free (S,X)),T holds
( h is x -constant iff ( h . (x -term) = x -term & ( for s1 being SortSymbol of S
for x1 being Element of X . s1 st ( x1 <> x or s <> s1 ) holds
h . (x1 -term) is x -omitting ) ) );