:: deftheorem defines -consequent-context-sequence MSAFREE5:def 40 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for B being non empty FinSequence of the carrier of S
for V1, V2 being b₃ -sorts FinSequence of Union X
for D being b₃ -sorts FinSequence of (Free (S,X))
for F being b₅ -context-sequence FinSequence of (Free (S,X)) holds
( F is V1,V2,D -consequent-context-sequence iff for i, j being Element of dom B st i + 1 = j holds
(F . j) -sub ((V1 . j) -term) = (F . i) -sub (D . i) );