deffunc H1( Nat) -> set = {$1,(max (($1 -' 1),1)),(min (($1 + 1),n))};
A1:
for x being Element of NAT st x in Seg n holds
H1(x) c= Seg n
proof
let i be
Element of
NAT ;
( i in Seg n implies H1(i) c= Seg n )
set y0 =
{i,(max ((i -' 1),1)),(min ((i + 1),n))};
assume A2:
i in Seg n
;
H1(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
verumproof
let z1 be
object ;
TARSKI:def 3 ( 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))}
;
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;
hence
z1 in Seg n
by A2, A4, A5, ENUMSET1:def 1;
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) = H1(x3)
from RELSET_1:sch 3(A1);
take
f
; 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; verum