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

( 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