let a be natural Number ; :: thesis: for D being set
for p being b₁ -valued FinSequence holds p | (Seg a) is FinSequence of D
let D be set ; :: thesis: for p being D -valued FinSequence holds p | (Seg a) is FinSequence of D
let p be D -valued FinSequence; :: thesis: p | (Seg a) is FinSequence of D
A1: p | (Seg a) is FinSequence by Th15;
( rng (p | (Seg a)) c= rng p & rng p c= D ) by RELAT_1:70, RELAT_1:def 19;
hence p | (Seg a) is FinSequence of D by A1, Def4, XBOOLE_1:1; :: thesis: verum