set null = 0 ;
reconsider null = 0 as QC-symbol of A by QC_LANG1:3;
set l = k |-> (x. null);
rng (k |-> (x. null)) c= QC-variables A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (k |-> (x. null)) or y in QC-variables A )
assume y in rng (k |-> (x. null)) ; :: thesis: y in QC-variables A
then consider x being object such that
A2: x in dom (k |-> (x. null)) and
A3: (k |-> (x. null)) . x = y by FUNCT_1:def 3;
y = x. null by A2, A3, FINSEQ_2:57;
hence y in QC-variables A ; :: thesis: verum
end;
then reconsider l = k |-> (x. null) as QC-variable_list of k,A by FINSEQ_1:def 4;
take l ; :: thesis: l is bound_QC-variables A -valued
let x be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in rng l or x in bound_QC-variables A )
assume x in rng l ; :: thesis: x in bound_QC-variables A
then consider i being object such that
A4: i in dom l and
A5: x = l . i by FUNCT_1:def 3;
reconsider i = i as Nat by A4;
l . i = x. null by A4, FINSEQ_2:57;
hence x in bound_QC-variables A by A5; :: thesis: verum