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)))) by Def2;
((len f) -' (len f)) + 1 = ((len f) - (len f)) + 1 by XREAL_1:233
.= 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:34 ;
A4: ovlldiff (f,f) = f | ((len f) -' (len f)) by A1, A2, Th6
.= f | 0 by XREAL_1:232
.= {} ;
ovlrdiff (f,f) = {} 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