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

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