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 that
A10: len a <= len g and
A11: a = smid g,1,(len a) and
A12: a = smid f,(((len f) -' (len a)) + 1),(len f) and
A13: for j being Nat st j <= len g & smid g,1,j = smid f,(((len f) -' j) + 1),(len f) holds
j <= len a and
A14: len b <= len g and
A15: b = smid g,1,(len b) and
A16: b = smid f,(((len f) -' (len b)) + 1),(len f) and
A17: 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
A18: len a <= len b by A10, A11, A12, A17;
len b <= len a by A13, A14, A15, A16;
hence a = b by A11, A15, A18, XXREAL_0:1; :: thesis: verum