deffunc H₁( Element of Segm n) -> Element of Seg n = ntoSeg n;
A1: for x being Element of Segm n holds H₁(x) is Element of Seg n ;
consider f being Function of (Segm n),(Seg n) such that
A2: for x being Element of Segm n holds f . x = H₁(x) from FUNCT_2:sch 9(A1);
take f ; :: thesis: f is NtoSEG
thus f is NtoSEG by A2; :: thesis: verum