let k be Element of NAT ; :: thesis: for h being FinSequence holds
( h is CQC-variable_list of k iff ( h is FinSequence of bound_QC-variables & len h = k ) )
let h be FinSequence; :: thesis: ( h is CQC-variable_list of k iff ( h is FinSequence of bound_QC-variables & len h = k ) )
thus ( h is CQC-variable_list of k implies ( h is FinSequence of bound_QC-variables & len h = k ) ) :: thesis: ( h is FinSequence of bound_QC-variables & len h = k implies h is CQC-variable_list of k )

proof

assume A1: h is CQC-variable_list of k ; :: thesis: ( h is FinSequence of bound_QC-variables & len h = k )
then rng h c= bound_QC-variables by RELAT_1:def 19;
hence h is FinSequence of bound_QC-variables by FINSEQ_1:def 4; :: thesis: len h = k
thus len h = k by A1, FINSEQ_1:def 18; :: thesis: verum

end;

thus ( h is FinSequence of bound_QC-variables & len h = k implies h is CQC-variable_list of k ) :: thesis: verum

proof

assume that
A2: h is FinSequence of bound_QC-variables and
A3: len h = k ; :: thesis: h is CQC-variable_list of k
rng h c= bound_QC-variables by A2, FINSEQ_1:def 4;
then rng h c= QC-variables by XBOOLE_1:1;
hence h is CQC-variable_list of k by A2, A3, FINSEQ_1:def 4, FINSEQ_1:def 18; :: thesis: verum

end;