let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of
for Sub being CQC_Substitution holds CQC_Subst ll,Sub is CQC-variable_list of
let ll be CQC-variable_list of ; :: thesis: for Sub being CQC_Substitution holds CQC_Subst ll,Sub is CQC-variable_list of
let Sub be CQC_Substitution; :: thesis: CQC_Subst ll,Sub is CQC-variable_list of
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 FINSEQ_1:def 18;
then len (@ ll) = k by SUBSTUT1:def 4;
then len s = k by A1, SUBSTUT1:def 3;
then s is CQC-variable_list of by SUBSTUT1:34;
hence CQC_Subst ll,Sub is CQC-variable_list of by A1, SUBSTUT1:def 4; :: thesis: verum