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