let G be finite Graph; for v being Vertex of G
for c being Chain of G
for vs being FinSequence of the carrier of G st not c is empty & vs is_vertex_seq_of c holds
( v in rng vs iff Degree (v,(rng c)) <> 0 )
let v be Vertex of G; for c being Chain of G
for vs being FinSequence of the carrier of G st not c is empty & vs is_vertex_seq_of c holds
( v in rng vs iff Degree (v,(rng c)) <> 0 )
let c be Chain of G; for vs being FinSequence of the carrier of G st not c is empty & vs is_vertex_seq_of c holds
( v in rng vs iff Degree (v,(rng c)) <> 0 )
let vs be FinSequence of the carrier of G; ( not c is empty & vs is_vertex_seq_of c implies ( v in rng vs iff Degree (v,(rng c)) <> 0 ) )
assume that
A1:
not c is empty
and
A2:
vs is_vertex_seq_of c
; ( v in rng vs iff Degree (v,(rng c)) <> 0 )
hereby ( Degree (v,(rng c)) <> 0 implies v in rng vs )
c is
FinSequence of the
carrier' of
G
by MSSCYC_1:def 1;
then A3:
rng c c= the
carrier' of
G
by FINSEQ_1:def 4;
assume that A4:
v in rng vs
and A5:
Degree (
v,
(rng c))
= 0
;
contradictionA6:
(
Edges_In (
v,
(rng c))
= {} &
Edges_Out (
v,
(rng c))
= {} )
by A5;
A7:
0 + 1
<= len c
by A1, NAT_1:13;
A8:
len vs = (len c) + 1
by A2;
consider i being
Nat such that A9:
i in dom vs
and A10:
vs . i = v
by A4, FINSEQ_2:10;
A11:
1
<= i
by A9, FINSEQ_3:25;
A12:
i <= len vs
by A9, FINSEQ_3:25;
per cases
( i = len vs or i < len vs )
by A12, XXREAL_0:1;
suppose
i < len vs
;
contradictionthen A15:
i <= len c
by A8, NAT_1:13;
then
i in dom c
by A11, FINSEQ_3:25;
then A16:
c . i in rng c
by FUNCT_1:def 3;
(
vs . i = the
Target of
G . (c . i) or
vs . i = the
Source of
G . (c . i) )
by A2, A11, A15, Lm3;
hence
contradiction
by A6, A10, A3, A16, Def1, Def2;
verum end;
end;
assume that
A17:
Degree (v,(rng c)) <> 0
and
A18:
not v in rng vs
; contradiction
per cases
( card (Edges_In (v,(rng c))) <> 0 or card (Edges_Out (v,(rng c))) <> 0 )
by A17;
suppose
card (Edges_In (v,(rng c))) <> 0
;
contradictionthen consider e being
object such that A19:
e in Edges_In (
v,
(rng c))
by CARD_1:27, XBOOLE_0:def 1;
A20:
the
Target of
G . e = v
by A19, Def1;
e in rng c
by A19, Def1;
then consider i being
Nat such that A21:
i in dom c
and A22:
c . i = e
by FINSEQ_2:10;
A23:
1
<= i
by A21, FINSEQ_3:25;
A24:
i <= len c
by A21, FINSEQ_3:25;
then
( 1
<= i + 1 &
i + 1
<= len vs )
by A2, A23, Lm3;
then A25:
i + 1
in dom vs
by FINSEQ_3:25;
i <= len vs
by A2, A23, A24, Lm3;
then A26:
i in dom vs
by A23, FINSEQ_3:25;
( (
vs . i = the
Target of
G . (c . i) &
vs . (i + 1) = the
Source of
G . (c . i) ) or (
vs . i = the
Source of
G . (c . i) &
vs . (i + 1) = the
Target of
G . (c . i) ) )
by A2, A23, A24, Lm3;
hence
contradiction
by A18, A20, A22, A26, A25, FUNCT_1:def 3;
verum end; suppose
card (Edges_Out (v,(rng c))) <> 0
;
contradictionthen consider e being
object such that A27:
e in Edges_Out (
v,
(rng c))
by CARD_1:27, XBOOLE_0:def 1;
A28:
the
Source of
G . e = v
by A27, Def2;
e in rng c
by A27, Def2;
then consider i being
Nat such that A29:
i in dom c
and A30:
c . i = e
by FINSEQ_2:10;
A31:
1
<= i
by A29, FINSEQ_3:25;
A32:
i <= len c
by A29, FINSEQ_3:25;
then
( 1
<= i + 1 &
i + 1
<= len vs )
by A2, A31, Lm3;
then A33:
i + 1
in dom vs
by FINSEQ_3:25;
i <= len vs
by A2, A31, A32, Lm3;
then A34:
i in dom vs
by A31, FINSEQ_3:25;
( (
vs . i = the
Target of
G . (c . i) &
vs . (i + 1) = the
Source of
G . (c . i) ) or (
vs . i = the
Source of
G . (c . i) &
vs . (i + 1) = the
Target of
G . (c . i) ) )
by A2, A31, A32, Lm3;
hence
contradiction
by A18, A28, A30, A34, A33, FUNCT_1:def 3;
verum end;