let A be QC-alphabet ; :: thesis: for k being 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 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):]
A1: k in NAT by ORDINAL1:def 12;
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):]
reconsider kl = [k,l] as Element of [:NAT,(QC-symbols A):] by A1, ZFMISC_1:def 2;
<*kl*> 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