:: deftheorem defines -context_including MSAFREE5:def 24 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) holds
( p is x -context_including iff ex i being Nat st
( i in dom p & p . i is context of x & ( for j being Nat
for t being Element of (Free (S,X)) st j in dom p & j <> i & t = p . j holds
t is x -omitting ) ) );