let IT1, IT2 be FinSequence of D; ( 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 ) ) )
; IT1 = IT2
A3:
dom IT1 = dom IT2
by A1, A2, FINSEQ_3:29;
hence
IT1 = IT2
by A1, A2, FINSEQ_3:29, FINSEQ_1:13; verum