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