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 set ; :: 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 13;

A5: now

( i -' 1 <= i & i <= n ) by A2, FINSEQ_1:3, 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

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