let D be non empty set ; :: thesis: for f, g being FinSequence of D holds g = (ovlpart f,g) ^ (ovlrdiff f,g)
let f, g be FinSequence of D; :: thesis: g = (ovlpart f,g) ^ (ovlrdiff f,g)
ovlpart f,g = smid g,1,(len (ovlpart f,g)) by FINSEQ_8:def 2
.= g | (len (ovlpart f,g)) by FINSEQ_8:5 ;
then (ovlpart f,g) ^ (ovlrdiff f,g) = (g | (len (ovlpart f,g))) ^ (g /^ (len (ovlpart f,g))) by FINSEQ_8:def 5
.= g by RFINSEQ:21 ;
hence g = (ovlpart f,g) ^ (ovlrdiff f,g) ; :: thesis: verum