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

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