let i be natural Number ; :: thesis: for D, D9 being non empty set st D = Seg i holds
for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9
let D, D9 be non empty set ; :: thesis: ( D = Seg i implies for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9 )
assume A1: D = Seg i ; :: thesis: for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9
let p be FinSequence of D9; :: thesis: for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9
let q be FinSequence of D; :: thesis: ( i <= len p implies p * q is FinSequence of D9 )
assume i <= len p ; :: thesis: p * q is FinSequence of D9
then reconsider pq = p * q as FinSequence by A1, Th28;
( rng pq c= rng p & rng p c= D9 ) by FINSEQ_1:def 4, RELAT_1:26;
then rng pq c= D9 ;
hence p * q is FinSequence of D9 by FINSEQ_1:def 4; :: thesis: verum