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