let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds CQC_Subst (ll,Sub) is CQC-variable_list of k
let ll be CQC-variable_list of k; :: thesis: for Sub being CQC_Substitution holds CQC_Subst (ll,Sub) is CQC-variable_list of k
let Sub be CQC_Substitution; :: thesis: CQC_Subst (ll,Sub) is CQC-variable_list of k
reconsider ll = ll as FinSequence of bound_QC-variables by SUBSTUT1:34;
reconsider s = CQC_Subst (ll,Sub) as FinSequence of bound_QC-variables ;
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 by SUBSTUT1:34;
hence CQC_Subst (ll,Sub) is CQC-variable_list of k by A1, SUBSTUT1:def 4; :: thesis: verum