let A be QC-alphabet ; for k being Nat
for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
let k be Nat; for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
let x be QC-symbol of A; <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
k in NAT
by ORDINAL1:def 12;
then
[k,x] in [:NAT,(QC-symbols A):]
by ZFMISC_1:def 2;
then
( rng <*[k,x]*> = {[k,x]} & {[k,x]} c= [:NAT,(QC-symbols A):] )
by FINSEQ_1:39, ZFMISC_1:31;
hence
<*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
by FINSEQ_1:def 4; verum