let i be natural Number ; :: thesis: for D being non empty set st D = Seg i holds
for p being FinSequence
for q being FinSequence of D st i <= len p holds
p * q is FinSequence
let D be non empty set ; :: thesis: ( D = Seg i implies for p being FinSequence
for q being FinSequence of D st i <= len p holds
p * q is FinSequence )
assume A1: D = Seg i ; :: thesis: for p being FinSequence
for q being FinSequence of D st i <= len p holds
p * q is FinSequence
let p be FinSequence; :: thesis: for q being FinSequence of D st i <= len p holds
p * q is FinSequence
let q be FinSequence of D; :: thesis: ( i <= len p implies p * q is FinSequence )
assume i <= len p ; :: thesis: p * q is FinSequence
then Seg i c= Seg (len p) by FINSEQ_1:5;
then A2: Seg i c= dom p by FINSEQ_1:def 3;
rng q c= Seg i by A1, FINSEQ_1:def 4;
then dom (p * q) = dom q by A2, RELAT_1:27, XBOOLE_1:1;
then dom (p * q) = Seg (len q) by FINSEQ_1:def 3;
hence p * q is FinSequence by FINSEQ_1:def 2; :: thesis: verum