let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
0 in QC-symbols A by QC_LANG1:3;
then [3,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87;
then ( rng <*[3,0]*> = {[3,0]} & {[3,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31;
then reconsider y = <*[3,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def 4;
let x be bound_QC-variable of A; :: thesis: for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
let p be FinSequence of [:NAT,(QC-symbols A):]; :: thesis: (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
QC-variables A c= [:NAT,(QC-symbols A):] by QC_LANG1:4;
then bound_QC-variables A c= [:NAT,(QC-symbols A):] ;
then rng <*x*> c= [:NAT,(QC-symbols A):] ;
then reconsider z = <*x*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def 4;
(y ^ z) ^ p is FinSequence of [:NAT,(QC-symbols A):] ;
hence (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] ; :: thesis: verum