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