let G be Graph; :: thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
let vs be FinSequence of the carrier of G; :: thesis: for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
let c be oriented Chain of G; :: thesis: ( not c is Simple & vs is_oriented_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) )
assume A1:
( not c is Simple & vs is_oriented_vertex_seq_of c )
; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
then consider n, m being Element of NAT such that
A2:
( 1 <= n & n < m & m <= len vs & vs . n = vs . m & ( n <> 1 or m <> len vs ) )
by Def7;
A3:
len vs = (len c) + 1
by A1, Def5;
A4:
m - n > n - n
by A2, XREAL_1:11;
reconsider n1 = n -' 1 as Element of NAT ;
A5:
1 - 1 <= n - 1
by A2, XREAL_1:11;
then A6:
n - 1 = n -' 1
by XREAL_0:def 2;
A7: n1 + 1 =
(n - 1) + 1
by A5, XREAL_0:def 2
.=
n
;
per cases
( ( n <> 1 & m <> len vs ) or ( n = 1 & m <> len vs ) or ( n <> 1 & m = len vs ) )
by A2;
suppose A8:
(
n <> 1 &
m <> len vs )
;
:: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )then
1
< n
by A2, XXREAL_0:1;
then
1
+ 1
<= n
by NAT_1:13;
then A9:
(1 + 1) - 1
<= n - 1
by XREAL_1:11;
n < len vs
by A2, XXREAL_0:2;
then A10:
n - 1
< ((len c) + 1) - 1
by A3, XREAL_1:11;
A11:
1
<= n1 + 1
by NAT_1:12;
A12:
m < len vs
by A2, A8, XXREAL_0:1;
then A13:
m <= len c
by A3, NAT_1:13;
A14:
( 1
<= m &
m <= len c &
len c <= len c )
by A2, A3, A12, NAT_1:13, XXREAL_0:2;
reconsider c1 = 1,
n1 -cut c as
oriented Chain of
G by A6, A9, A10, Th13;
reconsider c2 =
m,
(len c) -cut c as
oriented Chain of
G by A14, Th13;
set pp = 1,
n -cut vs;
set p2 =
m,
((len c) + 1) -cut vs;
set p2' =
(m + 1),
((len c) + 1) -cut vs;
reconsider pp = 1,
n -cut vs as
FinSequence of the
carrier of
G ;
reconsider p2 =
m,
((len c) + 1) -cut vs as
FinSequence of the
carrier of
G ;
A15:
( 1
<= n &
n <= len vs )
by A2, XXREAL_0:2;
A16:
( 1
<= m &
m <= (len c) + 1 &
(len c) + 1
<= len vs )
by A1, A2, Def5, XXREAL_0:2;
A17:
pp is_oriented_vertex_seq_of c1
by A1, A7, A9, A10, Th14;
A18:
p2 is_oriented_vertex_seq_of c2
by A1, A14, Th14;
A19:
len pp = (len c1) + 1
by A17, Def5;
A20:
len p2 = (len c2) + 1
by A18, Def5;
1
- 1
<= m - 1
by A14, XREAL_1:11;
then
m -' 1
= m - 1
by XREAL_0:def 2;
then reconsider m1 =
m - 1 as
Element of
NAT ;
A21:
m = m1 + 1
;
A22:
(len c2) + m = (len c) + 1
by A14, GRAPH_2:def 1;
A23:
m - m <= (len c) - m
by A13, XREAL_1:11;
then
(len c2) -' 1
= (len c2) - 1
by A22, XREAL_0:def 2;
then reconsider lc21 =
(len c2) - 1 as
Element of
NAT ;
A24:
m + lc21 = m1 + (len c2)
;
(
0 + 1
= 1 &
0 < len p2 )
by A20;
then A25:
(
0 + 1
= 1 &
0 <= 1 & 1
<= len p2 )
by NAT_1:13;
A26:
p2 =
(0 + 1),
(len p2) -cut p2
by GRAPH_2:7
.=
((0 + 1),1 -cut p2) ^ ((1 + 1),(len p2) -cut p2)
by A25, GRAPH_2:8
;
m1 <= m
by A21, NAT_1:12;
then A27:
p2 = ((m1 + 1),m -cut vs) ^ ((m + 1),((len c) + 1) -cut vs)
by A2, A3, GRAPH_2:8;
1,1
-cut p2 =
<*(p2 . (0 + 1))*>
by A25, GRAPH_2:6
.=
<*(vs . (m + 0 ))*>
by A16, A20, GRAPH_2:def 1
.=
m,
m -cut vs
by A2, A14, GRAPH_2:6
;
then A28:
(m + 1),
((len c) + 1) -cut vs = 2,
(len p2) -cut p2
by A26, A27, FINSEQ_1:46;
set domfc =
{ k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ;
deffunc H1(
set )
-> set =
c . $1;
consider fc being
Function such that A29:
dom fc = { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) }
and A30:
for
x being
set st
x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } holds
fc . x = H1(
x)
from FUNCT_1:sch 3();
{ k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } c= Seg (len c)
then reconsider fc =
fc as
FinSubsequence by A29, FINSEQ_1:def 12;
fc c= c
proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in fc or p in c )
assume A32:
p in fc
;
:: thesis: p in c
then consider x,
y being
set such that A33:
[x,y] = p
by RELAT_1:def 1;
A34:
(
x in dom fc &
y = fc . x )
by A32, A33, FUNCT_1:8;
then consider kk being
Element of
NAT such that A35:
(
x = kk & ( ( 1
<= kk &
kk <= n1 ) or (
m <= kk &
kk <= len c ) ) )
by A29;
( 1
<= kk &
kk <= len c )
by A6, A10, A14, A35, XXREAL_0:2;
then A36:
x in dom c
by A35, FINSEQ_3:27;
y = c . kk
by A29, A30, A34, A35;
hence
p in c
by A33, A35, A36, FUNCT_1:8;
:: thesis: verum
end; then reconsider fc =
fc as
Subset of
c ;
take
fc
;
:: thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )set domfvs =
{ k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ;
deffunc H2(
set )
-> set =
vs . $1;
consider fvs being
Function such that A37:
dom fvs = { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) }
and A38:
for
x being
set st
x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } holds
fvs . x = H2(
x)
from FUNCT_1:sch 3();
{ k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } c= Seg (len vs)
then reconsider fvs =
fvs as
FinSubsequence by A37, FINSEQ_1:def 12;
fvs c= vs
proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in fvs or p in vs )
assume A40:
p in fvs
;
:: thesis: p in vs
then consider x,
y being
set such that A41:
[x,y] = p
by RELAT_1:def 1;
A42:
(
x in dom fvs &
y = fvs . x )
by A40, A41, FUNCT_1:8;
then consider kk being
Element of
NAT such that A43:
(
x = kk & ( ( 1
<= kk &
kk <= n ) or (
m + 1
<= kk &
kk <= len vs ) ) )
by A37;
1
<= m + 1
by NAT_1:12;
then
( 1
<= kk &
kk <= len vs )
by A15, A43, XXREAL_0:2;
then A44:
x in dom vs
by A43, FINSEQ_3:27;
y = vs . kk
by A37, A38, A42, A43;
hence
p in vs
by A41, A43, A44, FUNCT_1:8;
:: thesis: verum
end; then reconsider fvs =
fvs as
Subset of
vs ;
take
fvs
;
:: thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )A45:
(
p2 . 1
= vs . m &
pp . (len pp) = vs . n )
by A15, A16, GRAPH_2:12;
then reconsider c' =
c1 ^ c2 as
oriented Chain of
G by A2, A17, A18, Th15;
take
c'
;
:: thesis: ex vs1 being FinSequence of the carrier of G st
( len c' < len c & vs1 is_oriented_vertex_seq_of c' & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c' & Seq fvs = vs1 )take p1 =
pp ^' p2;
:: thesis: ( len c' < len c & p1 is_oriented_vertex_seq_of c' & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )A46:
p1 = pp ^ ((m + 1),((len c) + 1) -cut vs)
by A28, GRAPH_2:def 2;
A47:
(len c1) + 1
= n1 + 1
by A6, A10, A11, Lm2;
- (- (m - n)) = m - n
;
then A48:
- (m - n) < 0
by A4;
len c' =
(n - 1) + (((len c) - m) + 1)
by A6, A22, A47, FINSEQ_1:35
.=
(len c) + (n + (- m))
;
hence A49:
len c' < len c
by A48, XREAL_1:32;
:: thesis: ( p1 is_oriented_vertex_seq_of c' & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )thus
p1 is_oriented_vertex_seq_of c'
by A2, A17, A18, A45, Th16;
:: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )then
len p1 = (len c') + 1
by Def5;
hence
len p1 < len vs
by A3, A49, XREAL_1:8;
:: thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )
1
<= 1
+ (len c1)
by NAT_1:12;
then
1
<= len pp
by A17, Def5;
then
p1 . 1
= pp . 1
by GRAPH_2:14;
hence
vs . 1
= p1 . 1
by A15, GRAPH_2:12;
:: thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )A50:
p2 . (len p2) = vs . ((len c) + 1)
by A16, GRAPH_2:12;
m - m <= (len c) - m
by A14, XREAL_1:11;
then
0 + 1
<= ((len c) - m) + 1
by XREAL_1:8;
then
1
< len p2
by A20, A22, NAT_1:13;
hence
vs . (len vs) = p1 . (len p1)
by A3, A50, GRAPH_2:16;
:: thesis: ( Seq fc = c' & Seq fvs = p1 )set DL =
{ kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } ;
set DR =
{ kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ;
then A55:
{ k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) }
by TARSKI:2;
A56:
(
{ kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } c= Seg (len c) &
{ kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } c= Seg (len c) )
then reconsider DL =
{ kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } as
finite set by FINSET_1:13;
reconsider DR =
{ kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } as
finite set by A56, FINSET_1:13;
then A61:
Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR)
by A56, FINSEQ_3:48;
m + lc21 = len c
by A22;
then A62:
card DR =
((len c2) + (- 1)) + 1
by GRAPH_2:4
.=
len c2
;
A63:
(
len (Sgm DL) = card DL &
len (Sgm DR) = card DR )
by A56, FINSEQ_3:44;
DL = Seg n1
by FINSEQ_1:def 1;
then A64:
Sgm DL = idseq n1
by FINSEQ_3:54;
then A65:
dom (Sgm DL) = Seg n1
by RELAT_1:71;
rng (Sgm DL) = DL
by A56, FINSEQ_1:def 13;
then A66:
rng (Sgm DL) c= dom fc
by A29, A55, XBOOLE_1:7;
rng (Sgm DR) = DR
by A56, FINSEQ_1:def 13;
then A67:
rng (Sgm DR) c= dom fc
by A29, A55, XBOOLE_1:7;
set SL =
Sgm DL;
set SR =
Sgm DR;
now let p be
set ;
:: thesis: ( ( p in c1 implies p in fc * (Sgm DL) ) & ( p in fc * (Sgm DL) implies p in c1 ) )hereby :: thesis: ( p in fc * (Sgm DL) implies p in c1 )
assume A68:
p in c1
;
:: thesis: p in fc * (Sgm DL)then consider x,
y being
set such that A69:
p = [x,y]
by RELAT_1:def 1;
A70:
(
x in dom c1 &
y = c1 . x )
by A68, A69, FUNCT_1:8;
then reconsider k =
x as
Element of
NAT ;
A71:
( 1
<= k &
k <= len c1 )
by A70, FINSEQ_3:27;
then A72:
x in dom (Sgm DL)
by A47, A65, FINSEQ_1:3;
then A73:
k = (Sgm DL) . k
by A64, A65, FUNCT_1:35;
A74:
k in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) }
by A47, A71;
then A75:
x in dom (fc * (Sgm DL))
by A29, A72, A73, FUNCT_1:21;
0 + 1
<= k
by A70, FINSEQ_3:27;
then consider i being
Element of
NAT such that A76:
(
0 <= i &
i < n1 &
k = i + 1 )
by A47, A71, GRAPH_2:1;
(fc * (Sgm DL)) . x =
fc . k
by A73, A75, FUNCT_1:22
.=
c . (1 + i)
by A29, A74, A76, GRFUNC_1:8
.=
y
by A6, A10, A11, A47, A70, A76, Lm2
;
hence
p in fc * (Sgm DL)
by A69, A75, FUNCT_1:8;
:: thesis: verum
end; assume A77:
p in fc * (Sgm DL)
;
:: thesis: p in c1then consider x,
y being
set such that A78:
p = [x,y]
by RELAT_1:def 1;
A79:
(
x in dom (fc * (Sgm DL)) &
y = (fc * (Sgm DL)) . x )
by A77, A78, FUNCT_1:8;
then A80:
(fc * (Sgm DL)) . x = fc . ((Sgm DL) . x)
by FUNCT_1:22;
A81:
(
x in dom (Sgm DL) &
(Sgm DL) . x in dom fc )
by A79, FUNCT_1:21;
then
x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) }
by A65, FINSEQ_1:def 1;
then consider k being
Element of
NAT such that A82:
(
k = x & 1
<= k &
k <= n1 )
;
A83:
k in dom fc
by A29, A82;
A84:
k = (Sgm DL) . k
by A64, A65, A81, A82, FUNCT_1:35;
A85:
k in dom c1
by A47, A82, FINSEQ_3:27;
0 + 1
<= k
by A82;
then consider i being
Element of
NAT such that A86:
(
0 <= i &
i < n1 &
k = i + 1 )
by A82, GRAPH_2:1;
c1 . k =
c . k
by A6, A10, A11, A47, A86, Lm2
.=
y
by A79, A80, A82, A83, A84, GRFUNC_1:8
;
hence
p in c1
by A78, A82, A85, FUNCT_1:8;
:: thesis: verum end; then A87:
c1 = fc * (Sgm DL)
by TARSKI:2;
now let p be
set ;
:: thesis: ( ( p in c2 implies p in fc * (Sgm DR) ) & ( p in fc * (Sgm DR) implies p in c2 ) )hereby :: thesis: ( p in fc * (Sgm DR) implies p in c2 )
assume A88:
p in c2
;
:: thesis: p in fc * (Sgm DR)then consider x,
y being
set such that A89:
p = [x,y]
by RELAT_1:def 1;
A90:
(
x in dom c2 &
y = c2 . x )
by A88, A89, FUNCT_1:8;
then reconsider k =
x as
Element of
NAT ;
A91:
( 1
<= k &
k <= len c2 )
by A90, FINSEQ_3:27;
A92:
x in dom (Sgm DR)
by A62, A63, A90, FINSEQ_3:31;
A93:
m1 + k = (Sgm DR) . k
by A21, A22, A24, A91, GRAPH_2:5;
A94:
(Sgm DR) . k in rng (Sgm DR)
by A92, FUNCT_1:def 5;
then A95:
x in dom (fc * (Sgm DR))
by A67, A92, FUNCT_1:21;
0 + 1
<= k
by A90, FINSEQ_3:27;
then consider i being
Element of
NAT such that A96:
(
0 <= i &
i < len c2 &
k = i + 1 )
by A91, GRAPH_2:1;
(fc * (Sgm DR)) . x =
fc . (m1 + k)
by A93, A95, FUNCT_1:22
.=
c . (m + i)
by A67, A93, A94, A96, GRFUNC_1:8
.=
y
by A14, A90, A96, GRAPH_2:def 1
;
hence
p in fc * (Sgm DR)
by A89, A95, FUNCT_1:8;
:: thesis: verum
end; assume A97:
p in fc * (Sgm DR)
;
:: thesis: p in c2then consider x,
y being
set such that A98:
p = [x,y]
by RELAT_1:def 1;
A99:
(
x in dom (fc * (Sgm DR)) &
y = (fc * (Sgm DR)) . x )
by A97, A98, FUNCT_1:8;
then A100:
(
x in dom (Sgm DR) &
(Sgm DR) . x in dom fc )
by FUNCT_1:21;
then reconsider k =
x as
Element of
NAT ;
A101:
k in dom c2
by A62, A63, A100, FINSEQ_3:31;
A102:
( 1
<= k &
k <= len c2 )
by A62, A63, A100, FINSEQ_3:27;
then A103:
m1 + k = (Sgm DR) . k
by A21, A22, A24, GRAPH_2:5;
0 + 1
<= k
by A100, FINSEQ_3:27;
then consider i being
Element of
NAT such that A104:
(
0 <= i &
i < len c2 &
k = i + 1 )
by A102, GRAPH_2:1;
c2 . k =
c . ((m1 + 1) + i)
by A14, A104, GRAPH_2:def 1
.=
fc . ((Sgm DR) . k)
by A100, A103, A104, GRFUNC_1:8
.=
y
by A99, A100, FUNCT_1:23
;
hence
p in c2
by A98, A101, FUNCT_1:8;
:: thesis: verum end; then A105:
c2 = fc * (Sgm DR)
by TARSKI:2;
Seq fc = fc * ((Sgm DL) ^ (Sgm DR))
by A29, A55, A61, FINSEQ_1:def 14;
hence
Seq fc = c'
by A66, A67, A87, A105, GRAPH_2:26;
:: thesis: Seq fvs = p1set DL =
{ kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } ;
set DR =
{ kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ;
then A110:
{ k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) }
by TARSKI:2;
A111:
(
{ kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } c= Seg (len vs) &
{ kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } c= Seg (len vs) )
then reconsider DL =
{ kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } as
finite set by FINSET_1:13;
reconsider DR =
{ kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } as
finite set by A111, FINSET_1:13;
then A117:
Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR)
by A111, FINSEQ_3:48;
1
<= len p2
by A20, NAT_1:12;
then
1
- 1
<= (len p2) - 1
by XREAL_1:11;
then
(len p2) -' 1
= (len p2) - 1
by XREAL_0:def 2;
then reconsider lp21 =
(len p2) - 1 as
Element of
NAT ;
lp21 -' 1
= lp21 - 1
by A20, A22, A23, XREAL_0:def 2;
then reconsider lp22 =
lp21 - 1 as
Element of
NAT ;
A118:
(m + 1) + lp22 =
m + ((lp21 - 1) + 1)
.=
m + (((((len c) - m) + 1) + 1) - 1)
by A18, A22, Def5
.=
(len c) + 1
;
then A119:
card DR =
lp22 + 1
by A3, GRAPH_2:4
.=
lp21
;
A120:
( 1
<= m + 1 &
m + 1
<= ((len c) + 1) + 1 )
by A16, NAT_1:12, XREAL_1:8;
A121:
(len p2) + m =
((len c) + 1) + 1
by A16, GRAPH_2:def 1
.=
(len ((m + 1),((len c) + 1) -cut vs)) + (m + 1)
by A16, A120, Lm2
.=
((len ((m + 1),((len c) + 1) -cut vs)) + 1) + m
;
A122:
(
len (Sgm DL) = card DL &
len (Sgm DR) = card DR )
by A111, FINSEQ_3:44;
DL = Seg n
by FINSEQ_1:def 1;
then A123:
Sgm DL = idseq n
by FINSEQ_3:54;
then A124:
dom (Sgm DL) = Seg n
by RELAT_1:71;
rng (Sgm DL) = DL
by A111, FINSEQ_1:def 13;
then A125:
rng (Sgm DL) c= dom fvs
by A37, A110, XBOOLE_1:7;
rng (Sgm DR) = DR
by A111, FINSEQ_1:def 13;
then A126:
rng (Sgm DR) c= dom fvs
by A37, A110, XBOOLE_1:7;
set SL =
Sgm DL;
set SR =
Sgm DR;
now let p be
set ;
:: thesis: ( ( p in pp implies p in fvs * (Sgm DL) ) & ( p in fvs * (Sgm DL) implies p in pp ) )hereby :: thesis: ( p in fvs * (Sgm DL) implies p in pp )
assume A127:
p in pp
;
:: thesis: p in fvs * (Sgm DL)then consider x,
y being
set such that A128:
p = [x,y]
by RELAT_1:def 1;
A129:
(
x in dom pp &
y = pp . x )
by A127, A128, FUNCT_1:8;
then reconsider k =
x as
Element of
NAT ;
A130:
( 1
<= k &
k <= len pp )
by A129, FINSEQ_3:27;
then A131:
x in dom (Sgm DL)
by A6, A19, A47, A124, FINSEQ_1:3;
then A132:
k = (Sgm DL) . k
by A123, A124, FUNCT_1:35;
A133:
k in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) }
by A6, A19, A47, A130;
then A134:
x in dom (fvs * (Sgm DL))
by A37, A131, A132, FUNCT_1:21;
0 + 1
<= k
by A129, FINSEQ_3:27;
then consider i being
Element of
NAT such that A135:
(
0 <= i &
i < n &
k = i + 1 )
by A6, A19, A47, A130, GRAPH_2:1;
(fvs * (Sgm DL)) . x =
fvs . k
by A132, A134, FUNCT_1:22
.=
vs . (1 + i)
by A37, A133, A135, GRFUNC_1:8
.=
y
by A6, A15, A19, A47, A129, A135, GRAPH_2:def 1
;
hence
p in fvs * (Sgm DL)
by A128, A134, FUNCT_1:8;
:: thesis: verum
end; assume A136:
p in fvs * (Sgm DL)
;
:: thesis: p in ppthen consider x,
y being
set such that A137:
p = [x,y]
by RELAT_1:def 1;
A138:
(
x in dom (fvs * (Sgm DL)) &
y = (fvs * (Sgm DL)) . x )
by A136, A137, FUNCT_1:8;
then A139:
(fvs * (Sgm DL)) . x = fvs . ((Sgm DL) . x)
by FUNCT_1:22;
A140:
(
x in dom (Sgm DL) &
(Sgm DL) . x in dom fvs )
by A138, FUNCT_1:21;
then
x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) }
by A124, FINSEQ_1:def 1;
then consider k being
Element of
NAT such that A141:
(
k = x & 1
<= k &
k <= n )
;
A142:
k in dom fvs
by A37, A141;
A143:
k = (Sgm DL) . k
by A123, A124, A140, A141, FUNCT_1:35;
A144:
k in dom pp
by A6, A19, A47, A141, FINSEQ_3:27;
0 + 1
<= k
by A141;
then consider i being
Element of
NAT such that A145:
(
0 <= i &
i < n &
k = i + 1 )
by A141, GRAPH_2:1;
pp . k =
vs . k
by A6, A15, A19, A47, A145, GRAPH_2:def 1
.=
y
by A138, A139, A141, A142, A143, GRFUNC_1:8
;
hence
p in pp
by A137, A141, A144, FUNCT_1:8;
:: thesis: verum end; then A146:
pp = fvs * (Sgm DL)
by TARSKI:2;
A147:
(m + 1) + lp22 = m + lp21
;
A148:
( 1
<= m + 1 &
m + 1
<= ((len c) + 1) + 1 )
by A2, A3, NAT_1:12, XREAL_1:9;
now let p be
set ;
:: thesis: ( ( p in (m + 1),((len c) + 1) -cut vs implies p in fvs * (Sgm DR) ) & ( p in fvs * (Sgm DR) implies p in (m + 1),((len c) + 1) -cut vs ) )hereby :: thesis: ( p in fvs * (Sgm DR) implies p in (m + 1),((len c) + 1) -cut vs )
assume A149:
p in (m + 1),
((len c) + 1) -cut vs
;
:: thesis: p in fvs * (Sgm DR)then consider x,
y being
set such that A150:
p = [x,y]
by RELAT_1:def 1;
A151:
(
x in dom ((m + 1),((len c) + 1) -cut vs) &
y = ((m + 1),((len c) + 1) -cut vs) . x )
by A149, A150, FUNCT_1:8;
then reconsider k =
x as
Element of
NAT ;
A152:
( 1
<= k &
k <= len ((m + 1),((len c) + 1) -cut vs) )
by A151, FINSEQ_3:27;
A153:
x in dom (Sgm DR)
by A119, A121, A122, A151, FINSEQ_3:31;
A154:
m + k = (Sgm DR) . k
by A3, A118, A121, A147, A152, GRAPH_2:5;
A155:
(Sgm DR) . k in rng (Sgm DR)
by A153, FUNCT_1:def 5;
then A156:
x in dom (fvs * (Sgm DR))
by A126, A153, FUNCT_1:21;
0 + 1
<= k
by A151, FINSEQ_3:27;
then consider i being
Element of
NAT such that A157:
(
0 <= i &
i < len ((m + 1),((len c) + 1) -cut vs) &
k = i + 1 )
by A152, GRAPH_2:1;
(fvs * (Sgm DR)) . x =
fvs . (m + k)
by A154, A156, FUNCT_1:22
.=
vs . ((m + 1) + i)
by A126, A154, A155, A157, GRFUNC_1:8
.=
y
by A3, A148, A151, A157, Lm2
;
hence
p in fvs * (Sgm DR)
by A150, A156, FUNCT_1:8;
:: thesis: verum
end; assume A158:
p in fvs * (Sgm DR)
;
:: thesis: p in (m + 1),((len c) + 1) -cut vsthen consider x,
y being
set such that A159:
p = [x,y]
by RELAT_1:def 1;
A160:
(
x in dom (fvs * (Sgm DR)) &
y = (fvs * (Sgm DR)) . x )
by A158, A159, FUNCT_1:8;
then A161:
(
x in dom (Sgm DR) &
(Sgm DR) . x in dom fvs )
by FUNCT_1:21;
then reconsider k =
x as
Element of
NAT ;
A162:
k in dom ((m + 1),((len c) + 1) -cut vs)
by A119, A121, A122, A161, FINSEQ_3:31;
A163:
( 1
<= k &
k <= len ((m + 1),((len c) + 1) -cut vs) )
by A119, A121, A122, A161, FINSEQ_3:27;
then A164:
m + k = (Sgm DR) . k
by A3, A118, A121, A147, GRAPH_2:5;
0 + 1
<= k
by A161, FINSEQ_3:27;
then consider i being
Element of
NAT such that A165:
(
0 <= i &
i < len ((m + 1),((len c) + 1) -cut vs) &
k = i + 1 )
by A163, GRAPH_2:1;
((m + 1),((len c) + 1) -cut vs) . k =
vs . ((m + 1) + i)
by A3, A148, A165, Lm2
.=
fvs . ((Sgm DR) . k)
by A161, A164, A165, GRFUNC_1:8
.=
y
by A160, A161, FUNCT_1:23
;
hence
p in (m + 1),
((len c) + 1) -cut vs
by A159, A162, FUNCT_1:8;
:: thesis: verum end; then A166:
(m + 1),
((len c) + 1) -cut vs = fvs * (Sgm DR)
by TARSKI:2;
Seq fvs = fvs * ((Sgm DL) ^ (Sgm DR))
by A37, A110, A117, FINSEQ_1:def 14;
hence
Seq fvs = p1
by A46, A125, A126, A146, A166, GRAPH_2:26;
:: thesis: verum end; suppose A167:
(
n = 1 &
m <> len vs )
;
:: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )then A168:
m < len vs
by A2, XXREAL_0:1;
then A169:
m <= len c
by A3, NAT_1:13;
A170:
1
< m
by A2, XXREAL_0:2;
A171:
( 1
<= m &
m <= len c &
len c <= len c )
by A2, A3, A168, NAT_1:13, XXREAL_0:2;
reconsider c2 =
m,
(len c) -cut c as
oriented Chain of
G by A169, A170, Th13;
set p2 =
m,
((len c) + 1) -cut vs;
A172:
m,
((len c) + 1) -cut vs is_oriented_vertex_seq_of c2
by A1, A169, A170, Th14;
set domfc =
{ k where k is Element of NAT : ( m <= k & k <= len c ) } ;
deffunc H1(
set )
-> set =
c . $1;
consider fc being
Function such that A173:
dom fc = { k where k is Element of NAT : ( m <= k & k <= len c ) }
and A174:
for
x being
set st
x in { k where k is Element of NAT : ( m <= k & k <= len c ) } holds
fc . x = H1(
x)
from FUNCT_1:sch 3();
{ k where k is Element of NAT : ( m <= k & k <= len c ) } c= Seg (len c)
then reconsider fc =
fc as
FinSubsequence by A173, FINSEQ_1:def 12;
fc c= c
proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in fc or p in c )
assume A176:
p in fc
;
:: thesis: p in c
then consider x,
y being
set such that A177:
[x,y] = p
by RELAT_1:def 1;
A178:
(
x in dom fc &
y = fc . x )
by A176, A177, FUNCT_1:8;
then consider kk being
Element of
NAT such that A179:
(
x = kk &
m <= kk &
kk <= len c )
by A173;
( 1
<= kk &
kk <= len c )
by A170, A179, XXREAL_0:2;
then A180:
x in dom c
by A179, FINSEQ_3:27;
y = c . kk
by A173, A174, A178, A179;
hence
p in c
by A177, A179, A180, FUNCT_1:8;
:: thesis: verum
end; then reconsider fc =
fc as
Subset of
c ;
take
fc
;
:: thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )set domfvs =
{ k where k is Element of NAT : ( m <= k & k <= len vs ) } ;
deffunc H2(
set )
-> set =
vs . $1;
consider fvs being
Function such that A181:
dom fvs = { k where k is Element of NAT : ( m <= k & k <= len vs ) }
and A182:
for
x being
set st
x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } holds
fvs . x = H2(
x)
from FUNCT_1:sch 3();
{ k where k is Element of NAT : ( m <= k & k <= len vs ) } c= Seg (len vs)
then reconsider fvs =
fvs as
FinSubsequence by A181, FINSEQ_1:def 12;
fvs c= vs
proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in fvs or p in vs )
assume A184:
p in fvs
;
:: thesis: p in vs
then consider x,
y being
set such that A185:
[x,y] = p
by RELAT_1:def 1;
A186:
(
x in dom fvs &
y = fvs . x )
by A184, A185, FUNCT_1:8;
then consider kk being
Element of
NAT such that A187:
(
x = kk &
m <= kk &
kk <= len vs )
by A181;
( 1
<= kk &
kk <= len vs )
by A170, A187, XXREAL_0:2;
then A188:
x in dom vs
by A187, FINSEQ_3:27;
y = vs . kk
by A181, A182, A186, A187;
hence
p in vs
by A185, A187, A188, FUNCT_1:8;
:: thesis: verum
end; then reconsider fvs =
fvs as
Subset of
vs ;
take
fvs
;
:: thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )take c1 =
c2;
:: thesis: ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )take p1 =
m,
((len c) + 1) -cut vs;
:: thesis: ( len c1 < len c & p1 is_oriented_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )A189:
(len c2) + m = (len c) + 1
by A2, A3, A167, Lm2;
A190:
m - m <= (len c) - m
by A169, XREAL_1:11;
1
- 1
<= m - 1
by A170, XREAL_1:11;
then
m -' 1
= m - 1
by XREAL_0:def 2;
then reconsider m1 =
m - 1 as
Element of
NAT ;
A191:
m = m1 + 1
;
(len c2) -' 1
= (len c2) - 1
by A189, A190, XREAL_0:def 2;
then reconsider lc21 =
(len c2) - 1 as
Element of
NAT ;
A192:
m + lc21 = m1 + (len c2)
;
A193:
( 1
<= m &
m <= ((len c) + 1) + 1 &
(len c) + 1
<= len vs )
by A2, A3, A167, NAT_1:12;
then A194:
(len (m,((len c) + 1) -cut vs)) + m = ((len c) + 1) + 1
by Lm2;
then
len (m,((len c) + 1) -cut vs) = (((len c) - m) + 1) + 1
;
then A195:
1
<= len (m,((len c) + 1) -cut vs)
by A189, NAT_1:12;
A196:
len c2 = (len c) + ((- m) + 1)
by A189;
1
- 1
< m - 1
by A170, XREAL_1:11;
then
0 < - (- (m - 1))
;
then
- (m - 1) < 0
;
hence A197:
len c1 < len c
by A196, XREAL_1:32;
:: thesis: ( p1 is_oriented_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )thus
p1 is_oriented_vertex_seq_of c1
by A1, A171, Th14;
:: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )
len p1 = (len c1) + 1
by A172, Def5;
hence
len p1 < len vs
by A3, A197, XREAL_1:8;
:: thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )thus
vs . 1
= p1 . 1
by A2, A3, A167, GRAPH_2:12;
:: thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )thus
vs . (len vs) = p1 . (len p1)
by A2, A3, A167, GRAPH_2:12;
:: thesis: ( Seq fc = c1 & Seq fvs = p1 )A198:
{ k where k is Element of NAT : ( m <= k & k <= len c ) } c= Seg (len c)
then reconsider domfc =
{ k where k is Element of NAT : ( m <= k & k <= len c ) } as
finite set by FINSET_1:13;
(len c2) -' 1
= (len c2) - 1
by A189, A190, XREAL_0:def 2;
then reconsider lc21 =
(len c2) - 1 as
Element of
NAT ;
m + lc21 = len c
by A189;
then A200:
card domfc =
((len c2) + (- 1)) + 1
by GRAPH_2:4
.=
len c2
;
A201:
len (Sgm domfc) = card domfc
by A198, FINSEQ_3:44;
A202:
rng (Sgm domfc) c= dom fc
by A173, A198, FINSEQ_1:def 13;
set SR =
Sgm domfc;
now let p be
set ;
:: thesis: ( ( p in c2 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c2 ) )hereby :: thesis: ( p in fc * (Sgm domfc) implies p in c2 )
assume A203:
p in c2
;
:: thesis: p in fc * (Sgm domfc)then consider x,
y being
set such that A204:
p = [x,y]
by RELAT_1:def 1;
A205:
(
x in dom c2 &
y = c2 . x )
by A203, A204, FUNCT_1:8;
then reconsider k =
x as
Element of
NAT ;
A206:
( 1
<= k &
k <= len c2 )
by A205, FINSEQ_3:27;
A207:
x in dom (Sgm domfc)
by A200, A201, A205, FINSEQ_3:31;
A208:
m1 + k = (Sgm domfc) . k
by A189, A191, A192, A206, GRAPH_2:5;
A209:
(Sgm domfc) . k in rng (Sgm domfc)
by A207, FUNCT_1:def 5;
then A210:
x in dom (fc * (Sgm domfc))
by A202, A207, FUNCT_1:21;
0 + 1
<= k
by A205, FINSEQ_3:27;
then consider i being
Element of
NAT such that A211:
(
0 <= i &
i < len c2 &
k = i + 1 )
by A206, GRAPH_2:1;
(fc * (Sgm domfc)) . x =
fc . (m1 + k)
by A208, A210, FUNCT_1:22
.=
c . (m + i)
by A202, A208, A209, A211, GRFUNC_1:8
.=
y
by A2, A3, A167, A205, A211, Lm2
;
hence
p in fc * (Sgm domfc)
by A204, A210, FUNCT_1:8;
:: thesis: verum
end; assume A212:
p in fc * (Sgm domfc)
;
:: thesis: p in c2then consider x,
y being
set such that A213:
p = [x,y]
by RELAT_1:def 1;
A214:
(
x in dom (fc * (Sgm domfc)) &
y = (fc * (Sgm domfc)) . x )
by A212, A213, FUNCT_1:8;
then A215:
(
x in dom (Sgm domfc) &
(Sgm domfc) . x in dom fc )
by FUNCT_1:21;
then reconsider k =
x as
Element of
NAT ;
A216:
k in dom c2
by A200, A201, A215, FINSEQ_3:31;
A217:
( 1
<= k &
k <= len c2 )
by A200, A201, A215, FINSEQ_3:27;
then A218:
m1 + k = (Sgm domfc) . k
by A189, A191, A192, GRAPH_2:5;
0 + 1
<= k
by A215, FINSEQ_3:27;
then consider i being
Element of
NAT such that A219:
(
0 <= i &
i < len c2 &
k = i + 1 )
by A217, GRAPH_2:1;
c2 . k =
c . ((m1 + 1) + i)
by A2, A3, A167, A219, Lm2
.=
fc . ((Sgm domfc) . k)
by A215, A218, A219, GRFUNC_1:8
.=
y
by A214, A215, FUNCT_1:23
;
hence
p in c2
by A213, A216, FUNCT_1:8;
:: thesis: verum end; then
c2 = fc * (Sgm domfc)
by TARSKI:2;
hence
Seq fc = c1
by A173, FINSEQ_1:def 14;
:: thesis: Seq fvs = p1A220:
{ k where k is Element of NAT : ( m <= k & k <= len vs ) } c= Seg (len vs)
then reconsider domfvs =
{ k where k is Element of NAT : ( m <= k & k <= len vs ) } as
finite set by FINSET_1:13;
1
- 1
<= (len (m,((len c) + 1) -cut vs)) - 1
by A195, XREAL_1:11;
then
(len (m,((len c) + 1) -cut vs)) -' 1
= (len (m,((len c) + 1) -cut vs)) - 1
by XREAL_0:def 2;
then reconsider lp21 =
(len (m,((len c) + 1) -cut vs)) - 1 as
Element of
NAT ;
A222:
m + lp21 = (len c) + 1
by A194;
A223:
m + lp21 = m1 + (len (m,((len c) + 1) -cut vs))
;
A224:
card domfvs =
((len (m,((len c) + 1) -cut vs)) + (- 1)) + 1
by A3, A222, GRAPH_2:4
.=
len (m,((len c) + 1) -cut vs)
;
A225:
len (Sgm domfvs) = card domfvs
by A220, FINSEQ_3:44;
A226:
rng (Sgm domfvs) c= dom fvs
by A181, A220, FINSEQ_1:def 13;
set SR =
Sgm domfvs;
now let p be
set ;
:: thesis: ( ( p in m,((len c) + 1) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in m,((len c) + 1) -cut vs ) )hereby :: thesis: ( p in fvs * (Sgm domfvs) implies p in m,((len c) + 1) -cut vs )
assume A227:
p in m,
((len c) + 1) -cut vs
;
:: thesis: p in fvs * (Sgm domfvs)then consider x,
y being
set such that A228:
p = [x,y]
by RELAT_1:def 1;
A229:
(
x in dom (m,((len c) + 1) -cut vs) &
y = (m,((len c) + 1) -cut vs) . x )
by A227, A228, FUNCT_1:8;
then reconsider k =
x as
Element of
NAT ;
A230:
( 1
<= k &
k <= len (m,((len c) + 1) -cut vs) )
by A229, FINSEQ_3:27;
A231:
x in dom (Sgm domfvs)
by A224, A225, A229, FINSEQ_3:31;
A232:
m1 + k = (Sgm domfvs) . k
by A3, A191, A194, A223, A230, GRAPH_2:5;
A233:
(Sgm domfvs) . k in rng (Sgm domfvs)
by A231, FUNCT_1:def 5;
then A234:
x in dom (fvs * (Sgm domfvs))
by A226, A231, FUNCT_1:21;
0 + 1
<= k
by A229, FINSEQ_3:27;
then consider i being
Element of
NAT such that A235:
(
0 <= i &
i < len (m,((len c) + 1) -cut vs) &
k = i + 1 )
by A230, GRAPH_2:1;
(fvs * (Sgm domfvs)) . x =
fvs . (m1 + k)
by A232, A234, FUNCT_1:22
.=
vs . (m + i)
by A226, A232, A233, A235, GRFUNC_1:8
.=
y
by A193, A229, A235, Lm2
;
hence
p in fvs * (Sgm domfvs)
by A228, A234, FUNCT_1:8;
:: thesis: verum
end; assume A236:
p in fvs * (Sgm domfvs)
;
:: thesis: p in m,((len c) + 1) -cut vsthen consider x,
y being
set such that A237:
p = [x,y]
by RELAT_1:def 1;
A238:
(
x in dom (fvs * (Sgm domfvs)) &
y = (fvs * (Sgm domfvs)) . x )
by A236, A237, FUNCT_1:8;
then A239:
(
x in dom (Sgm domfvs) &
(Sgm domfvs) . x in dom fvs )
by FUNCT_1:21;
then reconsider k =
x as
Element of
NAT ;
A240:
k in dom (m,((len c) + 1) -cut vs)
by A224, A225, A239, FINSEQ_3:31;
A241:
( 1
<= k &
k <= len (m,((len c) + 1) -cut vs) )
by A224, A225, A239, FINSEQ_3:27;
then A242:
m1 + k = (Sgm domfvs) . k
by A3, A191, A194, A223, GRAPH_2:5;
0 + 1
<= k
by A239, FINSEQ_3:27;
then consider i being
Element of
NAT such that A243:
(
0 <= i &
i < len (m,((len c) + 1) -cut vs) &
k = i + 1 )
by A241, GRAPH_2:1;
(m,((len c) + 1) -cut vs) . k =
vs . ((m1 + 1) + i)
by A193, A243, Lm2
.=
fvs . ((Sgm domfvs) . k)
by A239, A242, A243, GRFUNC_1:8
.=
y
by A238, A239, FUNCT_1:23
;
hence
p in m,
((len c) + 1) -cut vs
by A237, A240, FUNCT_1:8;
:: thesis: verum end; then
m,
((len c) + 1) -cut vs = fvs * (Sgm domfvs)
by TARSKI:2;
hence
Seq fvs = p1
by A181, FINSEQ_1:def 14;
:: thesis: verum end; suppose A244:
(
n <> 1 &
m = len vs )
;
:: thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )then
1
< n
by A2, XXREAL_0:1;
then
1
+ 1
<= n
by NAT_1:13;
then A245:
(1 + 1) - 1
<= n - 1
by XREAL_1:11;
n < len vs
by A2, XXREAL_0:2;
then A246:
n - 1
< ((len c) + 1) - 1
by A3, XREAL_1:11;
A247:
1
<= n1 + 1
by NAT_1:12;
reconsider c1 = 1,
n1 -cut c as
oriented Chain of
G by A6, A245, A246, Th13;
set pp = 1,
n -cut vs;
A248:
( 1
<= n &
n <= len vs )
by A2, XXREAL_0:2;
A249:
1,
n -cut vs is_oriented_vertex_seq_of c1
by A1, A7, A245, A246, Th14;
then A250:
len (1,n -cut vs) = (len c1) + 1
by Def5;
set domfc =
{ k where k is Element of NAT : ( 1 <= k & k <= n1 ) } ;
deffunc H1(
set )
-> set =
c . $1;
consider fc being
Function such that A251:
dom fc = { k where k is Element of NAT : ( 1 <= k & k <= n1 ) }
and A252:
for
x being
set st
x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } holds
fc . x = H1(
x)
from FUNCT_1:sch 3();
{ k where k is Element of NAT : ( 1 <= k & k <= n1 ) } c= Seg (len c)
then reconsider fc =
fc as
FinSubsequence by A251, FINSEQ_1:def 12;
fc c= c
proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in fc or p in c )
assume A254:
p in fc
;
:: thesis: p in c
then consider x,
y being
set such that A255:
[x,y] = p
by RELAT_1:def 1;
A256:
(
x in dom fc &
y = fc . x )
by A254, A255, FUNCT_1:8;
then consider kk being
Element of
NAT such that A257:
(
x = kk & 1
<= kk &
kk <= n1 )
by A251;
( 1
<= kk &
kk <= len c )
by A6, A246, A257, XXREAL_0:2;
then A258:
x in dom c
by A257, FINSEQ_3:27;
y = c . kk
by A251, A252, A256, A257;
hence
p in c
by A255, A257, A258, FUNCT_1:8;
:: thesis: verum
end; then reconsider fc =
fc as
Subset of
c ;
take
fc
;
:: thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )set domfvs =
{ k where k is Element of NAT : ( 1 <= k & k <= n ) } ;
deffunc H2(
set )
-> set =
vs . $1;
consider fvs being
Function such that A259:
dom fvs = { k where k is Element of NAT : ( 1 <= k & k <= n ) }
and A260:
for
x being
set st
x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } holds
fvs . x = H2(
x)
from FUNCT_1:sch 3();
{ k where k is Element of NAT : ( 1 <= k & k <= n ) } c= Seg (len vs)
then reconsider fvs =
fvs as
FinSubsequence by A259, FINSEQ_1:def 12;
fvs c= vs
proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in fvs or p in vs )
assume A262:
p in fvs
;
:: thesis: p in vs
then consider x,
y being
set such that A263:
[x,y] = p
by RELAT_1:def 1;
A264:
(
x in dom fvs &
y = fvs . x )
by A262, A263, FUNCT_1:8;
then consider kk being
Element of
NAT such that A265:
(
x = kk & 1
<= kk &
kk <= n )
by A259;
( 1
<= kk &
kk <= len vs )
by A248, A265, XXREAL_0:2;
then A266:
x in dom vs
by A265, FINSEQ_3:27;
y = vs . kk
by A259, A260, A264, A265;
hence
p in vs
by A263, A265, A266, FUNCT_1:8;
:: thesis: verum
end; then reconsider fvs =
fvs as
Subset of
vs ;
take
fvs
;
:: thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )take c' =
c1;
:: thesis: ex vs1 being FinSequence of the carrier of G st
( len c' < len c & vs1 is_oriented_vertex_seq_of c' & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c' & Seq fvs = vs1 )take p1 = 1,
n -cut vs;
:: thesis: ( len c' < len c & p1 is_oriented_vertex_seq_of c' & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )A267:
(len c1) + 1
= n1 + 1
by A6, A246, A247, Lm2;
then A268:
len c1 = n - 1
by A5, XREAL_0:def 2;
thus
len c' < len c
by A5, A246, A267, XREAL_0:def 2;
:: thesis: ( p1 is_oriented_vertex_seq_of c' & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )thus
p1 is_oriented_vertex_seq_of c'
by A1, A7, A245, A246, Th14;
:: thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )
len p1 = (len c1) + 1
by A249, Def5;
hence
len p1 < len vs
by A2, A268, XXREAL_0:2;
:: thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )thus
vs . 1
= p1 . 1
by A248, GRAPH_2:12;
:: thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c' & Seq fvs = p1 )thus
vs . (len vs) = p1 . (len p1)
by A2, A244, GRAPH_2:12;
:: thesis: ( Seq fc = c' & Seq fvs = p1 )
{ k where k is Element of NAT : ( 1 <= k & k <= n1 ) } c= Seg (len c)
then reconsider domfc =
{ k where k is Element of NAT : ( 1 <= k & k <= n1 ) } as
finite set by FINSET_1:13;
domfc = Seg n1
by FINSEQ_1:def 1;
then A270:
Sgm domfc = idseq n1
by FINSEQ_3:54;
then A271:
dom (Sgm domfc) = Seg n1
by RELAT_1:71;
set SL =
Sgm domfc;
now let p be
set ;
:: thesis: ( ( p in c1 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c1 ) )hereby :: thesis: ( p in fc * (Sgm domfc) implies p in c1 )
assume A272:
p in c1
;
:: thesis: p in fc * (Sgm domfc)then consider x,
y being
set such that A273:
p = [x,y]
by RELAT_1:def 1;
A274:
(
x in dom c1 &
y = c1 . x )
by A272, A273, FUNCT_1:8;
then reconsider k =
x as
Element of
NAT ;
A275:
( 1
<= k &
k <= len c1 )
by A274, FINSEQ_3:27;
then A276:
x in dom (Sgm domfc)
by A267, A271, FINSEQ_1:3;
then A277:
k = (Sgm domfc) . k
by A270, A271, FUNCT_1:35;
A278:
k in domfc
by A267, A275;
then A279:
x in dom (fc * (Sgm domfc))
by A251, A276, A277, FUNCT_1:21;
0 + 1
<= k
by A274, FINSEQ_3:27;
then consider i being
Element of
NAT such that A280:
(
0 <= i &
i < n1 &
k = i + 1 )
by A267, A275, GRAPH_2:1;
(fc * (Sgm domfc)) . x =
fc . k
by A277, A279, FUNCT_1:22
.=
c . (1 + i)
by A251, A278, A280, GRFUNC_1:8
.=
y
by A6, A246, A247, A267, A274, A280, Lm2
;
hence
p in fc * (Sgm domfc)
by A273, A279, FUNCT_1:8;
:: thesis: verum
end; assume A281:
p in fc * (Sgm domfc)
;
:: thesis: p in c1then consider x,
y being
set such that A282:
p = [x,y]
by RELAT_1:def 1;
A283:
(
x in dom (fc * (Sgm domfc)) &
y = (fc * (Sgm domfc)) . x )
by A281, A282, FUNCT_1:8;
then A284:
(fc * (Sgm domfc)) . x = fc . ((Sgm domfc) . x)
by FUNCT_1:22;
A285:
(
x in dom (Sgm domfc) &
(Sgm domfc) . x in dom fc )
by A283, FUNCT_1:21;
then
x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) }
by A271, FINSEQ_1:def 1;
then consider k being
Element of
NAT such that A286:
(
k = x & 1
<= k &
k <= n1 )
;
A287:
k in dom fc
by A251, A286;
A288:
k = (Sgm domfc) . k
by A270, A271, A285, A286, FUNCT_1:35;
A289:
k in dom c1
by A267, A286, FINSEQ_3:27;
0 + 1
<= k
by A286;
then consider i being
Element of
NAT such that A290:
(
0 <= i &
i < n1 &
k = i + 1 )
by A286, GRAPH_2:1;
c1 . k =
c . k
by A6, A246, A247, A267, A290, Lm2
.=
y
by A283, A284, A286, A287, A288, GRFUNC_1:8
;
hence
p in c1
by A282, A286, A289, FUNCT_1:8;
:: thesis: verum end; then
c1 = fc * (Sgm domfc)
by TARSKI:2;
hence
Seq fc = c'
by A251, FINSEQ_1:def 14;
:: thesis: Seq fvs = p1
{ k where k is Element of NAT : ( 1 <= k & k <= n ) } c= Seg (len vs)
then reconsider domfvs =
{ k where k is Element of NAT : ( 1 <= k & k <= n ) } as
finite set by FINSET_1:13;
domfvs = Seg n
by FINSEQ_1:def 1;
then A292:
Sgm domfvs = idseq n
by FINSEQ_3:54;
then A293:
dom (Sgm domfvs) = Seg n
by RELAT_1:71;
set SL =
Sgm domfvs;
now let p be
set ;
:: thesis: ( ( p in 1,n -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in 1,n -cut vs ) )hereby :: thesis: ( p in fvs * (Sgm domfvs) implies p in 1,n -cut vs )
assume A294:
p in 1,
n -cut vs
;
:: thesis: p in fvs * (Sgm domfvs)then consider x,
y being
set such that A295:
p = [x,y]
by RELAT_1:def 1;
A296:
(
x in dom (1,n -cut vs) &
y = (1,n -cut vs) . x )
by A294, A295, FUNCT_1:8;
then reconsider k =
x as
Element of
NAT ;
A297:
( 1
<= k &
k <= len (1,n -cut vs) )
by A296, FINSEQ_3:27;
then A298:
x in dom (Sgm domfvs)
by A250, A268, A293, FINSEQ_1:3;
then A299:
k = (Sgm domfvs) . k
by A292, A293, FUNCT_1:35;
A300:
k in domfvs
by A250, A268, A297;
then A301:
x in dom (fvs * (Sgm domfvs))
by A259, A298, A299, FUNCT_1:21;
0 + 1
<= k
by A296, FINSEQ_3:27;
then consider i being
Element of
NAT such that A302:
(
0 <= i &
i < n &
k = i + 1 )
by A250, A268, A297, GRAPH_2:1;
(fvs * (Sgm domfvs)) . x =
fvs . k
by A299, A301, FUNCT_1:22
.=
vs . (1 + i)
by A259, A300, A302, GRFUNC_1:8
.=
y
by A248, A250, A268, A296, A302, GRAPH_2:def 1
;
hence
p in fvs * (Sgm domfvs)
by A295, A301, FUNCT_1:8;
:: thesis: verum
end; assume A303:
p in fvs * (Sgm domfvs)
;
:: thesis: p in 1,n -cut vsthen consider x,
y being
set such that A304:
p = [x,y]
by RELAT_1:def 1;
A305:
(
x in dom (fvs * (Sgm domfvs)) &
y = (fvs * (Sgm domfvs)) . x )
by A303, A304, FUNCT_1:8;
then A306:
(fvs * (Sgm domfvs)) . x = fvs . ((Sgm domfvs) . x)
by FUNCT_1:22;
A307:
(
x in dom (Sgm domfvs) &
(Sgm domfvs) . x in dom fvs )
by A305, FUNCT_1:21;
then
x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) }
by A293, FINSEQ_1:def 1;
then consider k being
Element of
NAT such that A308:
(
k = x & 1
<= k &
k <= n )
;
A309:
k in dom fvs
by A259, A308;
A310:
k = (Sgm domfvs) . k
by A292, A293, A307, A308, FUNCT_1:35;
A311:
k in dom (1,n -cut vs)
by A250, A268, A308, FINSEQ_3:27;
0 + 1
<= k
by A308;
then consider i being
Element of
NAT such that A312:
(
0 <= i &
i < n &
k = i + 1 )
by A308, GRAPH_2:1;
(1,n -cut vs) . k =
vs . k
by A248, A250, A268, A312, GRAPH_2:def 1
.=
y
by A305, A306, A308, A309, A310, GRFUNC_1:8
;
hence
p in 1,
n -cut vs
by A304, A308, A311, FUNCT_1:8;
:: thesis: verum end; then
1,
n -cut vs = fvs * (Sgm domfvs)
by TARSKI:2;
hence
Seq fvs = p1
by A259, FINSEQ_1:def 14;
:: thesis: verum end;