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