defpred S1[ object , object ] means for i being Element of NAT st i = $1 holds
( ( 1 < i & i < n implies $2 = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies $2 = {i,n,(i + 1)} ) & ( 1 < i & i = n implies $2 = {i,(i -' 1),1} ) & ( i = 1 & i = n implies $2 = {i} ) );
A1:
for x being object st x in Seg n holds
ex y being object st
( y in bool (Seg n) & S1[x,y] )
proof
let x be
object ;
( x in Seg n implies ex y being object st
( y in bool (Seg n) & S1[x,y] ) )
assume A2:
x in Seg n
;
ex y being object st
( y in bool (Seg n) & S1[x,y] )
then reconsider i2 =
x as
Element of
NAT ;
A3:
( 1
<= i2 &
i2 <= n )
by A2, FINSEQ_1:1;
now ( ( 1 < i2 & i2 < n & ex y being object st
( y in bool (Seg n) & S1[x,y] ) ) or ( i2 = 1 & i2 < n & ex y being object st
( y in bool (Seg n) & S1[x,y] ) ) or ( 1 < i2 & i2 = n & ex y being object st
( y in bool (Seg n) & S1[x,y] ) ) or ( i2 = 1 & i2 = n & ex y being object st
( y in bool (Seg n) & S1[x,y] ) ) )per cases
( ( 1 < i2 & i2 < n ) or ( i2 = 1 & i2 < n ) or ( 1 < i2 & i2 = n ) or ( i2 = 1 & i2 = n ) )
by A3, XXREAL_0:1;
case A4:
( 1
< i2 &
i2 < n )
;
ex y being object st
( y in bool (Seg n) & S1[x,y] )
i2 <= i2 + 1
by NAT_1:12;
then A5:
1
< i2 + 1
by A4, XXREAL_0:2;
i2 + 1
<= n
by A4, NAT_1:13;
then A6:
i2 + 1
in Seg n
by A5;
set y0 =
{i2,(i2 -' 1),(i2 + 1)};
i2 - 1
> 0
by A4, XREAL_1:50;
then
i2 -' 1
> 0
by XREAL_0:def 2;
then A7:
i2 -' 1
>= 0 + 1
by NAT_1:13;
i2 -' 1
<= i2
by NAT_D:35;
then
i2 -' 1
< n
by A4, XXREAL_0:2;
then A8:
i2 -' 1
in Seg n
by A7;
A9:
{i2,(i2 -' 1),(i2 + 1)} c= Seg n
by A2, A8, A6, ENUMSET1:def 1;
S1[
x,
{i2,(i2 -' 1),(i2 + 1)}]
by A4;
hence
ex
y being
object st
(
y in bool (Seg n) &
S1[
x,
y] )
by A9;
verum end; case A10:
(
i2 = 1 &
i2 < n )
;
ex y being object st
( y in bool (Seg n) & S1[x,y] )then
i2 + 1
<= n
by NAT_1:13;
then A11:
i2 + 1
in Seg n
by A10;
set y0 =
{i2,n,(i2 + 1)};
A12:
n in Seg n
by A10;
A13:
{i2,n,(i2 + 1)} c= Seg n
by A2, A12, A11, ENUMSET1:def 1;
S1[
x,
{i2,n,(i2 + 1)}]
by A10;
hence
ex
y being
object st
(
y in bool (Seg n) &
S1[
x,
y] )
by A13;
verum end; case A14:
( 1
< i2 &
i2 = n )
;
ex y being object st
( y in bool (Seg n) & S1[x,y] )then
i2 - 1
> 0
by XREAL_1:50;
then
i2 -' 1
> 0
by XREAL_0:def 2;
then A15:
i2 -' 1
>= 0 + 1
by NAT_1:13;
set y0 =
{i2,(i2 -' 1),1};
A16:
1
in Seg n
by A14;
i2 -' 1
<= n
by A14, NAT_D:35;
then A17:
i2 -' 1
in Seg n
by A15;
A18:
{i2,(i2 -' 1),1} c= Seg n
by A2, A17, A16, ENUMSET1:def 1;
S1[
x,
{i2,(i2 -' 1),1}]
by A14;
hence
ex
y being
object st
(
y in bool (Seg n) &
S1[
x,
y] )
by A18;
verum end;
hence
ex
y being
object st
(
y in bool (Seg n) &
S1[
x,
y] )
;
verum
end;
consider f2 being Function of (Seg n),(bool (Seg n)) such that
A21:
for x3 being object st x3 in Seg n holds
S1[x3,f2 . x3]
from FUNCT_2:sch 1(A1);
consider R being Relation of (Seg n) such that
A22:
for i being set st i in Seg n holds
Im (R,i) = f2 . i
by FUNCT_2:93;
take
R
; for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) )
let i be Element of NAT ; ( i in Seg n implies ( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) ) )
assume A23:
i in Seg n
; ( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) )
then
Im (R,i) = f2 . i
by A22;
hence
( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) )
by A21, A23; verum