theorem Th3: :: CQC_LANG:3

for A being QC-alphabet
for k being Nat
for f being Substitution of A
for x being bound_QC-variable of A
for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A st f = a .--> x & ll = Subst (l,f) & 1 <= k & k <= len l holds
( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )