set l = k |-> (x. 0);
A1: dom (k |-> (x. 0)) = Seg k by FUNCOP_1:13;
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
A2: x in dom (k |-> (x. 0)) and
A3: (k |-> (x. 0)) . x = y by FUNCT_1:def 3;
y = x. 0 by A1, A2, A3, FINSEQ_2:57;
hence y in QC-variables ; :: thesis: verum

end;

then reconsider l = k |-> (x. 0) as QC-variable_list of k by FINSEQ_1:def 4;
take l ; :: thesis: l is bound_QC-variables -valued
let x be set ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in proj2 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
A4: i in dom l and
A5: x = l . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A4;
l . i = x. 0 by A1, A4, FINSEQ_2:57;
hence x in bound_QC-variables by A5; :: thesis: verum