set l = k |-> (x. 0 );
A1: 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
A2: x in dom (k |-> (x. 0 )) and
A3: (k |-> (x. 0 )) . x = y by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A2;
y = x. 0 by A1, A2, A3, FINSEQ_2:71;
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 5;
reconsider i = i as Element of NAT by A4;
l . i = x. 0 by A1, A4, FINSEQ_2:71;
hence x in bound_QC-variables by A5; :: thesis: verum