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