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 )
assume A2: i in Seg n ; :: thesis: H₁(i) c= Seg n
then n > 0 by FINSEQ_1:4;
then A3: 0 + 1 <= n by NAT_1:13;
set y0 = {i,(max (i -' 1),1),(min (i + 1),n)};
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 ( z1 = i or z1 = i -' 1 or z1 = 1 or z1 = i + 1 or z1 = n ) by XXREAL_0:15, XXREAL_0:16;
then reconsider z2 = z1 as Element of NAT by ORDINAL1:def 13;

A5: now

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

end;

now

assume A8: z1 = min (i + 1),n ; :: thesis: z2 in Seg n
1 <= i + 1 by NAT_1:12;
then A9: 1 <= min (i + 1),n by A3, XXREAL_0:20;
min (i + 1),n <= n by XXREAL_0:17;
hence z2 in Seg n by A8, A9; :: 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
A10: 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 A10; :: thesis: verum