let n, m be Element of NAT ; for S being set
for Y being Subset of S
for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
let S be set ; for Y being Subset of S
for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
let Y be Subset of S; for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) holds
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
let F be Matrix of n,m,(bool S); ( ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y ) ) implies for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y )
assume that
A1:
ex i, j being Element of NAT st
( i in Seg n & j in Seg m & F * (i,j) c= Y )
and
A2:
for i1, j1, i2, j2 being Element of NAT st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds
( F * (i1,j1) c= Y iff F * (i2,j2) c= Y )
; for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
consider i1, j1 being Element of NAT such that
A3:
i1 in Seg n
and
A4:
j1 in Seg m
and
A5:
F * (i1,j1) c= Y
by A1;
A6:
j1 <= m
by A4, FINSEQ_1:1;
1 <= i1
by A3, FINSEQ_1:1;
then
i1 - 1 >= 1 - 1
by XREAL_1:9;
then A7:
i1 -' 1 = i1 - 1
by XREAL_0:def 2;
1 <= j1
by A4, FINSEQ_1:1;
then
j1 - 1 >= 1 - 1
by XREAL_1:9;
then A8:
j1 -' 1 = j1 - 1
by XREAL_0:def 2;
A9:
i1 <= n
by A3, FINSEQ_1:1;
thus
for i, j being Element of NAT st i in Seg n & j in Seg m holds
F * (i,j) c= Y
verumproof
let i2,
j2 be
Element of
NAT ;
( i2 in Seg n & j2 in Seg m implies F * (i2,j2) c= Y )
assume that A10:
i2 in Seg n
and A11:
j2 in Seg m
;
F * (i2,j2) c= Y
A12:
j2 <= m
by A11, FINSEQ_1:1;
1
<= i2
by A10, FINSEQ_1:1;
then
i2 - 1
>= 1
- 1
by XREAL_1:9;
then A13:
i2 -' 1
= i2 - 1
by XREAL_0:def 2;
1
<= j2
by A11, FINSEQ_1:1;
then
j2 - 1
>= 1
- 1
by XREAL_1:9;
then A14:
j2 -' 1
= j2 - 1
by XREAL_0:def 2;
A15:
i2 <= n
by A10, FINSEQ_1:1;
now ( ( ( n = 0 or m = 0 ) & contradiction ) or ( n <> 0 & m <> 0 & F * (i2,j2) c= Y ) )per cases
( n = 0 or m = 0 or ( n <> 0 & m <> 0 ) )
;
case
(
n = 0 or
m = 0 )
;
contradictionhence
contradiction
by A3, A4;
verum end; case A16:
(
n <> 0 &
m <> 0 )
;
F * (i2,j2) c= Ythen
m >= 0 + 1
by NAT_1:13;
then
m - 1
>= 0
by XREAL_1:19;
then A17:
m -' 1
= m - 1
by XREAL_0:def 2;
then A18:
(
j1 -' 1
<= m -' 1 &
j2 -' 1
<= m -' 1 )
by A6, A8, A12, A14, XREAL_1:9;
n >= 0 + 1
by A16, NAT_1:13;
then
n - 1
>= 0
by XREAL_1:19;
then A19:
n -' 1
= n - 1
by XREAL_0:def 2;
then
(
i1 -' 1
<= n -' 1 &
i2 -' 1
<= n -' 1 )
by A9, A7, A15, A13, XREAL_1:9;
then consider fs1,
fs2 being
FinSequence of
NAT such that A20:
for
i,
k1,
k2 being
Element of
NAT st
i in dom fs1 &
k1 = fs1 . i &
k2 = fs2 . i holds
(
k1 <= n -' 1 &
k2 <= m -' 1 )
and A21:
fs1 . 1
= i1 -' 1
and A22:
fs1 . (len fs1) = i2 -' 1
and A23:
fs2 . 1
= j1 -' 1
and A24:
fs2 . (len fs2) = j2 -' 1
and A25:
len fs1 = len fs2
and A26:
len fs1 = (((((i1 -' 1) -' (i2 -' 1)) + ((i2 -' 1) -' (i1 -' 1))) + ((j1 -' 1) -' (j2 -' 1))) + ((j2 -' 1) -' (j1 -' 1))) + 1
and A27:
for
i being
Element of
NAT st 1
<= i &
i < len fs1 holds
fs1 /. i,
fs2 /. i,
fs1 /. (i + 1),
fs2 /. (i + 1) are_adjacent
by A18, Th7;
deffunc H1(
Nat)
-> Element of
NAT =
(fs1 /. $1) + 1;
ex
p being
FinSequence of
NAT st
(
len p = len fs1 & ( for
j being
Nat st
j in dom p holds
p . j = H1(
j) ) )
from FINSEQ_2:sch 1();
then consider p1 being
FinSequence of
NAT such that A28:
len p1 = len fs1
and A29:
for
k being
Nat st
k in dom p1 holds
p1 . k = (fs1 /. k) + 1
;
deffunc H2(
Nat)
-> Element of
NAT =
(fs2 /. $1) + 1;
ex
p being
FinSequence of
NAT st
(
len p = len fs2 & ( for
k being
Nat st
k in dom p holds
p . k = H2(
k) ) )
from FINSEQ_2:sch 1();
then consider p2 being
FinSequence of
NAT such that A30:
len p2 = len fs2
and A31:
for
k being
Nat st
k in dom p2 holds
p2 . k = (fs2 /. k) + 1
;
A32:
dom p2 = Seg (len fs2)
by A30, FINSEQ_1:def 3;
defpred S1[
Nat]
means ( $1
+ 1
<= len p1 implies
F * (
(p1 /. ($1 + 1)),
(p2 /. ($1 + 1)))
c= Y );
A33:
dom p1 = Seg (len fs1)
by A28, FINSEQ_1:def 3;
A34:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
A35:
1
<= k + 1
by NAT_1:12;
assume A36:
(
k + 1
<= len p1 implies
F * (
(p1 /. (k + 1)),
(p2 /. (k + 1)))
c= Y )
;
S1[k + 1]
now ( ( k + 1 <= len p1 & S1[k + 1] ) or ( k + 1 > len p1 & S1[k + 1] ) )per cases
( k + 1 <= len p1 or k + 1 > len p1 )
;
case A37:
k + 1
<= len p1
;
S1[k + 1]now ( ( (k + 1) + 1 <= len p1 & S1[k + 1] ) or ( (k + 1) + 1 > len p1 & S1[k + 1] ) )per cases
( (k + 1) + 1 <= len p1 or (k + 1) + 1 > len p1 )
;
case A38:
(k + 1) + 1
<= len p1
;
S1[k + 1]set lp11 =
fs1 /. ((k + 1) + 1);
set lp21 =
fs2 /. ((k + 1) + 1);
1
<= (k + 1) + 1
by NAT_1:12;
then A39:
(k + 1) + 1
in Seg (len p1)
by A38, FINSEQ_1:1;
then
(k + 1) + 1
in dom fs2
by A25, A28, FINSEQ_1:def 3;
then A40:
fs2 /. ((k + 1) + 1) = fs2 . ((k + 1) + 1)
by PARTFUN1:def 6;
A41:
(k + 1) + 1
in dom fs1
by A28, A39, FINSEQ_1:def 3;
then A42:
fs1 /. ((k + 1) + 1) = fs1 . ((k + 1) + 1)
by PARTFUN1:def 6;
then
fs1 /. ((k + 1) + 1) <= n - 1
by A19, A20, A41, A40;
then A43:
(fs1 /. ((k + 1) + 1)) + 1
<= (n - 1) + 1
by XREAL_1:6;
(k + 1) + 1
in dom p2
by A25, A28, A30, A39, FINSEQ_1:def 3;
then
p2 . ((k + 1) + 1) = p2 /. ((k + 1) + 1)
by PARTFUN1:def 6;
then A44:
p2 /. ((k + 1) + 1) = (fs2 /. ((k + 1) + 1)) + 1
by A25, A28, A31, A32, A39;
fs2 /. ((k + 1) + 1) <= m -' 1
by A20, A41, A42, A40;
then A45:
(fs2 /. ((k + 1) + 1)) + 1
<= (m - 1) + 1
by A17, XREAL_1:6;
1
<= 1
+ (fs2 /. ((k + 1) + 1))
by NAT_1:11;
then A46:
p2 /. ((k + 1) + 1) in Seg m
by A44, A45, FINSEQ_1:1;
(k + 1) + 1
in dom p1
by A39, FINSEQ_1:def 3;
then A47:
p1 /. ((k + 1) + 1) =
p1 . ((k + 1) + 1)
by PARTFUN1:def 6
.=
(fs1 /. ((k + 1) + 1)) + 1
by A28, A29, A33, A39
;
set lp1 =
fs1 /. (k + 1);
set lp2 =
fs2 /. (k + 1);
A48:
k + 1
< len p1
by A38, NAT_1:13;
then A49:
k + 1
in Seg (len p1)
by A35, FINSEQ_1:1;
then
k + 1
in dom fs2
by A25, A28, FINSEQ_1:def 3;
then A50:
fs2 /. (k + 1) = fs2 . (k + 1)
by PARTFUN1:def 6;
k + 1
in dom p1
by A49, FINSEQ_1:def 3;
then A51:
p1 /. (k + 1) =
p1 . (k + 1)
by PARTFUN1:def 6
.=
(fs1 /. (k + 1)) + 1
by A28, A29, A33, A49
;
A52:
k + 1
in dom fs1
by A28, A49, FINSEQ_1:def 3;
then A53:
fs1 /. (k + 1) = fs1 . (k + 1)
by PARTFUN1:def 6;
then
fs1 /. (k + 1) <= n - 1
by A19, A20, A52, A50;
then A54:
(fs1 /. (k + 1)) + 1
<= (n - 1) + 1
by XREAL_1:6;
1
<= 1
+ (fs1 /. (k + 1))
by NAT_1:11;
then A55:
p1 /. (k + 1) in Seg n
by A51, A54, FINSEQ_1:1;
k + 1
in dom p2
by A25, A28, A30, A49, FINSEQ_1:def 3;
then A56:
p2 /. (k + 1) =
p2 . (k + 1)
by PARTFUN1:def 6
.=
(fs2 /. (k + 1)) + 1
by A25, A28, A31, A32, A49
;
fs2 /. (k + 1) <= m -' 1
by A20, A52, A53, A50;
then A57:
(fs2 /. (k + 1)) + 1
<= (m - 1) + 1
by A17, XREAL_1:6;
1
<= 1
+ (fs2 /. (k + 1))
by NAT_1:11;
then A58:
p2 /. (k + 1) in Seg m
by A56, A57, FINSEQ_1:1;
1
<= 1
+ (fs1 /. ((k + 1) + 1))
by NAT_1:11;
then A59:
p1 /. ((k + 1) + 1) in Seg n
by A47, A43, FINSEQ_1:1;
(k + 1) + 1
in dom p2
by A25, A28, A30, A39, FINSEQ_1:def 3;
then p2 /. ((k + 1) + 1) =
p2 . ((k + 1) + 1)
by PARTFUN1:def 6
.=
(fs2 /. ((k + 1) + 1)) + 1
by A25, A28, A31, A32, A39
;
then
p1 /. (k + 1),
p2 /. (k + 1),
p1 /. ((k + 1) + 1),
p2 /. ((k + 1) + 1) are_adjacent
by A27, A28, A35, A48, A51, A56, A47, Th3;
hence
S1[
k + 1]
by A2, A36, A37, A55, A58, A59, A46;
verum end; hence
S1[
k + 1]
;
verum
hence
S1[
k + 1]
;
verum
end; A60:
1
<= len fs1
by A26, NAT_1:11;
then A61:
1
in Seg (len fs1)
by FINSEQ_1:1;
then
1
in dom fs2
by A25, FINSEQ_1:def 3;
then A62:
fs2 /. 1
= j1 -' 1
by A23, PARTFUN1:def 6;
1
in dom p2
by A25, A30, A61, FINSEQ_1:def 3;
then A63:
p2 /. 1 =
p2 . 1
by PARTFUN1:def 6
.=
(j1 -' 1) + 1
by A25, A31, A32, A61, A62
.=
j1
by A8
;
1
in dom fs1
by A61, FINSEQ_1:def 3;
then A64:
fs1 /. 1
= i1 -' 1
by A21, PARTFUN1:def 6;
1
in dom p1
by A28, A61, FINSEQ_1:def 3;
then p1 /. 1 =
p1 . 1
by PARTFUN1:def 6
.=
(i1 -' 1) + 1
by A29, A33, A61, A64
.=
i1
by A7
;
then A65:
S1[
0 ]
by A5, A63;
A66:
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(A65, A34);
1
- 1
<= (len fs1) - 1
by A60, XREAL_1:9;
then
(len fs1) -' 1
= (len fs1) - 1
by XREAL_0:def 2;
then A67:
((len fs1) -' 1) + 1
= len fs1
;
A68:
len fs1 in Seg (len fs1)
by A60, FINSEQ_1:1;
then
len fs1 in dom fs2
by A25, FINSEQ_1:def 3;
then A69:
fs2 /. (len fs1) = j2 -' 1
by A24, A25, PARTFUN1:def 6;
len fs1 in dom p1
by A28, A68, FINSEQ_1:def 3;
then A70:
p1 /. (len fs1) =
p1 . (len fs1)
by PARTFUN1:def 6
.=
(fs1 /. (len fs1)) + 1
by A29, A33, A68
;
len fs1 in dom fs1
by A68, FINSEQ_1:def 3;
then A71:
fs1 /. (len fs1) = i2 -' 1
by A22, PARTFUN1:def 6;
len fs1 in dom p2
by A25, A30, A68, FINSEQ_1:def 3;
then p2 /. (len fs1) =
p2 . (len fs1)
by PARTFUN1:def 6
.=
(fs2 /. (len fs1)) + 1
by A25, A31, A32, A68
;
hence
F * (
i2,
j2)
c= Y
by A13, A14, A28, A66, A67, A70, A71, A69;
verum end;
hence
F * (
i2,
j2)
c= Y
;
verum
end;