let i be Nat; :: thesis: for q, p being FinSequence st q = p | (Seg i) holds
len q = min i,(len p)
let q, p 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

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:21; :: thesis: verum

end;

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

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

end;

end;

end;

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