deffunc H₂( Element of NAT ) -> Element of REAL = ||.(seq . $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 = ||.(seq . n).||
thus for n being Element of NAT holds s . n = ||.(seq . n).|| by A1; :: thesis: verum