let G be Graph; 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; 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; ( 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 that
A1:
not c is Simple
and
A2:
vs is_oriented_vertex_seq_of c
; 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 )
consider n, m being Nat such that
A3:
1 <= n
and
A4:
n < m
and
A5:
m <= len vs
and
A6:
vs . n = vs . m
and
A7:
( n <> 1 or m <> len vs )
by A1, A2;
A8:
len vs = (len c) + 1
by A2;
A9:
m - n > n - n
by A4, XREAL_1:9;
reconsider n1 = n -' 1 as Element of NAT ;
A10:
1 - 1 <= n - 1
by A3, XREAL_1:9;
then A11:
n - 1 = n -' 1
by XREAL_0:def 2;
A12: n1 + 1 =
(n - 1) + 1
by A10, 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 A7;
suppose A13:
(
n <> 1 &
m <> len vs )
;
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 A3, XXREAL_0:1;
then
1
+ 1
<= n
by NAT_1:13;
then A14:
(1 + 1) - 1
<= n - 1
by XREAL_1:9;
n < len vs
by A4, A5, XXREAL_0:2;
then A15:
n - 1
< ((len c) + 1) - 1
by A8, XREAL_1:9;
A16:
1
<= n1 + 1
by NAT_1:12;
A17:
m < len vs
by A5, A13, XXREAL_0:1;
then A18:
m <= len c
by A8, NAT_1:13;
A19:
1
<= m
by A3, A4, XXREAL_0:2;
A20:
m <= len c
by A8, A17, NAT_1:13;
reconsider c1 = (1,
n1)
-cut c as
oriented Chain of
G by A11, A14, A15, Th12;
reconsider c2 = (
m,
(len c))
-cut c as
oriented Chain of
G by A19, A20, Th12;
set pp = (1,
n)
-cut vs;
set p2 = (
m,
((len c) + 1))
-cut vs;
set p29 = (
(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 ;
A21:
n <= len vs
by A4, A5, XXREAL_0:2;
A22:
1
<= m
by A3, A4, XXREAL_0:2;
A23:
m <= (len c) + 1
by A2, A5;
A24:
(len c) + 1
<= len vs
by A2;
A25:
pp is_oriented_vertex_seq_of c1
by A2, A12, A14, A15, Th13;
A26:
p2 is_oriented_vertex_seq_of c2
by A2, A19, A20, Th13;
A27:
len pp = (len c1) + 1
by A25;
A28:
len p2 = (len c2) + 1
by A26;
1
- 1
<= m - 1
by A19, XREAL_1:9;
then
m -' 1
= m - 1
by XREAL_0:def 2;
then reconsider m1 =
m - 1 as
Element of
NAT ;
A29:
m = m1 + 1
;
A30:
(len c2) + m = (len c) + 1
by A19, A20, FINSEQ_6:def 4;
A31:
m - m <= (len c) - m
by A18, XREAL_1:9;
then
(len c2) -' 1
= (len c2) - 1
by A30, XREAL_0:def 2;
then reconsider lc21 =
(len c2) - 1 as
Element of
NAT ;
A32:
m + lc21 = m1 + (len c2)
;
0 + 1
= 1
;
then A33:
1
<= len p2
by A28, NAT_1:13;
A34:
p2 =
(
(0 + 1),
(len p2))
-cut p2
by FINSEQ_6:133
.=
(((0 + 1),1) -cut p2) ^ (((1 + 1),(len p2)) -cut p2)
by A33, FINSEQ_6:134
;
m1 <= m
by A29, NAT_1:12;
then A35:
p2 = (((m1 + 1),m) -cut vs) ^ (((m + 1),((len c) + 1)) -cut vs)
by A5, A8, FINSEQ_6:134;
(1,1)
-cut p2 =
<*(p2 . (0 + 1))*>
by A33, FINSEQ_6:132
.=
<*(vs . (m + 0))*>
by A22, A23, A24, A28, FINSEQ_6:def 4
.=
(
m,
m)
-cut vs
by A5, A19, FINSEQ_6:132
;
then A36:
(
(m + 1),
((len c) + 1))
-cut vs = (2,
(len p2))
-cut p2
by A34, A35, FINSEQ_1:33;
set domfc =
{ k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ;
deffunc H1(
object )
-> set =
c . $1;
consider fc being
Function such that A37:
dom fc = { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) }
and A38:
for
x being
object st
x in { k where k is 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 Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } c= Seg (len c)
then reconsider fc =
fc as
FinSubsequence by A37, FINSEQ_1:def 12;
fc c= c
proof
let p be
object ;
TARSKI:def 3 ( not p in fc or p in c )
assume A42:
p in fc
;
p in c
then consider x,
y being
object such that A43:
[x,y] = p
by RELAT_1:def 1;
A44:
x in dom fc
by A42, A43, FUNCT_1:1;
A45:
y = fc . x
by A42, A43, FUNCT_1:1;
consider kk being
Nat such that A46:
x = kk
and A47:
( ( 1
<= kk &
kk <= n1 ) or (
m <= kk &
kk <= len c ) )
by A37, A44;
A48:
1
<= kk
by A19, A47, XXREAL_0:2;
kk <= len c
by A11, A15, A47, XXREAL_0:2;
then A49:
x in dom c
by A46, A48, FINSEQ_3:25;
y = c . kk
by A37, A38, A44, A45, A46;
hence
p in c
by A43, A46, A49, FUNCT_1:1;
verum
end; then reconsider fc =
fc as
Subset of
c ;
take
fc
;
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 Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ;
deffunc H2(
object )
-> set =
vs . $1;
consider fvs being
Function such that A50:
dom fvs = { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) }
and A51:
for
x being
object st
x in { k where k is 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 Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } c= Seg (len vs)
then reconsider fvs =
fvs as
FinSubsequence by A50, FINSEQ_1:def 12;
fvs c= vs
proof
let p be
object ;
TARSKI:def 3 ( not p in fvs or p in vs )
assume A55:
p in fvs
;
p in vs
then consider x,
y being
object such that A56:
[x,y] = p
by RELAT_1:def 1;
A57:
x in dom fvs
by A55, A56, FUNCT_1:1;
A58:
y = fvs . x
by A55, A56, FUNCT_1:1;
consider kk being
Nat such that A59:
x = kk
and A60:
( ( 1
<= kk &
kk <= n ) or (
m + 1
<= kk &
kk <= len vs ) )
by A50, A57;
1
<= m + 1
by NAT_1:12;
then A61:
1
<= kk
by A60, XXREAL_0:2;
kk <= len vs
by A21, A60, XXREAL_0:2;
then A62:
x in dom vs
by A59, A61, FINSEQ_3:25;
y = vs . kk
by A50, A51, A57, A58, A59;
hence
p in vs
by A56, A59, A62, FUNCT_1:1;
verum
end; then reconsider fvs =
fvs as
Subset of
vs ;
take
fvs
;
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 )A63:
p2 . 1
= vs . m
by A22, A23, A24, FINSEQ_6:138;
A64:
pp . (len pp) = vs . n
by A3, A21, FINSEQ_6:138;
then reconsider c9 =
c1 ^ c2 as
oriented Chain of
G by A6, A25, A26, A63, Th14;
take
c9
;
ex vs1 being FinSequence of the carrier of G st
( len c9 < len c & vs1 is_oriented_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 )take p1 =
pp ^' p2;
( len c9 < len c & p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )A65:
p1 = pp ^ (((m + 1),((len c) + 1)) -cut vs)
by A36, FINSEQ_6:def 5;
A66:
(len c1) + 1
= n1 + 1
by A11, A15, A16, Lm2;
- (- (m - n)) = m - n
;
then A67:
- (m - n) < 0
by A9;
len c9 =
(n - 1) + (((len c) - m) + 1)
by A11, A30, A66, FINSEQ_1:22
.=
(len c) + (n + (- m))
;
hence A68:
len c9 < len c
by A67, XREAL_1:30;
( p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )thus
p1 is_oriented_vertex_seq_of c9
by A6, A25, A26, A63, A64, Th15;
( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )then
len p1 = (len c9) + 1
;
hence
len p1 < len vs
by A8, A68, XREAL_1:6;
( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
1
<= 1
+ (len c1)
by NAT_1:12;
then
1
<= len pp
by A25;
then
p1 . 1
= pp . 1
by FINSEQ_6:140;
hence
vs . 1
= p1 . 1
by A3, A21, FINSEQ_6:138;
( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )A69:
p2 . (len p2) = vs . ((len c) + 1)
by A22, A23, A24, FINSEQ_6:138;
m - m <= (len c) - m
by A20, XREAL_1:9;
then
0 + 1
<= ((len c) - m) + 1
by XREAL_1:6;
then
1
< len p2
by A28, A30, NAT_1:13;
hence
vs . (len vs) = p1 . (len p1)
by A8, A69, FINSEQ_6:142;
( Seq fc = c9 & Seq fvs = p1 )set DL =
{ kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } ;
set DR =
{ kk where kk is Nat : ( m <= kk & kk <= len c ) } ;
now for x being object holds
( ( x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } implies x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ) )let x be
object ;
( ( x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } implies b1 in { b2 where k is Nat : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } ) )hereby ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } implies b1 in { b2 where k is Nat : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } )
assume
x in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) }
;
x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) } then
ex
k being
Nat st
(
x = k & ( ( 1
<= k &
k <= n1 ) or (
m <= k &
k <= len c ) ) )
;
then
(
x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } or
x in { kk where kk is Nat : ( m <= kk & kk <= len c ) } )
;
hence
x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) }
by XBOOLE_0:def 3;
verum
end; assume A70:
x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) }
;
b1 in { b2 where k is Nat : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } end; then A71:
{ k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } = { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Nat : ( m <= kk & kk <= len c ) }
by TARSKI:2;
A72:
(
{ kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } c= Seg (len c) &
{ kk where kk is Nat : ( m <= kk & kk <= len c ) } c= Seg (len c) )
then reconsider DL =
{ kk where kk is Nat : ( 1 <= kk & kk <= n1 ) } as
finite set by FINSET_1:1;
a72:
(
DL is
included_in_Seg &
{ kk where kk is Nat : ( m <= kk & kk <= len c ) } is
included_in_Seg )
by A72, FINSEQ_1:def 13;
reconsider DR =
{ kk where kk is Nat : ( m <= kk & kk <= len c ) } as
finite set by A72, FINSET_1:1;
now for i, j being Nat st i in DL & j in DR holds
i < jend; then A82:
Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR)
by a72, FINSEQ_3:42;
m + lc21 = len c
by A30;
then A83:
card DR =
((len c2) + (- 1)) + 1
by FINSEQ_6:130
.=
len c2
;
A84:
len (Sgm DR) = card DR
by a72, FINSEQ_3:39;
DL = Seg n1
by FINSEQ_1:def 1;
then A85:
Sgm DL = idseq n1
by FINSEQ_3:48;
then A86:
dom (Sgm DL) = Seg n1
;
rng (Sgm DL) = DL
by a72, FINSEQ_1:def 14;
then A87:
rng (Sgm DL) c= dom fc
by A37, A71, XBOOLE_1:7;
rng (Sgm DR) = DR
by a72, FINSEQ_1:def 14;
then A88:
rng (Sgm DR) c= dom fc
by A37, A71, XBOOLE_1:7;
set SL =
Sgm DL;
set SR =
Sgm DR;
now for p being object holds
( ( p in c1 implies p in fc * (Sgm DL) ) & ( p in fc * (Sgm DL) implies p in c1 ) )let p be
object ;
( ( p in c1 implies p in fc * (Sgm DL) ) & ( p in fc * (Sgm DL) implies p in c1 ) )hereby ( p in fc * (Sgm DL) implies p in c1 )
assume A89:
p in c1
;
p in fc * (Sgm DL)then consider x,
y being
object such that A90:
p = [x,y]
by RELAT_1:def 1;
A91:
x in dom c1
by A89, A90, FUNCT_1:1;
A92:
y = c1 . x
by A89, A90, FUNCT_1:1;
reconsider k =
x as
Element of
NAT by A91;
A93:
1
<= k
by A91, FINSEQ_3:25;
A94:
k <= len c1
by A91, FINSEQ_3:25;
then A95:
x in dom (Sgm DL)
by A66, A86, A93, FINSEQ_1:1;
then A96:
k = (Sgm DL) . k
by A85, FUNCT_1:18;
A97:
k in { k where k is Nat : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) }
by A66, A93, A94;
then A98:
x in dom (fc * (Sgm DL))
by A37, A95, A96, FUNCT_1:11;
0 + 1
<= k
by A91, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A99:
i < n1
and A100:
k = i + 1
by A66, A94, FINSEQ_6:127;
(fc * (Sgm DL)) . x =
fc . k
by A96, A98, FUNCT_1:12
.=
c . (1 + i)
by A37, A97, A100, GRFUNC_1:2
.=
y
by A11, A15, A16, A66, A92, A99, A100, Lm2
;
hence
p in fc * (Sgm DL)
by A90, A98, FUNCT_1:1;
verum
end; assume A101:
p in fc * (Sgm DL)
;
p in c1then consider x,
y being
object such that A102:
p = [x,y]
by RELAT_1:def 1;
A103:
x in dom (fc * (Sgm DL))
by A101, A102, FUNCT_1:1;
A104:
y = (fc * (Sgm DL)) . x
by A101, A102, FUNCT_1:1;
A105:
(fc * (Sgm DL)) . x = fc . ((Sgm DL) . x)
by A103, FUNCT_1:12;
A106:
x in dom (Sgm DL)
by A103, FUNCT_1:11;
then
x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) }
by A86, FINSEQ_1:def 1;
then consider k being
Nat such that A107:
k = x
and A108:
1
<= k
and A109:
k <= n1
;
A110:
k in dom fc
by A37, A108, A109;
A111:
k = (Sgm DL) . k
by A85, A106, A107, FUNCT_1:18;
A112:
k in dom c1
by A66, A108, A109, FINSEQ_3:25;
0 + 1
<= k
by A108;
then
ex
i being
Nat st
(
0 <= i &
i < n1 &
k = i + 1 )
by A109, FINSEQ_6:127;
then c1 . k =
c . k
by A11, A15, A16, A66, Lm2
.=
y
by A104, A105, A107, A110, A111, GRFUNC_1:2
;
hence
p in c1
by A102, A107, A112, FUNCT_1:1;
verum end; then A113:
c1 = fc * (Sgm DL)
by TARSKI:2;
now for p being object holds
( ( p in c2 implies p in fc * (Sgm DR) ) & ( p in fc * (Sgm DR) implies p in c2 ) )let p be
object ;
( ( p in c2 implies p in fc * (Sgm DR) ) & ( p in fc * (Sgm DR) implies p in c2 ) )hereby ( p in fc * (Sgm DR) implies p in c2 )
assume A114:
p in c2
;
p in fc * (Sgm DR)then consider x,
y being
object such that A115:
p = [x,y]
by RELAT_1:def 1;
A116:
x in dom c2
by A114, A115, FUNCT_1:1;
A117:
y = c2 . x
by A114, A115, FUNCT_1:1;
reconsider k =
x as
Element of
NAT by A116;
A118:
1
<= k
by A116, FINSEQ_3:25;
A119:
k <= len c2
by A116, FINSEQ_3:25;
A120:
x in dom (Sgm DR)
by A83, A84, A116, FINSEQ_3:29;
A121:
m1 + k = (Sgm DR) . k
by A29, A30, A32, A118, A119, FINSEQ_6:131;
A122:
(Sgm DR) . k in rng (Sgm DR)
by A120, FUNCT_1:def 3;
then A123:
x in dom (fc * (Sgm DR))
by A88, A120, FUNCT_1:11;
0 + 1
<= k
by A116, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A124:
i < len c2
and A125:
k = i + 1
by A119, FINSEQ_6:127;
(fc * (Sgm DR)) . x =
fc . (m1 + k)
by A121, A123, FUNCT_1:12
.=
c . (m + i)
by A88, A121, A122, A125, GRFUNC_1:2
.=
y
by A19, A20, A117, A124, A125, FINSEQ_6:def 4
;
hence
p in fc * (Sgm DR)
by A115, A123, FUNCT_1:1;
verum
end; assume A126:
p in fc * (Sgm DR)
;
p in c2then consider x,
y being
object such that A127:
p = [x,y]
by RELAT_1:def 1;
A128:
x in dom (fc * (Sgm DR))
by A126, A127, FUNCT_1:1;
A129:
y = (fc * (Sgm DR)) . x
by A126, A127, FUNCT_1:1;
A130:
x in dom (Sgm DR)
by A128, FUNCT_1:11;
A131:
(Sgm DR) . x in dom fc
by A128, FUNCT_1:11;
reconsider k =
x as
Element of
NAT by A130;
A132:
k in dom c2
by A83, A84, A130, FINSEQ_3:29;
A133:
1
<= k
by A130, FINSEQ_3:25;
A134:
k <= len c2
by A83, A84, A130, FINSEQ_3:25;
then A135:
m1 + k = (Sgm DR) . k
by A29, A30, A32, A133, FINSEQ_6:131;
0 + 1
<= k
by A130, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A136:
i < len c2
and A137:
k = i + 1
by A134, FINSEQ_6:127;
c2 . k =
c . ((m1 + 1) + i)
by A19, A20, A136, A137, FINSEQ_6:def 4
.=
fc . ((Sgm DR) . k)
by A131, A135, A137, GRFUNC_1:2
.=
y
by A129, A130, FUNCT_1:13
;
hence
p in c2
by A127, A132, FUNCT_1:1;
verum end; then A138:
c2 = fc * (Sgm DR)
by TARSKI:2;
Seq fc = fc * ((Sgm DL) ^ (Sgm DR))
by A37, A71, A82, FINSEQ_1:def 15;
hence
Seq fc = c9
by A87, A88, A113, A138, FINSEQ_6:150;
Seq fvs = p1set DL =
{ kk where kk is Nat : ( 1 <= kk & kk <= n ) } ;
set DR =
{ kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ;
now for x being object holds
( ( x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } implies x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ) )let x be
object ;
( ( x in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } implies x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } ) & ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } implies b1 in { b2 where k is Nat : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } ) )hereby ( x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } implies b1 in { b2 where k is Nat : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } )
end; assume A139:
x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) }
;
b1 in { b2 where k is Nat : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } end; then A140:
{ k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } = { kk where kk is Nat : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) }
by TARSKI:2;
A141:
(
{ kk where kk is Nat : ( 1 <= kk & kk <= n ) } c= Seg (len vs) &
{ kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } c= Seg (len vs) )
then reconsider DL =
{ kk where kk is Nat : ( 1 <= kk & kk <= n ) } as
finite set by FINSET_1:1;
a141:
(
DL is
included_in_Seg &
{ kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } is
included_in_Seg )
by A141, FINSEQ_1:def 13;
reconsider DR =
{ kk where kk is Nat : ( m + 1 <= kk & kk <= len vs ) } as
finite set by A141, FINSET_1:1;
now for i, j being Nat st i in DL & j in DR holds
i < jend; then A153:
Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR)
by a141, FINSEQ_3:42;
1
<= len p2
by A28, NAT_1:12;
then
1
- 1
<= (len p2) - 1
by XREAL_1:9;
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 A28, A30, A31, XREAL_0:def 2;
then reconsider lp22 =
lp21 - 1 as
Element of
NAT ;
A154:
(m + 1) + lp22 =
m + ((lp21 - 1) + 1)
.=
m + (((((len c) - m) + 1) + 1) - 1)
by A26, A30
.=
(len c) + 1
;
then A155:
card DR =
lp22 + 1
by A8, FINSEQ_6:130
.=
lp21
;
A156:
1
<= m + 1
by NAT_1:12;
A157:
m + 1
<= ((len c) + 1) + 1
by A23, XREAL_1:6;
A158:
(len p2) + m =
((len c) + 1) + 1
by A22, A23, A24, FINSEQ_6:def 4
.=
(len (((m + 1),((len c) + 1)) -cut vs)) + (m + 1)
by A24, A156, A157, Lm2
.=
((len (((m + 1),((len c) + 1)) -cut vs)) + 1) + m
;
A159:
len (Sgm DR) = card DR
by a141, FINSEQ_3:39;
DL = Seg n
by FINSEQ_1:def 1;
then A160:
Sgm DL = idseq n
by FINSEQ_3:48;
then A161:
dom (Sgm DL) = Seg n
;
rng (Sgm DL) = DL
by a141, FINSEQ_1:def 14;
then A162:
rng (Sgm DL) c= dom fvs
by A50, A140, XBOOLE_1:7;
rng (Sgm DR) = DR
by a141, FINSEQ_1:def 14;
then A163:
rng (Sgm DR) c= dom fvs
by A50, A140, XBOOLE_1:7;
set SL =
Sgm DL;
set SR =
Sgm DR;
now for p being object holds
( ( p in pp implies p in fvs * (Sgm DL) ) & ( p in fvs * (Sgm DL) implies p in pp ) )let p be
object ;
( ( p in pp implies p in fvs * (Sgm DL) ) & ( p in fvs * (Sgm DL) implies p in pp ) )hereby ( p in fvs * (Sgm DL) implies p in pp )
assume A164:
p in pp
;
p in fvs * (Sgm DL)then consider x,
y being
object such that A165:
p = [x,y]
by RELAT_1:def 1;
A166:
x in dom pp
by A164, A165, FUNCT_1:1;
A167:
y = pp . x
by A164, A165, FUNCT_1:1;
reconsider k =
x as
Element of
NAT by A166;
A168:
1
<= k
by A166, FINSEQ_3:25;
A169:
k <= len pp
by A166, FINSEQ_3:25;
then A170:
x in dom (Sgm DL)
by A11, A27, A66, A161, A168, FINSEQ_1:1;
then A171:
k = (Sgm DL) . k
by A160, FUNCT_1:18;
A172:
k in { k where k is Nat : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) }
by A11, A27, A66, A168, A169;
then A173:
x in dom (fvs * (Sgm DL))
by A50, A170, A171, FUNCT_1:11;
0 + 1
<= k
by A166, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A174:
i < n
and A175:
k = i + 1
by A11, A27, A66, A169, FINSEQ_6:127;
(fvs * (Sgm DL)) . x =
fvs . k
by A171, A173, FUNCT_1:12
.=
vs . (1 + i)
by A50, A172, A175, GRFUNC_1:2
.=
y
by A3, A11, A21, A27, A66, A167, A174, A175, FINSEQ_6:def 4
;
hence
p in fvs * (Sgm DL)
by A165, A173, FUNCT_1:1;
verum
end; assume A176:
p in fvs * (Sgm DL)
;
p in ppthen consider x,
y being
object such that A177:
p = [x,y]
by RELAT_1:def 1;
A178:
x in dom (fvs * (Sgm DL))
by A176, A177, FUNCT_1:1;
A179:
y = (fvs * (Sgm DL)) . x
by A176, A177, FUNCT_1:1;
A180:
(fvs * (Sgm DL)) . x = fvs . ((Sgm DL) . x)
by A178, FUNCT_1:12;
A181:
x in dom (Sgm DL)
by A178, FUNCT_1:11;
then
x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) }
by A161, FINSEQ_1:def 1;
then consider k being
Nat such that A182:
k = x
and A183:
1
<= k
and A184:
k <= n
;
A185:
k in dom fvs
by A50, A183, A184;
A186:
k = (Sgm DL) . k
by A160, A181, A182, FUNCT_1:18;
A187:
k in dom pp
by A11, A27, A66, A183, A184, FINSEQ_3:25;
0 + 1
<= k
by A183;
then
ex
i being
Nat st
(
0 <= i &
i < n &
k = i + 1 )
by A184, FINSEQ_6:127;
then pp . k =
vs . k
by A3, A11, A21, A27, A66, FINSEQ_6:def 4
.=
y
by A179, A180, A182, A185, A186, GRFUNC_1:2
;
hence
p in pp
by A177, A182, A187, FUNCT_1:1;
verum end; then A188:
pp = fvs * (Sgm DL)
by TARSKI:2;
A189:
(m + 1) + lp22 = m + lp21
;
A190:
1
<= m + 1
by NAT_1:12;
A191:
m + 1
<= ((len c) + 1) + 1
by A5, A8, XREAL_1:7;
now for p being object holds
( ( 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 ) )let p be
object ;
( ( 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 ( p in fvs * (Sgm DR) implies p in ((m + 1),((len c) + 1)) -cut vs )
assume A192:
p in (
(m + 1),
((len c) + 1))
-cut vs
;
p in fvs * (Sgm DR)then consider x,
y being
object such that A193:
p = [x,y]
by RELAT_1:def 1;
A194:
x in dom (((m + 1),((len c) + 1)) -cut vs)
by A192, A193, FUNCT_1:1;
A195:
y = (((m + 1),((len c) + 1)) -cut vs) . x
by A192, A193, FUNCT_1:1;
reconsider k =
x as
Element of
NAT by A194;
A196:
1
<= k
by A194, FINSEQ_3:25;
A197:
k <= len (((m + 1),((len c) + 1)) -cut vs)
by A194, FINSEQ_3:25;
A198:
x in dom (Sgm DR)
by A155, A158, A159, A194, FINSEQ_3:29;
A199:
m + k = (Sgm DR) . k
by A8, A154, A158, A189, A196, A197, FINSEQ_6:131;
A200:
(Sgm DR) . k in rng (Sgm DR)
by A198, FUNCT_1:def 3;
then A201:
x in dom (fvs * (Sgm DR))
by A163, A198, FUNCT_1:11;
0 + 1
<= k
by A194, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A202:
i < len (((m + 1),((len c) + 1)) -cut vs)
and A203:
k = i + 1
by A197, FINSEQ_6:127;
(fvs * (Sgm DR)) . x =
fvs . (m + k)
by A199, A201, FUNCT_1:12
.=
vs . ((m + 1) + i)
by A163, A199, A200, A203, GRFUNC_1:2
.=
y
by A8, A190, A191, A195, A202, A203, Lm2
;
hence
p in fvs * (Sgm DR)
by A193, A201, FUNCT_1:1;
verum
end; assume A204:
p in fvs * (Sgm DR)
;
p in ((m + 1),((len c) + 1)) -cut vsthen consider x,
y being
object such that A205:
p = [x,y]
by RELAT_1:def 1;
A206:
x in dom (fvs * (Sgm DR))
by A204, A205, FUNCT_1:1;
A207:
y = (fvs * (Sgm DR)) . x
by A204, A205, FUNCT_1:1;
A208:
x in dom (Sgm DR)
by A206, FUNCT_1:11;
A209:
(Sgm DR) . x in dom fvs
by A206, FUNCT_1:11;
reconsider k =
x as
Element of
NAT by A208;
A210:
k in dom (((m + 1),((len c) + 1)) -cut vs)
by A155, A158, A159, A208, FINSEQ_3:29;
A211:
1
<= k
by A208, FINSEQ_3:25;
A212:
k <= len (((m + 1),((len c) + 1)) -cut vs)
by A155, A158, A159, A208, FINSEQ_3:25;
then A213:
m + k = (Sgm DR) . k
by A8, A154, A158, A189, A211, FINSEQ_6:131;
0 + 1
<= k
by A208, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A214:
i < len (((m + 1),((len c) + 1)) -cut vs)
and A215:
k = i + 1
by A212, FINSEQ_6:127;
(((m + 1),((len c) + 1)) -cut vs) . k =
vs . ((m + 1) + i)
by A8, A190, A191, A214, A215, Lm2
.=
fvs . ((Sgm DR) . k)
by A209, A213, A215, GRFUNC_1:2
.=
y
by A207, A208, FUNCT_1:13
;
hence
p in (
(m + 1),
((len c) + 1))
-cut vs
by A205, A210, FUNCT_1:1;
verum end; then A216:
(
(m + 1),
((len c) + 1))
-cut vs = fvs * (Sgm DR)
by TARSKI:2;
Seq fvs = fvs * ((Sgm DL) ^ (Sgm DR))
by A50, A140, A153, FINSEQ_1:def 15;
hence
Seq fvs = p1
by A65, A162, A163, A188, A216, FINSEQ_6:150;
verum end; suppose A217:
(
n = 1 &
m <> len vs )
;
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 A218:
m < len vs
by A5, XXREAL_0:1;
then A219:
m <= len c
by A8, NAT_1:13;
A220:
1
< m
by A3, A4, XXREAL_0:2;
A221:
1
<= m
by A3, A4, XXREAL_0:2;
A222:
m <= len c
by A8, A218, NAT_1:13;
reconsider c2 = (
m,
(len c))
-cut c as
oriented Chain of
G by A219, A220, Th12;
set p2 = (
m,
((len c) + 1))
-cut vs;
A223:
(
m,
((len c) + 1))
-cut vs is_oriented_vertex_seq_of c2
by A2, A219, A220, Th13;
set domfc =
{ k where k is Nat : ( m <= k & k <= len c ) } ;
deffunc H1(
object )
-> set =
c . $1;
consider fc being
Function such that A224:
dom fc = { k where k is Nat : ( m <= k & k <= len c ) }
and A225:
for
x being
object st
x in { k where k is Nat : ( m <= k & k <= len c ) } holds
fc . x = H1(
x)
from FUNCT_1:sch 3();
{ k where k is Nat : ( m <= k & k <= len c ) } c= Seg (len c)
then reconsider fc =
fc as
FinSubsequence by A224, FINSEQ_1:def 12;
fc c= c
proof
let p be
object ;
TARSKI:def 3 ( not p in fc or p in c )
assume A229:
p in fc
;
p in c
then consider x,
y being
object such that A230:
[x,y] = p
by RELAT_1:def 1;
A231:
x in dom fc
by A229, A230, FUNCT_1:1;
A232:
y = fc . x
by A229, A230, FUNCT_1:1;
consider kk being
Nat such that A233:
x = kk
and A234:
m <= kk
and A235:
kk <= len c
by A224, A231;
1
<= kk
by A220, A234, XXREAL_0:2;
then A236:
x in dom c
by A233, A235, FINSEQ_3:25;
y = c . kk
by A224, A225, A231, A232, A233;
hence
p in c
by A230, A233, A236, FUNCT_1:1;
verum
end; then reconsider fc =
fc as
Subset of
c ;
take
fc
;
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 Nat : ( m <= k & k <= len vs ) } ;
deffunc H2(
object )
-> set =
vs . $1;
consider fvs being
Function such that A237:
dom fvs = { k where k is Nat : ( m <= k & k <= len vs ) }
and A238:
for
x being
object st
x in { k where k is Nat : ( m <= k & k <= len vs ) } holds
fvs . x = H2(
x)
from FUNCT_1:sch 3();
{ k where k is Nat : ( m <= k & k <= len vs ) } c= Seg (len vs)
then reconsider fvs =
fvs as
FinSubsequence by A237, FINSEQ_1:def 12;
fvs c= vs
proof
let p be
object ;
TARSKI:def 3 ( not p in fvs or p in vs )
assume A242:
p in fvs
;
p in vs
then consider x,
y being
object such that A243:
[x,y] = p
by RELAT_1:def 1;
A244:
x in dom fvs
by A242, A243, FUNCT_1:1;
A245:
y = fvs . x
by A242, A243, FUNCT_1:1;
consider kk being
Nat such that A246:
x = kk
and A247:
m <= kk
and A248:
kk <= len vs
by A237, A244;
1
<= kk
by A220, A247, XXREAL_0:2;
then A249:
x in dom vs
by A246, A248, FINSEQ_3:25;
y = vs . kk
by A237, A238, A244, A245, A246;
hence
p in vs
by A243, A246, A249, FUNCT_1:1;
verum
end; then reconsider fvs =
fvs as
Subset of
vs ;
take
fvs
;
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;
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;
( 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 )A250:
(len c2) + m = (len c) + 1
by A4, A5, A8, A217, Lm2;
A251:
m - m <= (len c) - m
by A219, XREAL_1:9;
1
- 1
<= m - 1
by A220, XREAL_1:9;
then
m -' 1
= m - 1
by XREAL_0:def 2;
then reconsider m1 =
m - 1 as
Element of
NAT ;
A252:
m = m1 + 1
;
(len c2) -' 1
= (len c2) - 1
by A250, A251, XREAL_0:def 2;
then reconsider lc21 =
(len c2) - 1 as
Element of
NAT ;
A253:
m + lc21 = m1 + (len c2)
;
A254:
m <= ((len c) + 1) + 1
by A5, A8, NAT_1:12;
A255:
(len c) + 1
<= len vs
by A2;
then A256:
(len ((m,((len c) + 1)) -cut vs)) + m = ((len c) + 1) + 1
by A4, A217, A254, Lm2;
then
len ((m,((len c) + 1)) -cut vs) = (((len c) - m) + 1) + 1
;
then A257:
1
<= len ((m,((len c) + 1)) -cut vs)
by A250, NAT_1:12;
A258:
len c2 = (len c) + ((- m) + 1)
by A250;
1
- 1
< m - 1
by A220, XREAL_1:9;
then
0 < - (- (m - 1))
;
then
- (m - 1) < 0
;
hence A259:
len c1 < len c
by A258, XREAL_1:30;
( 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 A2, A221, A222, Th13;
( 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 A223;
hence
len p1 < len vs
by A8, A259, XREAL_1:6;
( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )thus
vs . 1
= p1 . 1
by A4, A5, A6, A8, A217, FINSEQ_6:138;
( vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )thus
vs . (len vs) = p1 . (len p1)
by A4, A5, A8, A217, FINSEQ_6:138;
( Seq fc = c1 & Seq fvs = p1 )A260:
{ k where k is Nat : ( m <= k & k <= len c ) } c= Seg (len c)
then reconsider domfc =
{ k where k is Nat : ( m <= k & k <= len c ) } as
finite set by FINSET_1:1;
a260:
domfc is
included_in_Seg
by A260, FINSEQ_1:def 13;
(len c2) -' 1
= (len c2) - 1
by A250, A251, XREAL_0:def 2;
then reconsider lc21 =
(len c2) - 1 as
Element of
NAT ;
m + lc21 = len c
by A250;
then A264:
card domfc =
((len c2) + (- 1)) + 1
by FINSEQ_6:130
.=
len c2
;
A265:
len (Sgm domfc) = card domfc
by a260, FINSEQ_3:39;
A266:
rng (Sgm domfc) c= dom fc
by A224, FINSEQ_1:def 14;
set SR =
Sgm domfc;
now for p being object holds
( ( p in c2 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c2 ) )let p be
object ;
( ( p in c2 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c2 ) )hereby ( p in fc * (Sgm domfc) implies p in c2 )
assume A267:
p in c2
;
p in fc * (Sgm domfc)then consider x,
y being
object such that A268:
p = [x,y]
by RELAT_1:def 1;
A269:
x in dom c2
by A267, A268, FUNCT_1:1;
A270:
y = c2 . x
by A267, A268, FUNCT_1:1;
reconsider k =
x as
Element of
NAT by A269;
A271:
1
<= k
by A269, FINSEQ_3:25;
A272:
k <= len c2
by A269, FINSEQ_3:25;
A273:
x in dom (Sgm domfc)
by A264, A265, A269, FINSEQ_3:29;
A274:
m1 + k = (Sgm domfc) . k
by A250, A252, A253, A271, A272, FINSEQ_6:131;
A275:
(Sgm domfc) . k in rng (Sgm domfc)
by A273, FUNCT_1:def 3;
then A276:
x in dom (fc * (Sgm domfc))
by A266, A273, FUNCT_1:11;
0 + 1
<= k
by A269, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A277:
i < len c2
and A278:
k = i + 1
by A272, FINSEQ_6:127;
(fc * (Sgm domfc)) . x =
fc . (m1 + k)
by A274, A276, FUNCT_1:12
.=
c . (m + i)
by A266, A274, A275, A278, GRFUNC_1:2
.=
y
by A4, A5, A8, A217, A270, A277, A278, Lm2
;
hence
p in fc * (Sgm domfc)
by A268, A276, FUNCT_1:1;
verum
end; assume A279:
p in fc * (Sgm domfc)
;
p in c2then consider x,
y being
object such that A280:
p = [x,y]
by RELAT_1:def 1;
A281:
x in dom (fc * (Sgm domfc))
by A279, A280, FUNCT_1:1;
A282:
y = (fc * (Sgm domfc)) . x
by A279, A280, FUNCT_1:1;
A283:
x in dom (Sgm domfc)
by A281, FUNCT_1:11;
A284:
(Sgm domfc) . x in dom fc
by A281, FUNCT_1:11;
reconsider k =
x as
Element of
NAT by A283;
A285:
k in dom c2
by A264, A265, A283, FINSEQ_3:29;
A286:
1
<= k
by A283, FINSEQ_3:25;
A287:
k <= len c2
by A264, A265, A283, FINSEQ_3:25;
then A288:
m1 + k = (Sgm domfc) . k
by A250, A252, A253, A286, FINSEQ_6:131;
0 + 1
<= k
by A283, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A289:
i < len c2
and A290:
k = i + 1
by A287, FINSEQ_6:127;
c2 . k =
c . ((m1 + 1) + i)
by A4, A5, A8, A217, A289, A290, Lm2
.=
fc . ((Sgm domfc) . k)
by A284, A288, A290, GRFUNC_1:2
.=
y
by A282, A283, FUNCT_1:13
;
hence
p in c2
by A280, A285, FUNCT_1:1;
verum end; then
c2 = fc * (Sgm domfc)
by TARSKI:2;
hence
Seq fc = c1
by A224, FINSEQ_1:def 15;
Seq fvs = p1A291:
{ k where k is Nat : ( m <= k & k <= len vs ) } c= Seg (len vs)
then reconsider domfvs =
{ k where k is Nat : ( m <= k & k <= len vs ) } as
finite set by FINSET_1:1;
a291:
domfvs is
included_in_Seg
by A291, FINSEQ_1:def 13;
1
- 1
<= (len ((m,((len c) + 1)) -cut vs)) - 1
by A257, XREAL_1:9;
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 ;
A295:
m + lp21 = (len c) + 1
by A256;
A296:
m + lp21 = m1 + (len ((m,((len c) + 1)) -cut vs))
;
A297:
card domfvs =
((len ((m,((len c) + 1)) -cut vs)) + (- 1)) + 1
by A8, A295, FINSEQ_6:130
.=
len ((m,((len c) + 1)) -cut vs)
;
A298:
len (Sgm domfvs) = card domfvs
by a291, FINSEQ_3:39;
A299:
rng (Sgm domfvs) c= dom fvs
by A237, FINSEQ_1:def 14;
set SR =
Sgm domfvs;
now for p being object holds
( ( 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 ) )let p be
object ;
( ( 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 ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs )
assume A300:
p in (
m,
((len c) + 1))
-cut vs
;
p in fvs * (Sgm domfvs)then consider x,
y being
object such that A301:
p = [x,y]
by RELAT_1:def 1;
A302:
x in dom ((m,((len c) + 1)) -cut vs)
by A300, A301, FUNCT_1:1;
A303:
y = ((m,((len c) + 1)) -cut vs) . x
by A300, A301, FUNCT_1:1;
reconsider k =
x as
Element of
NAT by A302;
A304:
1
<= k
by A302, FINSEQ_3:25;
A305:
k <= len ((m,((len c) + 1)) -cut vs)
by A302, FINSEQ_3:25;
A306:
x in dom (Sgm domfvs)
by A297, A298, A302, FINSEQ_3:29;
A307:
m1 + k = (Sgm domfvs) . k
by A8, A252, A256, A296, A304, A305, FINSEQ_6:131;
A308:
(Sgm domfvs) . k in rng (Sgm domfvs)
by A306, FUNCT_1:def 3;
then A309:
x in dom (fvs * (Sgm domfvs))
by A299, A306, FUNCT_1:11;
0 + 1
<= k
by A302, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A310:
i < len ((m,((len c) + 1)) -cut vs)
and A311:
k = i + 1
by A305, FINSEQ_6:127;
(fvs * (Sgm domfvs)) . x =
fvs . (m1 + k)
by A307, A309, FUNCT_1:12
.=
vs . (m + i)
by A299, A307, A308, A311, GRFUNC_1:2
.=
y
by A4, A217, A254, A255, A303, A310, A311, Lm2
;
hence
p in fvs * (Sgm domfvs)
by A301, A309, FUNCT_1:1;
verum
end; assume A312:
p in fvs * (Sgm domfvs)
;
p in (m,((len c) + 1)) -cut vsthen consider x,
y being
object such that A313:
p = [x,y]
by RELAT_1:def 1;
A314:
x in dom (fvs * (Sgm domfvs))
by A312, A313, FUNCT_1:1;
A315:
y = (fvs * (Sgm domfvs)) . x
by A312, A313, FUNCT_1:1;
A316:
x in dom (Sgm domfvs)
by A314, FUNCT_1:11;
A317:
(Sgm domfvs) . x in dom fvs
by A314, FUNCT_1:11;
reconsider k =
x as
Element of
NAT by A316;
A318:
k in dom ((m,((len c) + 1)) -cut vs)
by A297, A298, A316, FINSEQ_3:29;
A319:
1
<= k
by A316, FINSEQ_3:25;
A320:
k <= len ((m,((len c) + 1)) -cut vs)
by A297, A298, A316, FINSEQ_3:25;
then A321:
m1 + k = (Sgm domfvs) . k
by A8, A252, A256, A296, A319, FINSEQ_6:131;
0 + 1
<= k
by A316, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A322:
i < len ((m,((len c) + 1)) -cut vs)
and A323:
k = i + 1
by A320, FINSEQ_6:127;
((m,((len c) + 1)) -cut vs) . k =
vs . ((m1 + 1) + i)
by A4, A217, A254, A255, A322, A323, Lm2
.=
fvs . ((Sgm domfvs) . k)
by A317, A321, A323, GRFUNC_1:2
.=
y
by A315, A316, FUNCT_1:13
;
hence
p in (
m,
((len c) + 1))
-cut vs
by A313, A318, FUNCT_1:1;
verum end; then
(
m,
((len c) + 1))
-cut vs = fvs * (Sgm domfvs)
by TARSKI:2;
hence
Seq fvs = p1
by A237, FINSEQ_1:def 15;
verum end; suppose A324:
(
n <> 1 &
m = len vs )
;
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 A3, XXREAL_0:1;
then
1
+ 1
<= n
by NAT_1:13;
then A325:
(1 + 1) - 1
<= n - 1
by XREAL_1:9;
n < len vs
by A4, A5, XXREAL_0:2;
then A326:
n - 1
< ((len c) + 1) - 1
by A8, XREAL_1:9;
A327:
1
<= n1 + 1
by NAT_1:12;
reconsider c1 = (1,
n1)
-cut c as
oriented Chain of
G by A11, A325, A326, Th12;
set pp = (1,
n)
-cut vs;
A328:
n <= len vs
by A4, A5, XXREAL_0:2;
A329:
(1,
n)
-cut vs is_oriented_vertex_seq_of c1
by A2, A12, A325, A326, Th13;
then A330:
len ((1,n) -cut vs) = (len c1) + 1
;
set domfc =
{ k where k is Nat : ( 1 <= k & k <= n1 ) } ;
deffunc H1(
object )
-> set =
c . $1;
consider fc being
Function such that A331:
dom fc = { k where k is Nat : ( 1 <= k & k <= n1 ) }
and A332:
for
x being
object st
x in { k where k is Nat : ( 1 <= k & k <= n1 ) } holds
fc . x = H1(
x)
from FUNCT_1:sch 3();
{ k where k is Nat : ( 1 <= k & k <= n1 ) } c= Seg (len c)
then reconsider fc =
fc as
FinSubsequence by A331, FINSEQ_1:def 12;
fc c= c
proof
let p be
object ;
TARSKI:def 3 ( not p in fc or p in c )
assume A336:
p in fc
;
p in c
then consider x,
y being
object such that A337:
[x,y] = p
by RELAT_1:def 1;
A338:
x in dom fc
by A336, A337, FUNCT_1:1;
A339:
y = fc . x
by A336, A337, FUNCT_1:1;
consider kk being
Nat such that A340:
x = kk
and A341:
1
<= kk
and A342:
kk <= n1
by A331, A338;
kk <= len c
by A11, A326, A342, XXREAL_0:2;
then A343:
x in dom c
by A340, A341, FINSEQ_3:25;
y = c . kk
by A331, A332, A338, A339, A340;
hence
p in c
by A337, A340, A343, FUNCT_1:1;
verum
end; then reconsider fc =
fc as
Subset of
c ;
take
fc
;
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 Nat : ( 1 <= k & k <= n ) } ;
deffunc H2(
object )
-> set =
vs . $1;
consider fvs being
Function such that A344:
dom fvs = { k where k is Nat : ( 1 <= k & k <= n ) }
and A345:
for
x being
object st
x in { k where k is Nat : ( 1 <= k & k <= n ) } holds
fvs . x = H2(
x)
from FUNCT_1:sch 3();
{ k where k is Nat : ( 1 <= k & k <= n ) } c= Seg (len vs)
then reconsider fvs =
fvs as
FinSubsequence by A344, FINSEQ_1:def 12;
fvs c= vs
proof
let p be
object ;
TARSKI:def 3 ( not p in fvs or p in vs )
assume A349:
p in fvs
;
p in vs
then consider x,
y being
object such that A350:
[x,y] = p
by RELAT_1:def 1;
A351:
x in dom fvs
by A349, A350, FUNCT_1:1;
A352:
y = fvs . x
by A349, A350, FUNCT_1:1;
consider kk being
Nat such that A353:
x = kk
and A354:
1
<= kk
and A355:
kk <= n
by A344, A351;
kk <= len vs
by A328, A355, XXREAL_0:2;
then A356:
x in dom vs
by A353, A354, FINSEQ_3:25;
y = vs . kk
by A344, A345, A351, A352, A353;
hence
p in vs
by A350, A353, A356, FUNCT_1:1;
verum
end; then reconsider fvs =
fvs as
Subset of
vs ;
take
fvs
;
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 c9 =
c1;
ex vs1 being FinSequence of the carrier of G st
( len c9 < len c & vs1 is_oriented_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 )take p1 = (1,
n)
-cut vs;
( len c9 < len c & p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )A357:
(len c1) + 1
= n1 + 1
by A11, A326, A327, Lm2;
then A358:
len c1 = n - 1
by A10, XREAL_0:def 2;
thus
len c9 < len c
by A10, A326, A357, XREAL_0:def 2;
( p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )thus
p1 is_oriented_vertex_seq_of c9
by A2, A12, A325, A326, Th13;
( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
len p1 = (len c1) + 1
by A329;
hence
len p1 < len vs
by A4, A5, A358, XXREAL_0:2;
( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )thus
vs . 1
= p1 . 1
by A3, A328, FINSEQ_6:138;
( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )thus
vs . (len vs) = p1 . (len p1)
by A3, A4, A6, A324, FINSEQ_6:138;
( Seq fc = c9 & Seq fvs = p1 )
{ k where k is Nat : ( 1 <= k & k <= n1 ) } c= Seg (len c)
then reconsider domfc =
{ k where k is Nat : ( 1 <= k & k <= n1 ) } as
finite set by FINSET_1:1;
domfc = Seg n1
by FINSEQ_1:def 1;
then A362:
Sgm domfc = idseq n1
by FINSEQ_3:48;
then A363:
dom (Sgm domfc) = Seg n1
;
set SL =
Sgm domfc;
now for p being object holds
( ( p in c1 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c1 ) )let p be
object ;
( ( p in c1 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c1 ) )hereby ( p in fc * (Sgm domfc) implies p in c1 )
assume A364:
p in c1
;
p in fc * (Sgm domfc)then consider x,
y being
object such that A365:
p = [x,y]
by RELAT_1:def 1;
A366:
x in dom c1
by A364, A365, FUNCT_1:1;
A367:
y = c1 . x
by A364, A365, FUNCT_1:1;
reconsider k =
x as
Element of
NAT by A366;
A368:
1
<= k
by A366, FINSEQ_3:25;
A369:
k <= len c1
by A366, FINSEQ_3:25;
then A370:
x in dom (Sgm domfc)
by A357, A363, A368, FINSEQ_1:1;
then A371:
k = (Sgm domfc) . k
by A362, FUNCT_1:18;
A372:
k in domfc
by A357, A368, A369;
then A373:
x in dom (fc * (Sgm domfc))
by A331, A370, A371, FUNCT_1:11;
0 + 1
<= k
by A366, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A374:
i < n1
and A375:
k = i + 1
by A357, A369, FINSEQ_6:127;
(fc * (Sgm domfc)) . x =
fc . k
by A371, A373, FUNCT_1:12
.=
c . (1 + i)
by A331, A372, A375, GRFUNC_1:2
.=
y
by A11, A326, A327, A357, A367, A374, A375, Lm2
;
hence
p in fc * (Sgm domfc)
by A365, A373, FUNCT_1:1;
verum
end; assume A376:
p in fc * (Sgm domfc)
;
p in c1then consider x,
y being
object such that A377:
p = [x,y]
by RELAT_1:def 1;
A378:
x in dom (fc * (Sgm domfc))
by A376, A377, FUNCT_1:1;
A379:
y = (fc * (Sgm domfc)) . x
by A376, A377, FUNCT_1:1;
A380:
(fc * (Sgm domfc)) . x = fc . ((Sgm domfc) . x)
by A378, FUNCT_1:12;
A381:
x in dom (Sgm domfc)
by A378, FUNCT_1:11;
then
x in { kk where kk is Nat : ( 1 <= kk & kk <= n1 ) }
by A363, FINSEQ_1:def 1;
then consider k being
Nat such that A382:
k = x
and A383:
1
<= k
and A384:
k <= n1
;
A385:
k in dom fc
by A331, A383, A384;
A386:
k = (Sgm domfc) . k
by A362, A381, A382, FUNCT_1:18;
A387:
k in dom c1
by A357, A383, A384, FINSEQ_3:25;
0 + 1
<= k
by A383;
then
ex
i being
Nat st
(
0 <= i &
i < n1 &
k = i + 1 )
by A384, FINSEQ_6:127;
then c1 . k =
c . k
by A11, A326, A327, A357, Lm2
.=
y
by A379, A380, A382, A385, A386, GRFUNC_1:2
;
hence
p in c1
by A377, A382, A387, FUNCT_1:1;
verum end; then
c1 = fc * (Sgm domfc)
by TARSKI:2;
hence
Seq fc = c9
by A331, FINSEQ_1:def 15;
Seq fvs = p1
{ k where k is Nat : ( 1 <= k & k <= n ) } c= Seg (len vs)
then reconsider domfvs =
{ k where k is Nat : ( 1 <= k & k <= n ) } as
finite set by FINSET_1:1;
domfvs = Seg n
by FINSEQ_1:def 1;
then A391:
Sgm domfvs = idseq n
by FINSEQ_3:48;
then A392:
dom (Sgm domfvs) = Seg n
;
set SL =
Sgm domfvs;
now for p being object holds
( ( p in (1,n) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs ) )let p be
object ;
( ( 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 ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs )
assume A393:
p in (1,
n)
-cut vs
;
p in fvs * (Sgm domfvs)then consider x,
y being
object such that A394:
p = [x,y]
by RELAT_1:def 1;
A395:
x in dom ((1,n) -cut vs)
by A393, A394, FUNCT_1:1;
A396:
y = ((1,n) -cut vs) . x
by A393, A394, FUNCT_1:1;
reconsider k =
x as
Element of
NAT by A395;
A397:
1
<= k
by A395, FINSEQ_3:25;
A398:
k <= len ((1,n) -cut vs)
by A395, FINSEQ_3:25;
then A399:
x in dom (Sgm domfvs)
by A330, A358, A392, A397, FINSEQ_1:1;
then A400:
k = (Sgm domfvs) . k
by A391, FUNCT_1:18;
A401:
k in domfvs
by A330, A358, A397, A398;
then A402:
x in dom (fvs * (Sgm domfvs))
by A344, A399, A400, FUNCT_1:11;
0 + 1
<= k
by A395, FINSEQ_3:25;
then consider i being
Nat such that
0 <= i
and A403:
i < n
and A404:
k = i + 1
by A330, A358, A398, FINSEQ_6:127;
(fvs * (Sgm domfvs)) . x =
fvs . k
by A400, A402, FUNCT_1:12
.=
vs . (1 + i)
by A344, A401, A404, GRFUNC_1:2
.=
y
by A3, A328, A330, A358, A396, A403, A404, FINSEQ_6:def 4
;
hence
p in fvs * (Sgm domfvs)
by A394, A402, FUNCT_1:1;
verum
end; assume A405:
p in fvs * (Sgm domfvs)
;
p in (1,n) -cut vsthen consider x,
y being
object such that A406:
p = [x,y]
by RELAT_1:def 1;
A407:
x in dom (fvs * (Sgm domfvs))
by A405, A406, FUNCT_1:1;
A408:
y = (fvs * (Sgm domfvs)) . x
by A405, A406, FUNCT_1:1;
A409:
(fvs * (Sgm domfvs)) . x = fvs . ((Sgm domfvs) . x)
by A407, FUNCT_1:12;
A410:
x in dom (Sgm domfvs)
by A407, FUNCT_1:11;
then
x in { kk where kk is Nat : ( 1 <= kk & kk <= n ) }
by A392, FINSEQ_1:def 1;
then consider k being
Nat such that A411:
k = x
and A412:
1
<= k
and A413:
k <= n
;
A414:
k in dom fvs
by A344, A412, A413;
A415:
k = (Sgm domfvs) . k
by A391, A410, A411, FUNCT_1:18;
A416:
k in dom ((1,n) -cut vs)
by A330, A358, A412, A413, FINSEQ_3:25;
0 + 1
<= k
by A412;
then
ex
i being
Nat st
(
0 <= i &
i < n &
k = i + 1 )
by A413, FINSEQ_6:127;
then ((1,n) -cut vs) . k =
vs . k
by A3, A328, A330, A358, FINSEQ_6:def 4
.=
y
by A408, A409, A411, A414, A415, GRFUNC_1:2
;
hence
p in (1,
n)
-cut vs
by A406, A411, A416, FUNCT_1:1;
verum end; then
(1,
n)
-cut vs = fvs * (Sgm domfvs)
by TARSKI:2;
hence
Seq fvs = p1
by A344, FINSEQ_1:def 15;
verum end;