let A be QC-alphabet ; :: thesis: for k being Element of NAT
for l being QC-symbol of A
for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let k be Element of NAT ; :: thesis: for l being QC-symbol of A
for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let l be QC-symbol of A; :: thesis: for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
let e be Element of vSUB A; :: thesis: [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
<*[k,l]*> in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
hence [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def 2; :: thesis: verum