set l = k |-> (x. 0 );
A1: len (k |-> (x. 0 )) = k by FINSEQ_2:69;
B2: dom (k |-> (x. 0 )) = Seg k by FUNCOP_1:19;
rng (k |-> (x. 0 )) c= QC-variables

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (k |-> (x. 0 )) or y in QC-variables )
assume y in rng (k |-> (x. 0 )) ; :: thesis: y in QC-variables
then consider x being set such that
A3: x in dom (k |-> (x. 0 )) and
A4: (k |-> (x. 0 )) . x = y by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3;
y = x. 0 by B2, A4, A3, FINSEQ_2:71;
hence y in QC-variables ; :: thesis: verum

end;

then k |-> (x. 0 ) is FinSequence of QC-variables by FINSEQ_1:def 4;
then reconsider l = k |-> (x. 0 ) as QC-variable_list of k by A1, QC_LANG1:def 8;
take l ; :: thesis: l is CQC-variable_list-like
let x be set ; :: according to TARSKI:def 3,CQC_LANG:def 5 :: thesis: ( not x in rng l or x in bound_QC-variables )
assume x in rng l ; :: thesis: x in bound_QC-variables
then consider i being set such that
A5: i in dom l and
A6: x = l . i by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A5;
l . i = x. 0 by B2, A5, FINSEQ_2:71;
hence x in bound_QC-variables by A6; :: thesis: verum