let Al be QC-alphabet ; :: thesis: for k being Nat
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Subst (ll,Sub) is CQC-variable_list of k,Al
let k be Nat; :: thesis: for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Subst (ll,Sub) is CQC-variable_list of k,Al
let ll be CQC-variable_list of k,Al; :: thesis: for Sub being CQC_Substitution of Al holds CQC_Subst (ll,Sub) is CQC-variable_list of k,Al
let Sub be CQC_Substitution of Al; :: thesis: CQC_Subst (ll,Sub) is CQC-variable_list of k,Al
reconsider ll = ll as FinSequence of bound_QC-variables Al by SUBSTUT1:34;
reconsider s = CQC_Subst (ll,Sub) as FinSequence of bound_QC-variables Al ;
A1: s = CQC_Subst ((@ ll),Sub) by SUBSTUT1:def 5;
len ll = k by CARD_1:def 7;
then len (@ ll) = k by SUBSTUT1:def 4;
then len s = k by A1, SUBSTUT1:def 3;
then s is CQC-variable_list of k,Al by SUBSTUT1:34;
hence CQC_Subst (ll,Sub) is CQC-variable_list of k,Al by A1, SUBSTUT1:def 4; :: thesis: verum