deffunc H₂( Element of NAT ) -> Real = ||.(S . $1).||;
consider s being Real_Sequence such that
A1: for n being Element of NAT holds s . n = H₂(n) from SEQ_1:sch 1();
take s ; :: thesis: for n being Element of NAT holds s . n = ||.(S . n).||
thus for n being Element of NAT holds s . n = ||.(S . n).|| by A1; :: thesis: verum