let A be QC-alphabet ; 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; 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; 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; [<*[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; verum