let n, m be Element of NAT ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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 :: thesis: verum

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 ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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 :: thesis: verum

proof

let i2, j2 be Element of NAT ; :: thesis: ( 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 ; :: thesis: 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;

end;assume that

A10: i2 in Seg n and

A11: j2 in Seg m ; :: thesis: 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 :: thesis: ( ( ( n = 0 or m = 0 ) & contradiction ) or ( n <> 0 & m <> 0 & F * (i2,j2) c= Y ) )end;

hence
F * (i2,j2) c= Y
; :: thesis: verumper cases
( n = 0 or m = 0 or ( n <> 0 & m <> 0 ) )
;

end;

case A16:
( n <> 0 & m <> 0 )
; :: thesis: F * (i2,j2) c= Y

then
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 H_{1}( 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 = H_{1}(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 H_{2}( 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 = H_{2}(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 S_{1}[ 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 S_{1}[k] holds

S_{1}[k + 1]

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: S_{1}[ 0 ]
by A5, A63;

A66: for i being Nat holds S_{1}[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; :: thesis: verum

end;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 H

ex p being FinSequence of NAT st

( len p = len fs1 & ( for j being Nat st j in dom p holds

p . j = H

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 H

ex p being FinSequence of NAT st

( len p = len fs2 & ( for k being Nat st k in dom p holds

p . k = H

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 S

A33: dom p1 = Seg (len fs1) by A28, FINSEQ_1:def 3;

A34: for k being Nat st S

S

proof

A60:
1 <= len fs1
by A26, NAT_1:11;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[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 ) ; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;A35: 1 <= k + 1 by NAT_1:12;

assume A36: ( k + 1 <= len p1 implies F * ((p1 /. (k + 1)),(p2 /. (k + 1))) c= Y ) ; :: thesis: S

now :: thesis: ( ( k + 1 <= len p1 & S_{1}[k + 1] ) or ( k + 1 > len p1 & S_{1}[k + 1] ) )end;

hence
Sper cases
( k + 1 <= len p1 or k + 1 > len p1 )
;

end;

case A37:
k + 1 <= len p1
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;

now :: thesis: ( ( (k + 1) + 1 <= len p1 & S_{1}[k + 1] ) or ( (k + 1) + 1 > len p1 & S_{1}[k + 1] ) )end;

hence
Sper cases
( (k + 1) + 1 <= len p1 or (k + 1) + 1 > len p1 )
;

end;

case A38:
(k + 1) + 1 <= len p1
; :: thesis: S_{1}[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 S_{1}[k + 1]
by A2, A36, A37, A55, A58, A59, A46; :: thesis: verum

end;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 S

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: S

A66: for i being Nat holds S

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; :: thesis: verum