let G be finite Graph; :: thesis:
let c be cyclic Path of G; :: thesis:
let vs be FinSequence of the carrier of G; :: thesis:
let v be Vertex of G; :: thesis:
assume that
A1: vs is_vertex_seq_of c and
A2: v in rng vs ; :: thesis:
set S = the Source of G;
set T = the Target of G;

then reconsider rc = rng c as empty set ;
Degree (v,rc) = 2 * 0 ;
hence Degree (v,(rng c)) is even ; :: thesis:

end;

suppose A3: not c is empty ; :: thesis:

set ev = { n where n is Element of NAT : ( 1 <= n & n <= len c & vs . n = v ) } ;
A4: { n where n is Element of NAT : ( 1 <= n & n <= len c & vs . n = v ) } c= Seg (len c)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { n where n is Element of NAT : ( 1 <= n & n <= len c & vs . n = v ) } ; :: thesis:
then ex n being Element of NAT st
( x = n & 1 <= n & n <= len c & vs . n = v ) ;
hence x in Seg (len c) by FINSEQ_1:1; :: thesis:

end;

reconsider rc = rng c as non empty set by A3;
A5: len vs = (len c) + 1 by A1;
set evout = [:{1},(Edges_Out (v,rc)):];
set evin = [:{0},(Edges_In (v,rc)):];
A6: card [:{1},(Edges_Out (v,rc)):] = (card {1}) * (card (Edges_Out (v,rc))) by CARD_2:46
.= 1 * (card (Edges_Out (v,rc))) by CARD_1:30
.= card (Edges_Out (v,rc)) ;
A7: card [:{0},(Edges_In (v,rc)):] = (card {0}) * (card (Edges_In (v,rc))) by CARD_2:46
.= 1 * (card (Edges_In (v,rc))) by CARD_1:30
.= card (Edges_In (v,rc)) ;

now :: thesis:

assume A8: [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] is empty ; :: thesis:
then [:{0},(Edges_In (v,rc)):] is empty ;
then Degree (v,rc) = 0 + 0 by A7, A6, A8;
hence contradiction by A1, A2, A3, Th32; :: thesis:

end;

then reconsider evio = [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] as non empty set ;
A9: [:{0},(Edges_In (v,rc)):] misses [:{1},(Edges_Out (v,rc)):]

proof

assume not [:{0},(Edges_In (v,rc)):] misses [:{1},(Edges_Out (v,rc)):] ; :: thesis:
then consider x being object such that
A10: x in [:{0},(Edges_In (v,rc)):] /\ [:{1},(Edges_Out (v,rc)):] by XBOOLE_0:4;
x in [:{1},(Edges_Out (v,rc)):] by A10, XBOOLE_0:def 4;
then consider x21, x22 being object such that
A11: x21 in {1} and
x22 in Edges_Out (v,rc) and
A12: x = [x21,x22] by ZFMISC_1:def 2;
A13: x21 = 1 by A11, TARSKI:def 1;
x in [:{0},(Edges_In (v,rc)):] by A10, XBOOLE_0:def 4;
then consider x11, x12 being object such that
A14: x11 in {0} and
x12 in Edges_In (v,rc) and
A15: x = [x11,x12] by ZFMISC_1:def 2;
x11 = 0 by A14, TARSKI:def 1;
hence contradiction by A15, A12, A13, XTUPLE_0:1; :: thesis:

end;

reconsider ev = { n where n is Element of NAT : ( 1 <= n & n <= len c & vs . n = v ) } as Subset of (Seg (len c)) by A4;
A16: rc c= the carrier' of G by FINSEQ_1:def 4;
then reconsider G9 = G as non void finite Graph ;
reconsider vs9 = vs as FinSequence of the carrier of G9 ;
A17: vs9 . 1 = vs . (len vs) by A1, MSSCYC_1:6;

now :: thesis:

A18: 0 + 1 <= len c by A3, NAT_1:13;
consider n being object such that
A19: n in dom vs and
A20: vs . n = v by A2, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A19;
A21: n <= len vs by A19, FINSEQ_3:25;
A22: 1 <= n by A19, FINSEQ_3:25;
thus not ev is empty :: thesis:

proof

per cases by A21, XXREAL_0:1;

suppose n = len vs ; :: thesis:

then 1 in ev by A17, A20, A18;
hence not ev is empty ; :: thesis:

end;

suppose n < len vs ; :: thesis:

then n <= len c by A5, NAT_1:13;
then n in ev by A20, A22;
hence not ev is empty ; :: thesis:

end;

then reconsider ev = ev as non empty finite set ;
set ev92 = [:2,ev:];

now :: thesis:

defpred S₁[ Element of [:2,ev:], Element of evio, Element of NAT ] means ( $1 = [1,$3] & ( ( vs . $3 = the Source of G . (c . $3) & $2 = [1,(c . $3)] ) or ( vs . $3 = the Target of G . (c . $3) & $2 = [0,(c . $3)] & the Target of G . (c . $3) <> the Source of G . (c . $3) ) ) );
defpred S₂[ Element of [:2,ev:], Element of evio, Element of NAT ] means ( $1 = [0,$3] & ( ex k being Element of NAT st
( 1 <= k & $3 = k + 1 & ( ( vs . $3 = the Target of G . (c . k) & $2 = [0,(c . k)] ) or ( vs . $3 = the Source of G . (c . k) & $2 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) or ( $3 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & $2 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & $2 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ) );
take Z = { [x,y] where x is Element of [:2,ev:], y is Element of evio : ex n being Element of NAT st
( 1 <= n & n <= len c & ( S₂[x,y,n] or S₁[x,y,n] ) ) } ; :: thesis:
thus for x being object st x in [:2,ev:] holds
ex y being object st
( y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] & [x,y] in Z ) :: thesis:

proof

A23: 1 in {1} by TARSKI:def 1;
let x be object ; :: thesis:
A24: 0 in {0} by TARSKI:def 1;
assume A25: x in [:2,ev:] ; :: thesis:
then consider u, w being object such that
A26: [u,w] = x by RELAT_1:def 1;
reconsider x9 = x as Element of [:2,ev:] by A25;
A27: u in 2 by A25, A26, ZFMISC_1:87;
w in ev by A25, A26, ZFMISC_1:87;
then consider n being Element of NAT such that
A28: w = n and
A29: 1 <= n and
A30: n <= len c and
A31: vs . n = v ;

per cases by A27, CARD_1:50, TARSKI:def 2;

suppose A32: u = 0 ; :: thesis:

thus ex y being object st
( y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] & [x,y] in Z ) :: thesis:

proof

per cases by A29, XXREAL_0:1;

suppose 1 < n ; :: thesis:

then consider k being Element of NAT such that
A33: n = 1 + k and
A34: 1 <= k by FINSEQ_4:84;
k <= n by A33, NAT_1:11;
then A35: k <= len c by A30, XXREAL_0:2;
then k in dom c by A34, FINSEQ_3:25;
then reconsider e = c . k as Element of rc by FUNCT_1:def 3;
A36: e in rc ;
thus ex y being object st
( y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A34, A35, Lm3;

suppose A37: the Target of G . (c . k) = vs . (k + 1) ; :: thesis:

take y = [0,(c . k)]; :: thesis:
e in Edges_In (v,rc) by A16, A31, A33, A36, A37, Def1;
then A38: y in [:{0},(Edges_In (v,rc)):] by A24, ZFMISC_1:87;
hence y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] by XBOOLE_0:def 3; :: thesis:
reconsider y9 = y as Element of evio by A38, XBOOLE_0:def 3;
S₂[x9,y9,n] by A26, A28, A32, A33, A34, A37;
hence [x,y] in Z by A29, A30; :: thesis:

end;

suppose A39: ( the Source of G . (c . k) = vs . (k + 1) & the Target of G . (c . k) <> the Source of G . (c . k) ) ; :: thesis:

take y = [1,(c . k)]; :: thesis:
e in Edges_Out (v,rc) by A16, A31, A33, A36, A39, Def2;
then A40: y in [:{1},(Edges_Out (v,rc)):] by A23, ZFMISC_1:87;
hence y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] by XBOOLE_0:def 3; :: thesis:
reconsider y9 = y as Element of evio by A40, XBOOLE_0:def 3;
S₂[x9,y9,n] by A26, A28, A32, A33, A34, A39;
hence [x,y] in Z by A29, A30; :: thesis:

end;

suppose A41: n = 1 ; :: thesis:

A42: 1 <= len c by A29, A30, XXREAL_0:2;
then len c in dom c by FINSEQ_3:25;
then reconsider e = c . (len c) as Element of rc by FUNCT_1:def 3;
A43: 1 <= len c by A29, A30, XXREAL_0:2;
A44: ( e in rc & vs . 1 = vs . ((len c) + 1) ) by A1, MSSCYC_1:6;
thus ex y being object st
( y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A42, Lm3;

suppose A45: the Target of G . (c . (len c)) = vs . ((len c) + 1) ; :: thesis:

take y = [0,(c . (len c))]; :: thesis:
e in Edges_In (v,rc) by A16, A31, A41, A44, A45, Def1;
then A46: y in [:{0},(Edges_In (v,rc)):] by A24, ZFMISC_1:87;
hence y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] by XBOOLE_0:def 3; :: thesis:
reconsider y9 = y as Element of evio by A46, XBOOLE_0:def 3;
S₂[x9,y9,1] by A1, A26, A28, A32, A41, A45, MSSCYC_1:6;
hence [x,y] in Z by A43; :: thesis:

end;

suppose A47: ( the Source of G . (c . (len c)) = vs . ((len c) + 1) & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ; :: thesis:

take y = [1,(c . (len c))]; :: thesis:
e in Edges_Out (v,rc) by A16, A31, A41, A44, A47, Def2;
then A48: y in [:{1},(Edges_Out (v,rc)):] by A23, ZFMISC_1:87;
hence y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] by XBOOLE_0:def 3; :: thesis:
reconsider y9 = y as Element of evio by A48, XBOOLE_0:def 3;
S₂[x9,y9,1] by A1, A26, A28, A32, A41, A47, MSSCYC_1:6;
hence [x,y] in Z by A43; :: thesis:

end;

suppose A49: u = 1 ; :: thesis:

n in dom c by A29, A30, FINSEQ_3:25;
then reconsider e = c . n as Element of rc by FUNCT_1:def 3;
A50: e in rc ;
thus ex y being object st
( y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A29, A30, Lm3;

suppose A51: vs . n = the Source of G . (c . n) ; :: thesis:

take y = [1,(c . n)]; :: thesis:
e in Edges_Out (v,rc) by A16, A31, A50, A51, Def2;
then A52: y in [:{1},(Edges_Out (v,rc)):] by A23, ZFMISC_1:87;
hence y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] by XBOOLE_0:def 3; :: thesis:
reconsider y9 = y as Element of evio by A52, XBOOLE_0:def 3;
S₁[x9,y9,n] by A26, A28, A49, A51;
hence [x,y] in Z by A29, A30; :: thesis:

end;

suppose A53: ( vs . n = the Target of G . (c . n) & the Target of G . (c . n) <> the Source of G . (c . n) ) ; :: thesis:

take y = [0,(c . n)]; :: thesis:
e in Edges_In (v,rc) by A16, A31, A50, A53, Def1;
then A54: y in [:{0},(Edges_In (v,rc)):] by A24, ZFMISC_1:87;
hence y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] by XBOOLE_0:def 3; :: thesis:
reconsider y9 = y as Element of evio by A54, XBOOLE_0:def 3;
S₁[x9,y9,n] by A26, A28, A49, A53;
hence [x,y] in Z by A29, A30; :: thesis:

end;

thus for y being object st y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] holds
ex x being object st
( x in [:2,ev:] & [x,y] in Z ) :: thesis:

proof

let y be object ; :: thesis:
assume A55: y in [:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] ; :: thesis:
then reconsider y9 = y as Element of evio ;

per cases by A55, XBOOLE_0:def 3;

suppose A56: y in [:{0},(Edges_In (v,rc)):] ; :: thesis:

then consider u, e being object such that
A57: [u,e] = y by RELAT_1:def 1;
A58: e in Edges_In (v,rc) by A56, A57, ZFMISC_1:87;
then A59: the Target of G . e = v by Def1;
e in rc by A58, Def1;
then consider n being object such that
A60: n in dom c and
A61: e = c . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A60;
A62: dom c = Seg (len c) by FINSEQ_1:def 3;
then A63: 1 <= n by A60, FINSEQ_1:1;
A64: 1 in 2 by CARD_1:50, TARSKI:def 2;
A65: 0 in 2 by CARD_1:50, TARSKI:def 2;
A66: n <= len c by A60, A62, FINSEQ_1:1;
A67: u in {0} by A56, A57, ZFMISC_1:87;
then A68: u = 0 by TARSKI:def 1;
thus ex x being object st
( x in [:2,ev:] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A63, A66, Lm3;

suppose A69: vs . (n + 1) = the Target of G . (c . n) ; :: thesis:

thus ex x being object st
( x in [:2,ev:] & [x,y] in Z ) :: thesis:

proof

per cases by A66, XXREAL_0:1;

suppose A70: n = len c ; :: thesis:

take x = [0,1]; :: thesis:
vs . 1 = v by A1, A59, A61, A69, A70, MSSCYC_1:6;
then A71: 1 in ev by A63, A70;
hence x in [:2,ev:] by A65, ZFMISC_1:87; :: thesis:
reconsider x9 = x as Element of [:2,ev:] by A65, A71, ZFMISC_1:87;
( 1 <= len c & S₂[x9,y9,1] ) by A1, A57, A67, A60, A61, A62, A69, A70, FINSEQ_1:1, MSSCYC_1:6, TARSKI:def 1;
hence [x,y] in Z ; :: thesis:

end;

suppose A72: n < len c ; :: thesis:

take x = [0,(n + 1)]; :: thesis:
A73: ( 1 <= n + 1 & n + 1 <= len c ) by A72, NAT_1:11, NAT_1:13;
then A74: n + 1 in ev by A59, A61, A69;
hence x in [:2,ev:] by A65, ZFMISC_1:87; :: thesis:
reconsider x9 = x as Element of [:2,ev:] by A65, A74, ZFMISC_1:87;
S₂[x9,y9,n + 1] by A57, A68, A61, A63, A69;
hence [x,y] in Z by A73; :: thesis:

end;

suppose A75: ( vs . n = the Target of G . (c . n) & the Target of G . (c . n) <> the Source of G . (c . n) ) ; :: thesis:

take x = [1,n]; :: thesis:
A76: n in ev by A59, A61, A63, A66, A75;
hence x in [:2,ev:] by A64, ZFMISC_1:87; :: thesis:
reconsider x9 = x as Element of [:2,ev:] by A64, A76, ZFMISC_1:87;
S₁[x9,y9,n] by A57, A67, A61, A75, TARSKI:def 1;
hence [x,y] in Z by A63, A66; :: thesis:

end;

suppose A77: y in [:{1},(Edges_Out (v,rc)):] ; :: thesis:

then consider u, e being object such that
A78: [u,e] = y by RELAT_1:def 1;
A79: e in Edges_Out (v,rc) by A77, A78, ZFMISC_1:87;
then A80: the Source of G . e = v by Def2;
e in rc by A79, Def2;
then consider n being object such that
A81: n in dom c and
A82: e = c . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A81;
A83: dom c = Seg (len c) by FINSEQ_1:def 3;
then A84: 1 <= n by A81, FINSEQ_1:1;
A85: 1 in 2 by CARD_1:50, TARSKI:def 2;
A86: 0 in 2 by CARD_1:50, TARSKI:def 2;
A87: n <= len c by A81, A83, FINSEQ_1:1;
A88: u in {1} by A77, A78, ZFMISC_1:87;
then A89: u = 1 by TARSKI:def 1;
thus ex x being object st
( x in [:2,ev:] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A84, A87, Lm3;

suppose A90: ( vs . (n + 1) = the Source of G . (c . n) & the Target of G . (c . n) <> the Source of G . (c . n) ) ; :: thesis:

thus ex x being object st
( x in [:2,ev:] & [x,y] in Z ) :: thesis:

proof

per cases by A87, XXREAL_0:1;

suppose A91: n = len c ; :: thesis:

take x = [0,1]; :: thesis:
vs . 1 = v by A1, A80, A82, A90, A91, MSSCYC_1:6;
then A92: 1 in ev by A84, A91;
hence x in [:2,ev:] by A86, ZFMISC_1:87; :: thesis:
reconsider x9 = x as Element of [:2,ev:] by A86, A92, ZFMISC_1:87;
( 1 <= len c & S₂[x9,y9,1] ) by A1, A78, A88, A81, A82, A83, A90, A91, FINSEQ_1:1, MSSCYC_1:6, TARSKI:def 1;
hence [x,y] in Z ; :: thesis:

end;

suppose A93: n < len c ; :: thesis:

take x = [0,(n + 1)]; :: thesis:
A94: ( 1 <= n + 1 & n + 1 <= len c ) by A93, NAT_1:11, NAT_1:13;
then A95: n + 1 in ev by A80, A82, A90;
hence x in [:2,ev:] by A86, ZFMISC_1:87; :: thesis:
reconsider x9 = x as Element of [:2,ev:] by A86, A95, ZFMISC_1:87;
S₂[x9,y9,n + 1] by A78, A89, A82, A84, A90;
hence [x,y] in Z by A94; :: thesis:

end;

suppose A96: vs . n = the Source of G . (c . n) ; :: thesis:

take x = [1,n]; :: thesis:
A97: n in ev by A80, A82, A84, A87, A96;
hence x in [:2,ev:] by A85, ZFMISC_1:87; :: thesis:
reconsider x9 = x as Element of [:2,ev:] by A85, A97, ZFMISC_1:87;
S₁[x9,y9,n] by A78, A88, A82, A96, TARSKI:def 1;
hence [x,y] in Z by A84, A87; :: thesis:

end;

thus for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) :: thesis:

proof

let x, y, z, u be object ; :: thesis:
assume that
A98: [x,y] in Z and
A99: [z,u] in Z ; :: thesis:
consider x9 being Element of [:2,ev:], y9 being Element of evio such that
A100: [x,y] = [x9,y9] and
A101: ex n being Element of NAT st
( 1 <= n & n <= len c & ( S₂[x9,y9,n] or S₁[x9,y9,n] ) ) by A98;
consider z9 being Element of [:2,ev:], u9 being Element of evio such that
A102: [z,u] = [z9,u9] and
A103: ex n being Element of NAT st
( 1 <= n & n <= len c & ( S₂[z9,u9,n] or S₁[z9,u9,n] ) ) by A99;
A104: x = x9 by A100, XTUPLE_0:1;
A105: y = y9 by A100, XTUPLE_0:1;
consider n2 being Element of NAT such that
A106: 1 <= n2 and
A107: n2 <= len c and
A108: ( S₂[z9,u9,n2] or S₁[z9,u9,n2] ) by A103;
consider n1 being Element of NAT such that
A109: 1 <= n1 and
A110: n1 <= len c and
A111: ( S₂[x9,y9,n1] or S₁[x9,y9,n1] ) by A101;
A112: z = z9 by A102, XTUPLE_0:1;
thus ( x = z implies y = u ) :: thesis:

proof

assume A113: x = z ; :: thesis:

per cases by A111, A108;

suppose A114: ( S₂[x9,y9,n1] & S₂[z9,u9,n2] ) ; :: thesis:

then A115: n1 = n2 by A104, A112, A113, XTUPLE_0:1;
thus y = u :: thesis:

proof

per cases by A114;

suppose ( ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y9 = [0,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) & ex k being Element of NAT st
( 1 <= k & n2 = k + 1 & ( ( vs . n2 = the Target of G . (c . k) & u9 = [0,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ) ; :: thesis:

hence y = u by A102, A105, A115, XTUPLE_0:1; :: thesis:

end;

suppose ( ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y9 = [0,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) & n2 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & u9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & u9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

hence y = u by A115; :: thesis:

end;

suppose ( n1 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & y9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & y9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) & ex k being Element of NAT st
( 1 <= k & n2 = k + 1 & ( ( vs . n2 = the Target of G . (c . k) & u9 = [0,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ) ; :: thesis:

hence y = u by A115; :: thesis:

end;

suppose ( n1 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & y9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & y9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) & n2 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & u9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & u9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

hence y = u by A102, A105, XTUPLE_0:1; :: thesis:

end;

suppose ( S₂[x9,y9,n1] & S₁[z9,u9,n2] ) ; :: thesis:

hence y = u by A104, A112, A113, XTUPLE_0:1; :: thesis:

end;

suppose ( S₁[x9,y9,n1] & S₂[z9,u9,n2] ) ; :: thesis:

hence y = u by A104, A112, A113, XTUPLE_0:1; :: thesis:

end;

suppose A116: ( S₁[x9,y9,n1] & S₁[z9,u9,n2] ) ; :: thesis:

then n1 = n2 by A104, A112, A113, XTUPLE_0:1;
hence y = u by A100, A102, A116, XTUPLE_0:1; :: thesis:

end;

A117: u = u9 by A102, XTUPLE_0:1;
thus ( y = u implies x = z ) :: thesis:

proof

assume A118: y = u ; :: thesis:

per cases by A111, A108;

suppose A119: ( S₂[x9,y9,n1] & S₂[z9,u9,n2] ) ; :: thesis:

thus x = z :: thesis:

proof

per cases by A119;

suppose A120: ( ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y9 = [0,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) & ex k being Element of NAT st
( 1 <= k & n2 = k + 1 & ( ( vs . n2 = the Target of G . (c . k) & u9 = [0,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ) ; :: thesis:

then consider k2 being Element of NAT such that
A121: 1 <= k2 and
A122: n2 = k2 + 1 and
A123: ( ( vs . n2 = the Target of G . (c . k2) & u9 = [0,(c . k2)] ) or ( vs . n2 = the Source of G . (c . k2) & u9 = [1,(c . k2)] & the Target of G . (c . k2) <> the Source of G . (c . k2) ) ) ;
k2 <= n2 by A122, NAT_1:12;
then A124: k2 <= len c by A107, XXREAL_0:2;
consider k1 being Element of NAT such that
A125: 1 <= k1 and
A126: n1 = k1 + 1 and
A127: ( ( vs . n1 = the Target of G . (c . k1) & y9 = [0,(c . k1)] ) or ( vs . n1 = the Source of G . (c . k1) & y9 = [1,(c . k1)] & the Target of G . (c . k1) <> the Source of G . (c . k1) ) ) by A120;
k1 <= n1 by A126, NAT_1:12;
then A128: k1 <= len c by A110, XXREAL_0:2;
c . k1 = c . k2 by A105, A117, A118, A127, A123, XTUPLE_0:1;
then k1 = k2 by A125, A121, A128, A124, Lm2;
hence x = z by A100, A102, A119, A126, A122, XTUPLE_0:1; :: thesis:

end;

suppose A129: ( ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y9 = [0,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) & n2 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & u9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & u9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

A130: 1 <= len c by A109, A110, XXREAL_0:2;
consider k1 being Element of NAT such that
A131: 1 <= k1 and
A132: n1 = k1 + 1 and
( ( vs . n1 = the Target of G . (c . k1) & y9 = [0,(c . k1)] ) or ( vs . n1 = the Source of G . (c . k1) & y9 = [1,(c . k1)] & the Target of G . (c . k1) <> the Source of G . (c . k1) ) ) by A129;
k1 <= n1 by A132, NAT_1:12;
then A133: k1 <= len c by A110, XXREAL_0:2;
c . k1 = c . (len c) by A105, A117, A118, A129, A132, XTUPLE_0:1;
then (len c) + 1 <= len c by A110, A131, A132, A133, A130, Lm2;
hence x = z by NAT_1:13; :: thesis:

end;

suppose A134: ( n1 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & y9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & y9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) & ex k being Element of NAT st
( 1 <= k & n2 = k + 1 & ( ( vs . n2 = the Target of G . (c . k) & u9 = [0,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ) ; :: thesis:

A135: 1 <= len c by A106, A107, XXREAL_0:2;
consider k2 being Element of NAT such that
A136: 1 <= k2 and
A137: n2 = k2 + 1 and
( ( vs . n2 = the Target of G . (c . k2) & u9 = [0,(c . k2)] ) or ( vs . n2 = the Source of G . (c . k2) & u9 = [1,(c . k2)] & the Target of G . (c . k2) <> the Source of G . (c . k2) ) ) by A134;
k2 <= n2 by A137, NAT_1:12;
then A138: k2 <= len c by A107, XXREAL_0:2;
c . k2 = c . (len c) by A105, A117, A118, A134, A137, XTUPLE_0:1;
then (len c) + 1 <= len c by A107, A136, A137, A138, A135, Lm2;
hence x = z by NAT_1:13; :: thesis:

end;

suppose ( n1 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & y9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & y9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) & n2 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & u9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & u9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

hence x = z by A100, A102, A119, XTUPLE_0:1; :: thesis:

end;

suppose A139: ( S₂[x9,y9,n1] & S₁[z9,u9,n2] ) ; :: thesis:

thus x = z :: thesis:

proof

per cases by A139;

suppose ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y9 = [0,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ; :: thesis:

then consider k being Element of NAT such that
A140: 1 <= k and
A141: n1 = k + 1 and
( ( vs . n1 = the Target of G . (c . k) & y9 = [0,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ;
k <= n1 by A141, NAT_1:12;
then A142: k <= len c by A110, XXREAL_0:2;
c . n2 = c . k by A105, A117, A118, A139, A140, A141, XTUPLE_0:1;
then n2 = k by A106, A107, A140, A142, Lm2;
hence x = z by A1, A105, A117, A106, A107, A118, A139, A141, Lm3, XTUPLE_0:1; :: thesis:

end;

suppose A143: ( n1 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & y9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & y9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

A144: 1 <= len c by A109, A110, XXREAL_0:2;
c . n2 = c . (len c) by A105, A117, A118, A139, A143, XTUPLE_0:1;
then A145: n2 = len c by A106, A107, A144, Lm2;
( ( vs . n2 = the Target of G . (c . n2) & vs . (n2 + 1) = the Source of G . (c . n2) ) or ( vs . n2 = the Source of G . (c . n2) & vs . (n2 + 1) = the Target of G . (c . n2) ) ) by A1, A106, A107, Lm3;
hence x = z by A1, A105, A117, A118, A139, A143, A145, MSSCYC_1:6, XTUPLE_0:1; :: thesis:

end;

suppose A146: ( S₁[x9,y9,n1] & S₂[z9,u9,n2] ) ; :: thesis:

thus x = z :: thesis:

proof

per cases by A146;

suppose ex k being Element of NAT st
( 1 <= k & n2 = k + 1 & ( ( vs . n2 = the Target of G . (c . k) & u9 = [0,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ; :: thesis:

then consider k being Element of NAT such that
A147: 1 <= k and
A148: n2 = k + 1 and
( ( vs . n2 = the Target of G . (c . k) & u9 = [0,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u9 = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ;
k <= n2 by A148, NAT_1:12;
then A149: k <= len c by A107, XXREAL_0:2;
c . n1 = c . k by A105, A117, A118, A146, A147, A148, XTUPLE_0:1;
then n1 = k by A109, A110, A147, A149, Lm2;
hence x = z by A1, A105, A117, A109, A110, A118, A146, A148, Lm3, XTUPLE_0:1; :: thesis:

end;

suppose A150: ( n2 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & u9 = [0,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & u9 = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

A151: 1 <= len c by A109, A110, XXREAL_0:2;
c . n1 = c . (len c) by A105, A117, A118, A146, A150, XTUPLE_0:1;
then A152: n1 = len c by A109, A110, A151, Lm2;
( ( vs . n1 = the Target of G . (c . n1) & vs . (n1 + 1) = the Source of G . (c . n1) ) or ( vs . n1 = the Source of G . (c . n1) & vs . (n1 + 1) = the Target of G . (c . n1) ) ) by A1, A109, A110, Lm3;
hence x = z by A1, A105, A117, A118, A146, A150, A152, MSSCYC_1:6, XTUPLE_0:1; :: thesis:

end;

suppose A153: ( S₁[x9,y9,n1] & S₁[z9,u9,n2] ) ; :: thesis:

then c . n1 = c . n2 by A105, A117, A118, XTUPLE_0:1;
then n1 = n2 by A109, A110, A106, A107, Lm2;
hence x = z by A100, A102, A153, XTUPLE_0:1; :: thesis:

end;

then [:2,ev:],[:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):] are_equipotent ;
then card [:2,ev:] = card ([:{0},(Edges_In (v,rc)):] \/ [:{1},(Edges_Out (v,rc)):]) by CARD_1:5
.= (card [:{0},(Edges_In (v,rc)):]) + (card [:{1},(Edges_Out (v,rc)):]) by A9, CARD_2:40 ;
then Degree (v,rc) = (card 2) * (card ev) by A7, A6, CARD_2:46
.= 2 * (card ev) ;
hence Degree (v,(rng c)) is even ; :: thesis:

end;