:: deftheorem CONTEXTSEQ defines -context-sequence MSAFREE5:def 38 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for B being non empty FinSequence of the carrier of S
for V being b₃ -sorts FinSequence of Union X
for F being FinSequence of (Free (S,X)) holds
( F is V -context-sequence iff ( dom F = dom B & ( for i being Element of dom B holds F . i is context of V . i ) ) );