let A be QC-alphabet ; :: thesis: for k being Nat
for l being CQC-variable_list of k,A
for i being Nat st 1 <= i & i <= len l holds
l . i in bound_QC-variables A
let k be Nat; :: thesis: for l being CQC-variable_list of k,A
for i being Nat st 1 <= i & i <= len l holds
l . i in bound_QC-variables A
let l be CQC-variable_list of k,A; :: thesis: for i being Nat st 1 <= i & i <= len l holds
l . i in bound_QC-variables A
let i be Nat; :: thesis: ( 1 <= i & i <= len l implies l . i in bound_QC-variables A )
assume that
A1: 1 <= i and
A2: i <= len l ; :: thesis: l . i in bound_QC-variables A
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 A by RELAT_1:def 19;
hence l . i in bound_QC-variables A by A3; :: thesis: verum