let a be natural Number ; :: thesis: for p being FinSequence holds p | (Seg a) is FinSequence
let p be FinSequence; :: thesis: p | (Seg a) is FinSequence
A0: a is Nat by TARSKI:1;
A1: dom (p | (Seg a)) = (dom p) /\ (Seg a) by RELAT_1:61
.= (Seg (len p)) /\ (Seg a) by Def3 ;
( len p <= a or a <= len p ) ;
then ( dom (p | (Seg a)) = Seg (len p) or dom (p | (Seg a)) = Seg a ) by A1, Th5, XBOOLE_1:28;
hence p | (Seg a) is FinSequence by A0, Def2; :: thesis: verum