let a, b be FinSequence of D; :: thesis: ( len a <= len g & a = smid g,1,(len a) & a = smid f,(((len f) -' (len a)) + 1),(len f) & ( for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len a ) & len b <= len g & b = smid g,1,(len b) & b = smid f,(((len f) -' (len b)) + 1),(len f) & ( for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len b ) implies a = b )
assume A10: ( len a <= len g & a = smid g,1,(len a) & a = smid f,(((len f) -' (len a)) + 1),(len f) & ( for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len a ) & len b <= len g & b = smid g,1,(len b) & b = smid f,(((len f) -' (len b)) + 1),(len f) & ( for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len b ) ) ; :: thesis: a = b
then A11: len a <= len b ;
len b <= len a by A10;
hence a = b by A10, A11, XXREAL_0:1; :: thesis: verum