let k be Element of NAT ; :: thesis: for f being FinSequence of bound_QC-variables st len f = k holds
f is CQC-variable_list of k
let f be FinSequence of bound_QC-variables ; :: thesis: ( len f = k implies f is CQC-variable_list of k )
assume A1: len f = k ; :: thesis: f is CQC-variable_list of k
f is FinSequence of QC-variables by FINSEQ_2:27;
then A2: ( f is QC-variable_list of k & rng f = { (f . i) where i is Element of NAT : ( 1 <= i & i <= len f ) } ) by A1, Th9, QC_LANG1:def 8;
then ( f is QC-variable_list of k & { (f . i) where i is Element of NAT : ( 1 <= i & i <= len f ) } c= bound_QC-variables ) by FINSEQ_1:def 4;
hence f is CQC-variable_list of k by A2, CQC_LANG:def 5; :: thesis: verum