let i be natural Number ; :: thesis: for p, q being FinSequence st q = p | (Seg i) holds
len q = min (i,(len p))
let p, q be FinSequence; :: thesis: ( q = p | (Seg i) implies len q = min (i,(len p)) )
assume A1: q = p | (Seg i) ; :: thesis: len q = min (i,(len p))

now :: thesis: ( ( i <= len p & len q = i ) or ( not i <= len p & len q = len p ) )

per cases ( i <= len p or not i <= len p ) ;

case i <= len p ; :: thesis: len q = i

hence len q = i by A1, FINSEQ_1:17; :: thesis: verum

end;

case not i <= len p ; :: thesis: len q = len p

hence len q = len p by A1, Th18; :: thesis: verum

end;

end;

end;

hence len q = min (i,(len p)) by XXREAL_0:def 9; :: thesis: verum