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 ) ;
end;
end;
hence len q = min (i,(len p)) by XXREAL_0:def 9; :: thesis: verum