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