deffunc H₁( Nat) -> set = {$1,(max (($1 -' 1),1)),(min (($1 + 1),n))};
A1: for x being Element of NAT st x in Seg n holds
H₁(x) c= Seg n

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies H₁(i) c= Seg n )
set y0 = {i,(max ((i -' 1),1)),(min ((i + 1),n))};
assume A2: i in Seg n ; :: thesis: H₁(i) c= Seg n
then Seg n <> {} ;
then n > 0 ;
then A3: 0 + 1 <= n by NAT_1:13;
thus {i,(max ((i -' 1),1)),(min ((i + 1),n))} c= Seg n :: thesis: verum

proof

let z1 be object ; :: according to TARSKI:def 3 :: thesis: ( not z1 in {i,(max ((i -' 1),1)),(min ((i + 1),n))} or z1 in Seg n )
assume A4: z1 in {i,(max ((i -' 1),1)),(min ((i + 1),n))} ; :: thesis: z1 in Seg n
then ( z1 = i or z1 = max ((i -' 1),1) or z1 = min ((i + 1),n) ) by ENUMSET1:def 1;
then reconsider z2 = z1 as Element of NAT by ORDINAL1:def 12;

A5: now :: thesis: ( z1 = max ((i -' 1),1) implies z1 in Seg n )

( i -' 1 <= i & i <= n ) by A2, FINSEQ_1:1, NAT_D:35;
then i -' 1 <= n by XXREAL_0:2;
then A6: ( 1 <= max ((i -' 1),1) & max ((i -' 1),1) <= n ) by A3, XXREAL_0:28, XXREAL_0:30;
assume z1 = max ((i -' 1),1) ; :: thesis: z1 in Seg n
hence z1 in Seg n by A6; :: thesis: verum

end;

now :: thesis: ( z1 = min ((i + 1),n) implies z2 in Seg n )

1 <= i + 1 by NAT_1:12;
then A7: 1 <= min ((i + 1),n) by A3, XXREAL_0:20;
A8: min ((i + 1),n) <= n by XXREAL_0:17;
assume z1 = min ((i + 1),n) ; :: thesis: z2 in Seg n
hence z2 in Seg n by A7, A8; :: thesis: verum

end;

hence z1 in Seg n by A2, A4, A5, ENUMSET1:def 1; :: thesis: verum

end;

end;

consider f being Relation of (Seg n) such that
A9: for x3 being Element of NAT st x3 in Seg n holds
Im (f,x3) = H₁(x3) from RELSET_1:sch 3(A1);
take f ; :: thesis: for i being Element of NAT st i in Seg n holds
Im (f,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))}
thus for i being Element of NAT st i in Seg n holds
Im (f,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} by A9; :: thesis: verum