let k be Element of NAT ; :: thesis: for l being CQC-variable_list of
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 ; :: 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 )
A1: rng l c= bound_QC-variables by RELAT_1:def 19;
assume ( 1 <= i & i <= len l ) ; :: thesis: l . i in bound_QC-variables
then i in dom l by FINSEQ_3:27;
then l . i in rng l by FUNCT_1:def 5;
hence l . i in bound_QC-variables by A1; :: thesis: verum