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