:: deftheorem Def3 defines CQC_Subst SUBSTUT1:def 3 :
for A being QC-alphabet
for l being FinSequence of QC-variables A
for Sub being CQC_Substitution of A
for b₄ being FinSequence of QC-variables A holds
( b₄ = CQC_Subst (l,Sub) iff ( len b₄ = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies b₄ . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b₄ . k = l . k ) ) ) ) );