let a be Nat; :: thesis: for p being FinSequence holds p | (Seg a) is FinSequence
let p be FinSequence; :: thesis: p | (Seg a) is FinSequence
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 Def2; :: thesis: verum