let k be Element of NAT ; :: thesis: for f being CQC-variable_list of k holds f is FinSequence of bound_QC-variables
let f be CQC-variable_list of k; :: thesis: f is FinSequence of bound_QC-variables
rng f c= bound_QC-variables by RELAT_1:def 19;
hence f is FinSequence of bound_QC-variables by FINSEQ_1:def 4; :: thesis: verum