reconsider y = <*[3,0 ]*> as FinSequence of [:NAT ,NAT :] ;
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 QC_LANG1:4, 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