let A be QC-alphabet ; :: thesis: for k being Element of NAT
for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
let k be Element of NAT ; :: thesis: for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
let x be QC-symbol of A; :: thesis: <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
[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; :: thesis: verum