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