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:8 ;
hence g = (ovlpart (f,g)) ^ (ovlrdiff (f,g)) ; :: thesis: verum