set l = k |-> (x. 0 );
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 reconsider l = k |-> (x. 0 ) as QC-variable_list of 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 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