let A be QC-alphabet ; :: thesis: for k being Element of NAT
for f being CQC-variable_list of k,A holds f is FinSequence of bound_QC-variables A
let k be Element of 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