let k be Element of NAT ; :: thesis: for l being CQC-variable_list of k
for i being Element of NAT st 1 <= i & i <= len l holds
l . i in bound_QC-variables
let l be CQC-variable_list of k; :: thesis: for i being Element of NAT st 1 <= i & i <= len l holds
l . i in bound_QC-variables
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len l implies l . i in bound_QC-variables )
assume that
A1: 1 <= i and
A2: i <= len l ; :: thesis: l . i in bound_QC-variables
i in dom l by A1, A2, FINSEQ_3:25;
then A3: l . i in rng l by FUNCT_1:def 3;
rng l c= bound_QC-variables by RELAT_1:def 19;
hence l . i in bound_QC-variables by A3; :: thesis: verum