let D be non empty set ; 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; ( 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; verum