let a be natural Number ; :: thesis: for D being set
for p being FinSequence of D holds p | (Seg a) is FinSequence of D
let D be set ; :: thesis: for p being FinSequence of D holds p | (Seg a) is FinSequence of D
let p be FinSequence of D; :: 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 Def4, RELAT_1:70;
hence p | (Seg a) is FinSequence of D by A1, Def4, XBOOLE_1:1; :: thesis: verum