let s, t be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds s . n = ||.(S . n).|| ) & ( for n being Element of NAT holds t . n = ||.(S . n).|| ) implies s = t )
assume A2: ( ( for n being Element of NAT holds s . n = ||.(S . n).|| ) & ( for n being Element of NAT holds t . n = ||.(S . n).|| ) ) ; :: thesis: s = t

now

let n be Element of NAT ; :: thesis: s . n = t . n
s . n = ||.(S . n).|| by A2;
hence s . n = t . n by A2; :: thesis: verum

end;

hence s = t by FUNCT_2:113; :: thesis: verum