let IT1, IT2 be FinSequence of NAT ; :: thesis: ( dom IT1 = dom F & ( for n being Nat st n in dom IT1 holds
IT1 . n = len (F . n) ) & dom IT2 = dom F & ( for n being Nat st n in dom IT2 holds
IT2 . n = len (F . n) ) implies IT1 = IT2 )
assume that
A1: ( dom IT1 = dom F & ( for n being Nat st n in dom IT1 holds
IT1 . n = len (F . n) ) ) and
A2: ( dom IT2 = dom F & ( for n being Nat st n in dom IT2 holds
IT2 . n = len (F . n) ) ) ; :: thesis: IT1 = IT2
A3: len IT1 = len IT2 by A1, A2, FINSEQ_3:29;

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

let k be Nat; :: thesis: ( k in dom IT1 implies IT1 . k = IT2 . k )
assume k in dom IT1 ; :: thesis: IT1 . k = IT2 . k
then ( IT1 . k = len (F . k) & IT2 . k = len (F . k) ) by A1, A2;
hence IT1 . k = IT2 . k ; :: thesis: verum

end;

hence IT1 = IT2 by A3, FINSEQ_2:9; :: thesis: verum