let IT1, IT2 be FinSequence of D; :: thesis: ( len IT1 = Sum (Length F) & ( for n being Nat st n in dom IT1 holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & IT1 . n = (F . (k + 1)) . m ) ) & len IT2 = Sum (Length F) & ( for n being Nat st n in dom IT2 holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & IT2 . n = (F . (k + 1)) . m ) ) implies IT1 = IT2 )
assume that
A1: ( len IT1 = Sum (Length F) & ( for n being Nat st n in dom IT1 holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & IT1 . n = (F . (k + 1)) . m ) ) ) and
A2: ( len IT2 = Sum (Length F) & ( for n being Nat st n in dom IT2 holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & IT2 . n = (F . (k + 1)) . m ) ) ) ; :: thesis: IT1 = IT2
A3: dom IT1 = dom IT2 by A1, A2, FINSEQ_3:29;

now :: thesis: for n being Nat st n in dom IT1 holds
IT1 . n = IT2 . n

let n be Nat; :: thesis: ( n in dom IT1 implies IT1 . n = IT2 . n )
assume A4: n in dom IT1 ; :: thesis: IT1 . n = IT2 . n
then consider k1, m1 being Nat such that
A5: ( 1 <= m1 & m1 <= len (F . (k1 + 1)) & k1 < len F & m1 + (Sum (Length (F | k1))) = n & n <= Sum (Length (F | (k1 + 1))) & IT1 . n = (F . (k1 + 1)) . m1 ) by A1;
consider k2, m2 being Nat such that
A6: ( 1 <= m2 & m2 <= len (F . (k2 + 1)) & k2 < len F & m2 + (Sum (Length (F | k2))) = n & n <= Sum (Length (F | (k2 + 1))) & IT2 . n = (F . (k2 + 1)) . m2 ) by A2, A3, A4;
( k1 = k2 & m1 = m2 ) by A5, A6, Th6;
hence IT1 . n = IT2 . n by A5, A6; :: thesis: verum

end;

hence IT1 = IT2 by A1, A2, FINSEQ_3:29, FINSEQ_1:13; :: thesis: verum