let D be non empty set ; :: thesis: for f being FinSequence of D holds
( ovlcon f,f = f & ovlpart f,f = f & ovlldiff f,f = {} & ovlrdiff f,f = {} )
let f be FinSequence of D; :: thesis: ( ovlcon f,f = f & ovlpart f,f = f & ovlldiff f,f = {} & ovlrdiff f,f = {} )
A1: ( ovlpart f,f = smid f,1,(len (ovlpart f,f)) & ovlpart f,f = smid f,(((len f) -' (len (ovlpart f,f))) + 1),(len f) ) by Def2;
((len f) -' (len f)) + 1 = ((len f) - (len f)) + 1 by XREAL_1:235
.= 0 + 1 ;
then smid f,1,(len f) = smid f,(((len f) -' (len f)) + 1),(len f) ;
then A2: len f <= len (ovlpart f,f) by Def2;
then A3: ovlcon f,f = f ^ (<*> D) by Th2
.= f by FINSEQ_1:47 ;
A4: ovlldiff f,f = f | ((len f) -' (len f)) by A1, A2, Th6
.= f | 0 by XREAL_1:234
.= {} ;
ovlrdiff f,f = <*> D by A2, Th2
.= {} ;
hence ( ovlcon f,f = f & ovlpart f,f = f & ovlldiff f,f = {} & ovlrdiff f,f = {} ) by A1, A2, A3, A4, Th6; :: thesis: verum