let G be Graph; :: thesis: ( G is connected iff for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )
set E = the carrier' of G;
set S = the Source of G;
set T = the Target of G;
thus
( G is connected implies for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )
:: thesis: ( ( for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) ) implies G is connected )proof
assume A1:
G is
connected
;
:: thesis: for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 )
let v1,
v2 be
Vertex of
G;
:: thesis: ( v1 <> v2 implies ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )
assume A2:
v1 <> v2
;
:: thesis: ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 )
assume A3:
for
c being
Chain of
G for
vs being
FinSequence of the
carrier of
G holds
(
c is
empty or not
vs is_vertex_seq_of c or not
vs . 1
= v1 or not
vs . (len vs) = v2 )
;
:: thesis: contradiction
reconsider V = the
carrier of
G as non
empty set ;
set V1 =
{ v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) } ;
set V2 =
V \ { v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) } ;
v1 in { v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) }
;
then reconsider V1 =
{ v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) } as non
empty set ;
defpred S1[
set ]
means ( $1
= v1 or ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = $1 ) );
A4:
{ v where v is Element of V : S1[v] } is
Subset of
V
from DOMAIN_1:sch 7();
then reconsider V2 =
V \ { v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) } as non
empty set by XBOOLE_0:def 5;
defpred S2[
set ]
means ( the
Source of
G . $1
in V1 & the
Target of
G . $1
in V1 );
consider E1 being
set such that A6:
for
e being
set holds
(
e in E1 iff (
e in the
carrier' of
G &
S2[
e] ) )
from XBOOLE_0:sch 1();
set E2 = the
carrier' of
G \ E1;
A7:
E1 c= the
carrier' of
G
A8:
dom the
Source of
G = the
carrier' of
G
by FUNCT_2:def 1;
A9:
dom the
Target of
G = the
carrier' of
G
by FUNCT_2:def 1;
A10:
rng the
Source of
G c= V
by RELAT_1:def 19;
A11:
rng the
Target of
G c= V
by RELAT_1:def 19;
A12:
dom (the Source of G | E1) =
(dom the Source of G) /\ E1
by RELAT_1:90
.=
the
carrier' of
G /\ E1
by FUNCT_2:def 1
.=
E1
by A7, XBOOLE_1:28
;
rng (the Source of G | E1) c= V1
then reconsider S1 = the
Source of
G | E1 as
Function of
E1,
V1 by A12, FUNCT_2:def 1, RELSET_1:11;
A14:
dom (the Target of G | E1) =
(dom the Target of G) /\ E1
by RELAT_1:90
.=
the
carrier' of
G /\ E1
by FUNCT_2:def 1
.=
E1
by A7, XBOOLE_1:28
;
rng (the Target of G | E1) c= V1
then reconsider T1 = the
Target of
G | E1 as
Function of
E1,
V1 by A14, FUNCT_2:def 1, RELSET_1:11;
A16:
dom (the Source of G | (the carrier' of G \ E1)) =
(dom the Source of G) /\ (the carrier' of G \ E1)
by RELAT_1:90
.=
the
carrier' of
G \ E1
by A8, XBOOLE_1:28
;
rng (the Source of G | (the carrier' of G \ E1)) c= V2
proof
let v be
set ;
:: according to TARSKI:def 3 :: thesis: ( not v in rng (the Source of G | (the carrier' of G \ E1)) or v in V2 )
assume
v in rng (the Source of G | (the carrier' of G \ E1))
;
:: thesis: v in V2
then consider e being
set such that A17:
(
e in dom (the Source of G | (the carrier' of G \ E1)) &
(the Source of G | (the carrier' of G \ E1)) . e = v )
by FUNCT_1:def 5;
reconsider e =
e as
Element of the
carrier' of
G by A16, A17;
A18:
(the Source of G | (the carrier' of G \ E1)) . e = the
Source of
G . e
by A17, FUNCT_1:70;
A19:
not
e in E1
by A16, A17, XBOOLE_0:def 5;
per cases
( not e in the carrier' of G or not the Source of G . e in V1 or not the Target of G . e in V1 )
by A6, A19;
suppose A21:
not the
Target of
G . e in V1
;
:: thesis: v in V2reconsider Te = the
Target of
G . e as
Vertex of
G by A16, A17, FUNCT_2:7;
A22:
v in rng (the Source of G | (the carrier' of G \ E1))
by A17, FUNCT_1:def 5;
rng (the Source of G | (the carrier' of G \ E1)) c= rng the
Source of
G
by RELAT_1:99;
then A23:
v in rng the
Source of
G
by A22;
assume
not
v in V2
;
:: thesis: contradictionthen
v in V1
by A10, A23, XBOOLE_0:def 5;
then consider v' being
Vertex of
G such that A24:
(
v' = v & (
v' = v1 or ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v' ) ) )
;
thus
contradiction
:: thesis: verumproof
per cases
( v' = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v' ) )
by A24;
suppose
ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v' )
;
:: thesis: contradictionthen consider c being
Chain of
G,
vs being
FinSequence of the
carrier of
G such that A27:
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v' )
;
reconsider c' =
c ^ <*e*> as
Chain of
G by A16, A17, A18, A24, A27, Th17;
ex
vs' being
FinSequence of the
carrier of
G st
(
vs' = vs ^' <*(the Source of G . e),(the Target of G . e)*> &
vs' is_vertex_seq_of c' &
vs' . 1
= vs . 1 &
vs' . (len vs') = Te )
by A16, A17, A18, A24, A27, Th17;
hence
contradiction
by A21, A27;
:: thesis: verum end;
end; end;
end;
then reconsider S2 = the
Source of
G | (the carrier' of G \ E1) as
Function of
(the carrier' of G \ E1),
V2 by A16, FUNCT_2:def 1, RELSET_1:11;
A28:
dom (the Target of G | (the carrier' of G \ E1)) =
(dom the Target of G) /\ (the carrier' of G \ E1)
by RELAT_1:90
.=
the
carrier' of
G \ E1
by A9, XBOOLE_1:28
;
rng (the Target of G | (the carrier' of G \ E1)) c= V2
proof
let v be
set ;
:: according to TARSKI:def 3 :: thesis: ( not v in rng (the Target of G | (the carrier' of G \ E1)) or v in V2 )
assume
v in rng (the Target of G | (the carrier' of G \ E1))
;
:: thesis: v in V2
then consider e being
set such that A29:
(
e in dom (the Target of G | (the carrier' of G \ E1)) &
(the Target of G | (the carrier' of G \ E1)) . e = v )
by FUNCT_1:def 5;
reconsider e =
e as
Element of the
carrier' of
G by A28, A29;
A30:
(the Target of G | (the carrier' of G \ E1)) . e = the
Target of
G . e
by A29, FUNCT_1:70;
A31:
not
e in E1
by A28, A29, XBOOLE_0:def 5;
per cases
( not e in the carrier' of G or not the Target of G . e in V1 or not the Source of G . e in V1 )
by A6, A31;
suppose A33:
not the
Source of
G . e in V1
;
:: thesis: v in V2reconsider Se = the
Source of
G . e as
Vertex of
G by A28, A29, FUNCT_2:7;
A34:
v in rng (the Target of G | (the carrier' of G \ E1))
by A29, FUNCT_1:def 5;
rng (the Target of G | (the carrier' of G \ E1)) c= rng the
Target of
G
by RELAT_1:99;
then A35:
v in rng the
Target of
G
by A34;
assume
not
v in V2
;
:: thesis: contradictionthen
v in V1
by A11, A35, XBOOLE_0:def 5;
then consider v' being
Vertex of
G such that A36:
(
v' = v & (
v' = v1 or ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v' ) ) )
;
thus
contradiction
:: thesis: verumproof
per cases
( v' = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v' ) )
by A36;
suppose
ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v' )
;
:: thesis: contradictionthen consider c being
Chain of
G,
vs being
FinSequence of the
carrier of
G such that A39:
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v' )
;
reconsider c' =
c ^ <*e*> as
Chain of
G by A28, A29, A30, A36, A39, Th18;
ex
vs' being
FinSequence of the
carrier of
G st
(
vs' = vs ^' <*(the Target of G . e),(the Source of G . e)*> &
vs' is_vertex_seq_of c' &
vs' . 1
= vs . 1 &
vs' . (len vs') = Se )
by A28, A29, A30, A36, A39, Th18;
hence
contradiction
by A33, A39;
:: thesis: verum end;
end; end;
end;
then reconsider T2 = the
Target of
G | (the carrier' of G \ E1) as
Function of
(the carrier' of G \ E1),
V2 by A28, FUNCT_2:def 1, RELSET_1:11;
reconsider G1 =
MultiGraphStruct(#
V1,
E1,
S1,
T1 #),
G2 =
MultiGraphStruct(#
V2,
(the carrier' of G \ E1),
S2,
T2 #) as
Graph ;
A40:
V1 misses V2
by XBOOLE_1:79;
G is_sum_of G1,
G2
proof
thus A41:
the
Target of
G1 tolerates the
Target of
G2
:: according to GRAPH_1:def 4 :: thesis: ( the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G,the carrier' of G,the Source of G,the Target of G #) = G1 \/ G2 )
thus A42:
the
Source of
G1 tolerates the
Source of
G2
:: thesis: MultiGraphStruct(# the carrier of G,the carrier' of G,the Source of G,the Target of G #) = G1 \/ G2
reconsider MG =
MultiGraphStruct(# the
carrier of
G,the
carrier' of
G,the
Source of
G,the
Target of
G #) as
strict Graph ;
A43:
the
carrier of
MG = the
carrier of
G1 \/ the
carrier of
G2
by A4, XBOOLE_1:45;
A44:
the
carrier' of
MG = the
carrier' of
G1 \/ the
carrier' of
G2
by A7, XBOOLE_1:45;
A45:
for
v being
set st
v in the
carrier' of
G1 holds
( the
Source of
MG . v = the
Source of
G1 . v & the
Target of
MG . v = the
Target of
G1 . v )
by FUNCT_1:72;
for
v being
set st
v in the
carrier' of
G2 holds
( the
Source of
MG . v = the
Source of
G2 . v & the
Target of
MG . v = the
Target of
G2 . v )
by FUNCT_1:72;
hence
MultiGraphStruct(# the
carrier of
G,the
carrier' of
G,the
Source of
G,the
Target of
G #)
= G1 \/ G2
by A41, A42, A43, A44, A45, GRAPH_1:def 3;
:: thesis: verum
end;
hence
contradiction
by A1, A40, GRAPH_1:def 8;
:: thesis: verum
end;
assume A46:
for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 )
; :: thesis: G is connected
thus
G is connected
:: thesis: verumproof
given G1,
G2 being
Graph such that A47:
the
carrier of
G1 misses the
carrier of
G2
and A48:
G is_sum_of G1,
G2
;
:: according to GRAPH_1:def 8 :: thesis: contradiction
A49:
the
carrier of
G1 /\ the
carrier of
G2 = {}
by A47, XBOOLE_0:def 7;
set V1 = the
carrier of
G1;
set V2 = the
carrier of
G2;
set E1 = the
carrier' of
G1;
set S1 = the
Source of
G1;
set S2 = the
Source of
G2;
set T1 = the
Target of
G1;
set T2 = the
Target of
G2;
A50:
( the
Target of
G1 tolerates the
Target of
G2 & the
Source of
G1 tolerates the
Source of
G2 &
MultiGraphStruct(# the
carrier of
G,the
carrier' of
G,the
Source of
G,the
Target of
G #)
= G1 \/ G2 )
by A48, GRAPH_1:def 4;
then A51:
( the
carrier of
MultiGraphStruct(# the
carrier of
G,the
carrier' of
G,the
Source of
G,the
Target of
G #)
= the
carrier of
G1 \/ the
carrier of
G2 & the
carrier' of
G = the
carrier' of
G1 \/ the
carrier' of
G2 & ( for
e being
set st
e in the
carrier' of
G1 holds
( the
Source of
G . e = the
Source of
G1 . e & the
Target of
G . e = the
Target of
G1 . e ) ) & ( for
e being
set st
e in the
carrier' of
G2 holds
( the
Source of
G . e = the
Source of
G2 . e & the
Target of
G . e = the
Target of
G2 . e ) ) )
by GRAPH_1:def 3;
consider v1 being
Vertex of
G1;
consider v2 being
Vertex of
G2;
reconsider v1' =
v1,
v2' =
v2 as
Vertex of
G by A51, XBOOLE_0:def 3;
v1 <> v2
by A49, XBOOLE_0:def 4;
then consider c being
Chain of
G,
vs being
FinSequence of the
carrier of
G such that A52:
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1' &
vs . (len vs) = v2' )
by A46;
A53:
len vs = (len c) + 1
by A52, GRAPH_2:def 7;
defpred S1[
Nat]
means ( $1
in dom vs &
vs . $1 is
Vertex of
G2 );
1
<= (len c) + 1
by NAT_1:11;
then
len vs in dom vs
by A53, FINSEQ_3:27;
then A54:
ex
k being
Nat st
S1[
k]
by A52;
consider k being
Nat such that A55:
S1[
k]
and A56:
for
n being
Nat st
S1[
n] holds
k <= n
from NAT_1:sch 5(A54);
A57:
1
<= k
by A55, FINSEQ_3:27;
k <> 1
by A49, A52, A55, XBOOLE_0:def 4;
then
1
< k
by A57, XXREAL_0:1;
then
1
+ 1
<= k
by NAT_1:13;
then consider i being
Element of
NAT such that A58:
( 1
<= i &
i < k &
k = i + 1 )
by GRAPH_2:1;
A59:
k <= len vs
by A55, FINSEQ_3:27;
then
i <= len vs
by A58, XXREAL_0:2;
then A60:
i in dom vs
by A58, FINSEQ_3:27;
set e =
c . i;
c is
FinSequence of the
carrier' of
G
by MSSCYC_1:def 1;
then A61:
rng c c= the
carrier' of
G
by FINSEQ_1:def 4;
A62:
i <= len c
by A53, A58, A59, XREAL_1:8;
then
i in dom c
by A58, FINSEQ_3:27;
then A63:
c . i in rng c
by FUNCT_1:def 5;
end;