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):]
A1: 0 is QC-symbol of A by Th3;
reconsider y = <*[3,0]*> as FinSequence of [:NAT,(QC-symbols A):] by A1, Lm2;
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 Th4;
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