let i, j be Nat; :: 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:45;
then A2: rng (p * f) c= D by XBOOLE_1:1;
p * f is FinSequence by A1, Th42;
hence p * f is FinSequence of D by A2, FINSEQ_1:def 4; :: thesis: verum