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