let S be Real_Sequence; :: thesis: ( S = ||.s.|| iff for n being Element of 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 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 A4: 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 Def2, A2, A4;
hence S . n = ||.(s . n).|| by A4; :: thesis: verum

end;

assume A5: 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 A6: 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 A5
.= ||.(s /. e).|| by A6, PARTFUN1:def 6 ; :: thesis: verum

end;

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