reconsider y = <*[3,0]*> as FinSequence of [:NAT,NAT:] by Lm1;
let x be bound_QC-variable; :: thesis: for p being FinSequence of [:NAT,NAT:] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,NAT:]
let p be FinSequence of [:NAT,NAT:]; :: thesis: (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,NAT:]
bound_QC-variables c= [:NAT,NAT:] by Th4, XBOOLE_1:1;
then rng <*x*> c= [:NAT,NAT:] by XBOOLE_1:1;
then reconsider z = <*x*> as FinSequence of [:NAT,NAT:] by FINSEQ_1:def 4;
(y ^ z) ^ p is FinSequence of [:NAT,NAT:] ;
hence (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,NAT:] ; :: thesis: verum