let a be Nat; :: 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 Th19;
( rng (p | (Seg a)) c= rng p & rng p c= D ) by Def4, RELAT_1:70;
then rng (p | (Seg a)) c= D by XBOOLE_1:1;
hence p | (Seg a) is FinSequence of D by A1, Def4; :: thesis: verum