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:79 ;
((len (f ^ g)) -' (len g)) + 1 = (((len f) + (len g)) -' (len g)) + 1 by FINSEQ_1:35
.= (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:35
.= 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:79 ;
A5: len (ovlpart f,(f ^ g)) <= len f by Th10;
((len f) -' (len f)) + 1 = 0 + 1 by XREAL_1:234
.= 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:31
.= f by FINSEQ_1:79 ;
len f <= (len f) + (len g) by NAT_1:12;
then A7: len f <= len (f ^ g) by FINSEQ_1:35;
smid (f ^ g),1,(len f) = (f ^ g) | (len f) by Th5
.= f by FINSEQ_5:26 ;
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:26 ;
hence ( ovlpart (f ^ g),g = g & ovlpart f,(f ^ g) = f ) by A4; :: thesis: verum