let S be Real_Sequence; :: thesis: ( S = ||.s.|| iff for n being Nat holds S . n = ||.(s . n).|| )
A2: dom S = NAT by PARTFUN1:def 2;
A3: dom s = NAT by PARTFUN1:def 2;
thus ( S = ||.s.|| implies for n being Nat holds S . n = ||.(s . n).|| ) :: thesis: ( ( for n being Nat holds S . n = ||.(s . n).|| ) implies S = ||.s.|| )

proof

assume A4: S = ||.s.|| ; :: thesis: for n being Nat holds S . n = ||.(s . n).||
let n be Nat; :: thesis: S . n = ||.(s . n).||
A5: n in NAT by ORDINAL1:def 12;
thus S . n = ||.s.|| . n by A4
.= ||.(s /. n).|| by Def2, A2, A4, A5
.= ||.(s . n).|| by A3, A5, PARTFUN1:def 6 ; :: thesis: verum

end;

assume A6: for n being 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 A7: e in dom s ; :: thesis: S . e = ||.(s /. e).||
then reconsider n = e as Element of NAT by PARTFUN1:def 2;
thus S . e = ||.(s . n).|| by A6
.= ||.(s /. e).|| by A7, PARTFUN1:def 6 ; :: thesis: verum

end;

hence S = ||.s.|| by A2, A3, Def2; :: thesis: verum