let S be Real_Sequence; :: thesis: ( S = ||.s.|| iff for n being Element of NAT holds S . n = ||.(s . n).|| )
E1: dom S = NAT by PARTFUN1:def 4;
E2: dom s = NAT by PARTFUN1:def 4;
thus ( S = ||.s.|| implies for n being Element of NAT holds S . n = ||.(s . n).|| ) :: thesis: ( ( for n being Element of NAT holds S . n = ||.(s . n).|| ) implies S = ||.s.|| )

proof

assume Z: S = ||.s.|| ; :: thesis: for n being Element of NAT holds S . n = ||.(s . n).||
let n be Element of NAT ; :: thesis: S . n = ||.(s . n).||
||.s.|| . n = ||.(s /. n).|| by Def1, E1, Z;
hence S . n = ||.(s . n).|| by Z; :: thesis: verum

end;

assume Z: for n being Element of NAT holds S . n = ||.(s . n).|| ; :: thesis: S = ||.s.||
for e being set st e in dom s holds
S . e = ||.(s /. e).||

proof

let e be set ; :: thesis: ( e in dom s implies S . e = ||.(s /. e).|| )
assume Z1: e in dom s ; :: thesis: S . e = ||.(s /. e).||
then reconsider n = e as Element of NAT by PARTFUN1:def 4;
thus S . e = ||.(s . n).|| by Z
.= ||.(s /. e).|| by Z1, PARTFUN1:def 8 ; :: thesis: verum

end;

hence S = ||.s.|| by E1, E2, Def1; :: thesis: verum