let IT1, IT2 be sequence of NAT; :: thesis: ( ( for n being Nat holds IT1 . n = len (s . n) ) & ( for n being Nat holds IT2 . n = len (s . n) ) implies IT1 = IT2 )
assume that
A1: for n being Nat holds IT1 . n = len (s . n) and
A2: for n being Nat holds IT2 . n = len (s . n) ; :: thesis: IT1 = IT2

now :: thesis: for n being Element of NAT holds IT1 . n = IT2 . n

let n be Element of NAT ; :: thesis: IT1 . n = IT2 . n
IT1 . n = len (s . n) by A1;
hence IT1 . n = IT2 . n by A2; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum