let G be finite Graph; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( v in rng vs iff Degree (v,(rng c)) <> 0 )

hereby :: thesis: ( 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 ; :: thesis: contradiction
A6: ( 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 A13: i = len vs ; :: thesis: contradiction

set ic = len c;
len c in dom c by A7, FINSEQ_3:25;
then A14: c . (len c) in rng c by FUNCT_1:def 3;
( vs . (len vs) = the Target of G . (c . (len c)) or vs . (len vs) = the Source of G . (c . (len c)) ) by A2, A7, Lm3;
hence contradiction by A6, A10, A3, A13, A14, Def1, Def2; :: thesis: verum

end;

suppose i < len vs ; :: thesis: contradiction

then 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; :: thesis: verum

end;

end;

end;

assume that
A17: Degree (v,(rng c)) <> 0 and
A18: not v in rng vs ; :: thesis: 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 ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose card (Edges_Out (v,(rng c))) <> 0 ; :: thesis: contradiction

then 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; :: thesis: verum

end;

end;