let D be non empty set ; for f, g being FinSequence of D holds
( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f )
let f, g be FinSequence of D; ( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f )
A1:
len (ovlpart ((f ^ g),g)) <= len g
by Def2;
A2: smid (g,1,(len g)) =
g | (len g)
by Th5
.=
g
by FINSEQ_1:58
;
((len (f ^ g)) -' (len g)) + 1 =
(((len f) + (len g)) -' (len g)) + 1
by FINSEQ_1:22
.=
(len f) + 1
by NAT_D:34
;
then smid ((f ^ g),(((len (f ^ g)) -' (len g)) + 1),(len (f ^ g))) =
smid ((f ^ g),((len f) + 1),((len f) + (len g)))
by FINSEQ_1:22
.=
g
by Th9
;
then
len g <= len (ovlpart ((f ^ g),g))
by A2, Def2;
then A3:
len g = len (ovlpart ((f ^ g),g))
by A1, XXREAL_0:1;
A4: ovlpart ((f ^ g),g) =
smid (g,1,(len (ovlpart ((f ^ g),g))))
by Def2
.=
g | (len g)
by A3, Th5
.=
g
by FINSEQ_1:58
;
A5:
len (ovlpart (f,(f ^ g))) <= len f
by Th10;
((len f) -' (len f)) + 1 =
0 + 1
by XREAL_1:232
.=
1
;
then A6: smid (f,(((len f) -' (len f)) + 1),(len f)) =
(f /^ ((0 + 1) -' 1)) | (len f)
by NAT_D:34
.=
(f /^ 0) | (len f)
by NAT_D:34
.=
f | (len f)
by FINSEQ_5:28
.=
f
by FINSEQ_1:58
;
len f <= (len f) + (len g)
by NAT_1:12;
then A7:
len f <= len (f ^ g)
by FINSEQ_1:22;
smid ((f ^ g),1,(len f)) =
(f ^ g) | (len f)
by Th5
.=
f
by FINSEQ_5:23
;
then
len f <= len (ovlpart (f,(f ^ g)))
by A6, A7, Def2;
then A8:
len f = len (ovlpart (f,(f ^ g)))
by A5, XXREAL_0:1;
ovlpart (f,(f ^ g)) =
smid ((f ^ g),1,(len (ovlpart (f,(f ^ g)))))
by Def2
.=
(f ^ g) | (len f)
by A8, Th5
.=
f
by FINSEQ_5:23
;
hence
( ovlpart ((f ^ g),g) = g & ovlpart (f,(f ^ g)) = f )
by A4; verum