let D be non empty set ; :: thesis: for f, g being FinSequence of D holds
( ovlcon f,g = ((ovlldiff f,g) ^ (ovlpart f,g)) ^ (ovlrdiff f,g) & ovlcon f,g = (ovlldiff f,g) ^ ((ovlpart f,g) ^ (ovlrdiff f,g)) )
let f, g be FinSequence of D; :: thesis: ( ovlcon f,g = ((ovlldiff f,g) ^ (ovlpart f,g)) ^ (ovlrdiff f,g) & ovlcon f,g = (ovlldiff f,g) ^ ((ovlpart f,g) ^ (ovlrdiff f,g)) )
(ovlpart f,g) ^ (g /^ (len (ovlpart f,g))) = (smid g,1,(len (ovlpart f,g))) ^ (g /^ (len (ovlpart f,g))) by Def2
.= (g | (len (ovlpart f,g))) ^ (g /^ (len (ovlpart f,g))) by Th5
.= g by RFINSEQ:21 ;
hence ovlcon f,g = (f | ((len f) -' (len (ovlpart f,g)))) ^ ((ovlpart f,g) ^ (g /^ (len (ovlpart f,g)))) by Th11
.= ((ovlldiff f,g) ^ (ovlpart f,g)) ^ (ovlrdiff f,g) by FINSEQ_1:45 ;
:: thesis: ovlcon f,g = (ovlldiff f,g) ^ ((ovlpart f,g) ^ (ovlrdiff f,g))
hence ovlcon f,g = (ovlldiff f,g) ^ ((ovlpart f,g) ^ (ovlrdiff f,g)) by FINSEQ_1:45; :: thesis: verum