:: deftheorem Def1 defines Subst CQC_LANG:def 1 :
for A being QC-alphabet
for l being FinSequence of QC-variables A
for f being Substitution of A
for b₄ being FinSequence of QC-variables A holds
( b₄ = Subst (l,f) iff ( len b₄ = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies b₄ . k = f . (l . k) ) & ( not l . k in dom f implies b₄ . k = l . k ) ) ) ) );