let a be natural Number ; :: thesis: for p, q being FinSequence st a <= len p & q = p | (Seg a) holds
( len q = a & dom q = Seg a )
let p, q be FinSequence; :: thesis: ( a <= len p & q = p | (Seg a) implies ( len q = a & dom q = Seg a ) )
assume that
A1: a <= len p and
A2: q = p | (Seg a) ; :: thesis: ( len q = a & dom q = Seg a )
Seg a c= Seg (len p) by A1, Th5;
then Seg a c= dom p by Def3;
then ( a in NAT & dom q = Seg a ) by A2, ORDINAL1:def 12, RELAT_1:62;
hence ( len q = a & dom q = Seg a ) by Def3; :: thesis: verum