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 A1: ( vs is_vertex_seq_of c & v in rng vs ) ; :: thesis:
set T = the Target of G;
set S = the Source of G;

per cases ;

suppose c is empty ; :: thesis:

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

end;

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

then reconsider rc = rng c as non empty set ;
A3: rc c= the carrier' of G by FINSEQ_1:def 4;
then not the carrier' of G is empty by XBOOLE_1:3;
then reconsider G' = G as non void finite Graph ;
reconsider vs' = vs as FinSequence of the carrier of G' ;
A4: vs' . 1 = vs . (len vs) by A1, MSSCYC_1:6;
A5: len vs = (len c) + 1 by A1, GRAPH_2:def 7;
set ev = { n where n is Element of NAT : ( 1 <= n & n <= len c & vs . n = v ) } ;
{ n where n is Element of NAT : ( 1 <= n & n <= len c & vs . n = v ) } c= Seg (len c)

proof

let x be set ; :: 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 consider n being Element of NAT such that
A6: ( x = n & 1 <= n & n <= len c & vs . n = v ) ;
thus x in Seg (len c) by A6, FINSEQ_1:3; :: thesis:

end;

then reconsider ev = { n where n is Element of NAT : ( 1 <= n & n <= len c & vs . n = v ) } as Subset of (Seg (len c)) ;

now

consider n being set such that
A7: ( n in dom vs & vs . n = v ) by A1, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A7;
A8: ( 1 <= n & n <= len vs ) by A7, FINSEQ_3:27;
len c <> 0 by A2;
then 0 < len c ;
then A9: 0 + 1 <= len c by NAT_1:13;
thus not ev is empty :: thesis:

proof

per cases by A8, XXREAL_0:1;

suppose n = len vs ; :: thesis:

then 1 in ev by A4, A7, A9;
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 A7, A8;
hence not ev is empty ; :: thesis:

end;

then reconsider ev = ev as non empty finite set ;
set ev'2 = [:2,ev:];
set evin = [:{0 },(Edges_In v,rc):];
set evout = [:{1},(Edges_Out v,rc):];
A10: card [:{0 },(Edges_In v,rc):] = (card {0 }) * (card (Edges_In v,rc)) by CARD_2:65
.= 1 * (card (Edges_In v,rc)) by CARD_1:50
.= card (Edges_In v,rc) ;
A11: card [:{1},(Edges_Out v,rc):] = (card {1}) * (card (Edges_Out v,rc)) by CARD_2:65
.= 1 * (card (Edges_Out v,rc)) by CARD_1:50
.= card (Edges_Out v,rc) ;

now

assume [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] is empty ; :: thesis:
then ( [:{0 },(Edges_In v,rc):] is empty & [:{1},(Edges_Out v,rc):] is empty ) ;
then Degree v,rc = 0 + 0 by A10, A11;
hence contradiction by A1, A2, Th37; :: thesis:

end;

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

now

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)) ) ) ) ) );
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) ) ) );
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 set st x in [:2,ev:] holds
ex y being set st
( y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] & [x,y] in Z ) :: thesis:

proof

let x be set ; :: thesis:
assume A12: x in [:2,ev:] ; :: thesis:
then consider u, w being set such that
A13: [u,w] = x by RELAT_1:def 1;
reconsider x' = x as Element of [:2,ev:] by A12;
A14: ( u in 2 & w in ev ) by A12, A13, ZFMISC_1:106;
then consider n being Element of NAT such that
A15: ( w = n & 1 <= n & n <= len c & vs . n = v ) ;
A16: ( 0 in {0 } & 1 in {1} ) by TARSKI:def 1;

per cases by A14, CARD_1:88, TARSKI:def 2;

suppose A17: u = 0 ; :: thesis:

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

proof

per cases by A15, XXREAL_0:1;

suppose 1 < n ; :: thesis:

then consider k being Element of NAT such that
A18: ( n = 1 + k & 1 <= k ) by FSM_1:1;
k <= n by A18, NAT_1:11;
then A19: k <= len c by A15, XXREAL_0:2;
then k in dom c by A18, FINSEQ_3:27;
then reconsider e = c . k as Element of rc by FUNCT_1:def 5;
A20: e in rc ;
thus ex y being set st
( y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A18, A19, Lm3;

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

take y = [0 ,(c . k)]; :: thesis:
e in Edges_In v,rc by A3, A15, A18, A20, A21, Def1;
then A22: y in [:{0 },(Edges_In v,rc):] by A16, ZFMISC_1:106;
hence y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] by XBOOLE_0:def 3; :: thesis:
reconsider y' = y as Element of evio by A22, XBOOLE_0:def 3;
S₁[x',y',n] by A13, A15, A17, A18, A21;
hence [x,y] in Z by A15; :: thesis:

end;

suppose A23: ( 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 A3, A15, A18, A20, A23, Def2;
then A24: y in [:{1},(Edges_Out v,rc):] by A16, ZFMISC_1:106;
hence y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] by XBOOLE_0:def 3; :: thesis:
reconsider y' = y as Element of evio by A24, XBOOLE_0:def 3;
S₁[x',y',n] by A13, A15, A17, A18, A23;
hence [x,y] in Z by A15; :: thesis:

end;

suppose A25: n = 1 ; :: thesis:

A26: ( 1 <= len c & len c <= len c ) by A15, XXREAL_0:2;
then len c in dom c by FINSEQ_3:27;
then reconsider e = c . (len c) as Element of rc by FUNCT_1:def 5;
A27: e in rc ;
A28: vs . 1 = vs . ((len c) + 1) by A1, A5, MSSCYC_1:6;
A29: ( 1 <= 1 & 1 <= len c ) by A15, XXREAL_0:2;
thus ex y being set st
( y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A26, Lm3;

suppose A30: 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 A3, A15, A25, A27, A28, A30, Def1;
then A31: y in [:{0 },(Edges_In v,rc):] by A16, ZFMISC_1:106;
hence y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] by XBOOLE_0:def 3; :: thesis:
reconsider y' = y as Element of evio by A31, XBOOLE_0:def 3;
S₁[x',y',1] by A1, A5, A13, A15, A17, A25, A30, MSSCYC_1:6;
hence [x,y] in Z by A29; :: thesis:

end;

suppose A32: ( 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 A3, A15, A25, A27, A28, A32, Def2;
then A33: y in [:{1},(Edges_Out v,rc):] by A16, ZFMISC_1:106;
hence y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] by XBOOLE_0:def 3; :: thesis:
reconsider y' = y as Element of evio by A33, XBOOLE_0:def 3;
S₁[x',y',1] by A1, A5, A13, A15, A17, A25, A32, MSSCYC_1:6;
hence [x,y] in Z by A29; :: thesis:

end;

suppose A34: u = 1 ; :: thesis:

n in dom c by A15, FINSEQ_3:27;
then reconsider e = c . n as Element of rc by FUNCT_1:def 5;
A35: e in rc ;
thus ex y being set st
( y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A15, Lm3;

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

take y = [1,(c . n)]; :: thesis:
e in Edges_Out v,rc by A3, A15, A35, A36, Def2;
then A37: y in [:{1},(Edges_Out v,rc):] by A16, ZFMISC_1:106;
hence y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] by XBOOLE_0:def 3; :: thesis:
reconsider y' = y as Element of evio by A37, XBOOLE_0:def 3;
S₂[x',y',n] by A13, A15, A34, A36;
hence [x,y] in Z by A15; :: thesis:

end;

suppose A38: ( 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 A3, A15, A35, A38, Def1;
then A39: y in [:{0 },(Edges_In v,rc):] by A16, ZFMISC_1:106;
hence y in [:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] by XBOOLE_0:def 3; :: thesis:
reconsider y' = y as Element of evio by A39, XBOOLE_0:def 3;
S₂[x',y',n] by A13, A15, A34, A38;
hence [x,y] in Z by A15; :: thesis:

end;

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

proof

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

per cases by A40, XBOOLE_0:def 3;

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

then consider u, e being set such that
A42: [u,e] = y by RELAT_1:def 1;
A43: ( u in {0 } & e in Edges_In v,rc ) by A41, A42, ZFMISC_1:106;
then A44: u = 0 by TARSKI:def 1;
A45: ( e in rc & the Target of G . e = v ) by A43, Def1;
then consider n being set such that
A46: ( n in dom c & e = c . n ) by FUNCT_1:def 5;
A47: dom c = Seg (len c) by FINSEQ_1:def 3;
reconsider n = n as Element of NAT by A46;
A48: ( 1 <= n & n <= len c ) by A46, A47, FINSEQ_1:3;
A49: ( 0 in 2 & 1 in 2 ) by CARD_1:88, TARSKI:def 2;
thus ex x being set st
( x in [:2,ev:] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A48, Lm3;

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

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

proof

per cases by A48, XXREAL_0:1;

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

take x = [0 ,1]; :: thesis:
A52: vs . 1 = v by A1, A5, A45, A46, A50, A51, MSSCYC_1:6;
A53: ( 1 <= 1 & 1 <= n & 1 <= len c ) by A46, A47, A51, FINSEQ_1:3;
A54: 1 in ev by A48, A51, A52;
hence x in [:2,ev:] by A49, ZFMISC_1:106; :: thesis:
reconsider x' = x as Element of [:2,ev:] by A49, A54, ZFMISC_1:106;
S₁[x',y',1] by A1, A5, A42, A43, A46, A50, A51, MSSCYC_1:6, TARSKI:def 1;
hence [x,y] in Z by A53; :: thesis:

end;

suppose n < len c ; :: thesis:

then A55: ( 1 <= n + 1 & n + 1 <= len c ) by NAT_1:11, NAT_1:13;
take x = [0 ,(n + 1)]; :: thesis:
A56: n + 1 in ev by A45, A46, A50, A55;
hence x in [:2,ev:] by A49, ZFMISC_1:106; :: thesis:
reconsider x' = x as Element of [:2,ev:] by A49, A56, ZFMISC_1:106;
S₁[x',y',n + 1] by A42, A44, A46, A48, A50;
hence [x,y] in Z by A55; :: thesis:

end;

suppose A57: ( 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:
A58: n in ev by A45, A46, A48, A57;
hence x in [:2,ev:] by A49, ZFMISC_1:106; :: thesis:
reconsider x' = x as Element of [:2,ev:] by A49, A58, ZFMISC_1:106;
S₂[x',y',n] by A42, A43, A46, A57, TARSKI:def 1;
hence [x,y] in Z by A48; :: thesis:

end;

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

then consider u, e being set such that
A60: [u,e] = y by RELAT_1:def 1;
A61: ( u in {1} & e in Edges_Out v,rc ) by A59, A60, ZFMISC_1:106;
then A62: u = 1 by TARSKI:def 1;
A63: ( e in rc & the Source of G . e = v ) by A61, Def2;
then consider n being set such that
A64: ( n in dom c & e = c . n ) by FUNCT_1:def 5;
A65: dom c = Seg (len c) by FINSEQ_1:def 3;
reconsider n = n as Element of NAT by A64;
A66: ( 1 <= n & n <= len c ) by A64, A65, FINSEQ_1:3;
A67: ( 0 in 2 & 1 in 2 ) by CARD_1:88, TARSKI:def 2;
thus ex x being set st
( x in [:2,ev:] & [x,y] in Z ) :: thesis:

proof

per cases by A1, A66, Lm3;

suppose A68: ( 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 set st
( x in [:2,ev:] & [x,y] in Z ) :: thesis:

proof

per cases by A66, XXREAL_0:1;

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

take x = [0 ,1]; :: thesis:
A70: vs . 1 = v by A1, A5, A63, A64, A68, A69, MSSCYC_1:6;
A71: ( 1 <= 1 & 1 <= n & 1 <= len c ) by A64, A65, A69, FINSEQ_1:3;
A72: 1 in ev by A66, A69, A70;
hence x in [:2,ev:] by A67, ZFMISC_1:106; :: thesis:
reconsider x' = x as Element of [:2,ev:] by A67, A72, ZFMISC_1:106;
S₁[x',y',1] by A1, A5, A60, A61, A64, A68, A69, MSSCYC_1:6, TARSKI:def 1;
hence [x,y] in Z by A71; :: thesis:

end;

suppose n < len c ; :: thesis:

then A73: ( 1 <= n + 1 & n + 1 <= len c ) by NAT_1:11, NAT_1:13;
take x = [0 ,(n + 1)]; :: thesis:
A74: n + 1 in ev by A63, A64, A68, A73;
hence x in [:2,ev:] by A67, ZFMISC_1:106; :: thesis:
reconsider x' = x as Element of [:2,ev:] by A67, A74, ZFMISC_1:106;
S₁[x',y',n + 1] by A60, A62, A64, A66, A68;
hence [x,y] in Z by A73; :: thesis:

end;

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

take x = [1,n]; :: thesis:
A76: n in ev by A63, A64, A66, A75;
hence x in [:2,ev:] by A67, ZFMISC_1:106; :: thesis:
reconsider x' = x as Element of [:2,ev:] by A67, A76, ZFMISC_1:106;
S₂[x',y',n] by A60, A61, A64, A75, TARSKI:def 1;
hence [x,y] in Z by A66; :: thesis:

end;

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

proof

let x, y, z, u be set ; :: thesis:
assume A77: ( [x,y] in Z & [z,u] in Z ) ; :: thesis:
then consider x' being Element of [:2,ev:], y' being Element of evio such that
A78: [x,y] = [x',y'] and
A79: ex n being Element of NAT st
( 1 <= n & n <= len c & ( S₁[x',y',n] or S₂[x',y',n] ) ) ;
consider z' being Element of [:2,ev:], u' being Element of evio such that
A80: [z,u] = [z',u'] and
A81: ex n being Element of NAT st
( 1 <= n & n <= len c & ( S₁[z',u',n] or S₂[z',u',n] ) ) by A77;
A82: ( x = x' & y = y' & z = z' & u = u' ) by A78, A80, ZFMISC_1:33;
consider n1 being Element of NAT such that
A83: ( 1 <= n1 & n1 <= len c ) and
A84: ( S₁[x',y',n1] or S₂[x',y',n1] ) by A79;
consider n2 being Element of NAT such that
A85: ( 1 <= n2 & n2 <= len c ) and
A86: ( S₁[z',u',n2] or S₂[z',u',n2] ) by A81;
thus ( x = z implies y = u ) :: thesis:

proof

assume A87: x = z ; :: thesis:

per cases by A84, A86;

suppose A88: ( S₁[x',y',n1] & S₁[z',u',n2] ) ; :: thesis:

then A89: n1 = n2 by A82, A87, ZFMISC_1:33;
thus y = u :: thesis:

proof

per cases by A88;

suppose A90: ( ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y' = [0 ,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y' = [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) & u' = [0 ,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u' = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ) ; :: thesis:

then consider k1 being Element of NAT such that
A91: ( 1 <= k1 & n1 = k1 + 1 & ( ( vs . n1 = the Target of G . (c . k1) & y' = [0 ,(c . k1)] ) or ( vs . n1 = the Source of G . (c . k1) & y' = [1,(c . k1)] & the Target of G . (c . k1) <> the Source of G . (c . k1) ) ) ) ;
consider k2 being Element of NAT such that
A92: ( 1 <= k2 & n2 = k2 + 1 & ( ( vs . n2 = the Target of G . (c . k2) & u' = [0 ,(c . k2)] ) or ( vs . n2 = the Source of G . (c . k2) & u' = [1,(c . k2)] & the Target of G . (c . k2) <> the Source of G . (c . k2) ) ) ) by A90;
thus y = u by A82, A89, A91, A92; :: thesis:

end;

suppose A93: ( ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y' = [0 ,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y' = [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)) & u' = [0 ,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & u' = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

thus y = u by A89, A93; :: thesis:

end;

suppose A94: ( n1 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & y' = [0 ,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & y' = [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) & u' = [0 ,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u' = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ) ; :: thesis:

thus y = u by A89, A94; :: thesis:

end;

suppose ( n1 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & y' = [0 ,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & y' = [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)) & u' = [0 ,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & u' = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

hence y = u by A82; :: thesis:

end;

suppose ( S₁[x',y',n1] & S₂[z',u',n2] ) ; :: thesis:

hence y = u by A82, A87, ZFMISC_1:33; :: thesis:

end;

suppose ( S₂[x',y',n1] & S₁[z',u',n2] ) ; :: thesis:

hence y = u by A82, A87, ZFMISC_1:33; :: thesis:

end;

suppose A95: ( S₂[x',y',n1] & S₂[z',u',n2] ) ; :: thesis:

then n1 = n2 by A82, A87, ZFMISC_1:33;
hence y = u by A78, A80, A95, ZFMISC_1:33; :: thesis:

end;

thus ( y = u implies x = z ) :: thesis:

proof

assume A96: y = u ; :: thesis:

per cases by A84, A86;

suppose A97: ( S₁[x',y',n1] & S₁[z',u',n2] ) ; :: thesis:

thus x = z :: thesis:

proof

per cases by A97;

suppose A98: ( ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y' = [0 ,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y' = [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) & u' = [0 ,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u' = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ) ; :: thesis:

then consider k1 being Element of NAT such that
A99: ( 1 <= k1 & n1 = k1 + 1 & ( ( vs . n1 = the Target of G . (c . k1) & y' = [0 ,(c . k1)] ) or ( vs . n1 = the Source of G . (c . k1) & y' = [1,(c . k1)] & the Target of G . (c . k1) <> the Source of G . (c . k1) ) ) ) ;
consider k2 being Element of NAT such that
A100: ( 1 <= k2 & n2 = k2 + 1 & ( ( vs . n2 = the Target of G . (c . k2) & u' = [0 ,(c . k2)] ) or ( vs . n2 = the Source of G . (c . k2) & u' = [1,(c . k2)] & the Target of G . (c . k2) <> the Source of G . (c . k2) ) ) ) by A98;
A101: c . k1 = c . k2 by A82, A96, A99, A100, ZFMISC_1:33;
( k1 <= n1 & k2 <= n2 ) by A99, A100, NAT_1:12;
then ( k1 <= len c & k2 <= len c ) by A83, A85, XXREAL_0:2;
then k1 = k2 by A99, A100, A101, Lm2;
hence x = z by A78, A80, A97, A99, A100, ZFMISC_1:33; :: thesis:

end;

suppose A102: ( ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y' = [0 ,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y' = [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)) & u' = [0 ,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & u' = [1,(c . (len c))] & the Target of G . (c . (len c)) <> the Source of G . (c . (len c)) ) ) ) ; :: thesis:

then consider k1 being Element of NAT such that
A103: ( 1 <= k1 & n1 = k1 + 1 & ( ( vs . n1 = the Target of G . (c . k1) & y' = [0 ,(c . k1)] ) or ( vs . n1 = the Source of G . (c . k1) & y' = [1,(c . k1)] & the Target of G . (c . k1) <> the Source of G . (c . k1) ) ) ) ;
A104: c . k1 = c . (len c) by A82, A96, A102, A103, ZFMISC_1:33;
k1 <= n1 by A103, NAT_1:12;
then A105: k1 <= len c by A83, XXREAL_0:2;
( 1 <= len c & len c <= len c ) by A83, XXREAL_0:2;
then (len c) + 1 <= len c by A83, A103, A104, A105, Lm2;
hence x = z by NAT_1:13; :: thesis:

end;

suppose A106: ( n1 = 1 & ( ( vs . 1 = the Target of G . (c . (len c)) & y' = [0 ,(c . (len c))] ) or ( vs . 1 = the Source of G . (c . (len c)) & y' = [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) & u' = [0 ,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u' = [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
A107: ( 1 <= k2 & n2 = k2 + 1 & ( ( vs . n2 = the Target of G . (c . k2) & u' = [0 ,(c . k2)] ) or ( vs . n2 = the Source of G . (c . k2) & u' = [1,(c . k2)] & the Target of G . (c . k2) <> the Source of G . (c . k2) ) ) ) ;
A108: c . k2 = c . (len c) by A82, A96, A106, A107, ZFMISC_1:33;
k2 <= n2 by A107, NAT_1:12;
then A109: k2 <= len c by A85, XXREAL_0:2;
( 1 <= len c & len c <= len c ) by A85, XXREAL_0:2;
then (len c) + 1 <= len c by A85, A107, A108, A109, Lm2;
hence x = z by NAT_1:13; :: thesis:

end;

hence x = z by A78, A80, A97, ZFMISC_1:33; :: thesis:

end;

suppose A110: ( S₁[x',y',n1] & S₂[z',u',n2] ) ; :: thesis:

thus x = z :: thesis:

proof

per cases by A110;

suppose ex k being Element of NAT st
( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y' = [0 ,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y' = [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
A111: ( 1 <= k & n1 = k + 1 & ( ( vs . n1 = the Target of G . (c . k) & y' = [0 ,(c . k)] ) or ( vs . n1 = the Source of G . (c . k) & y' = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ;
A112: c . n2 = c . k by A82, A96, A110, A111, ZFMISC_1:33;
k <= n1 by A111, NAT_1:12;
then k <= len c by A83, XXREAL_0:2;
then n2 = k by A85, A111, A112, Lm2;
hence x = z by A1, A82, A85, A96, A110, A111, Lm3, ZFMISC_1:33; :: thesis:

end;

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

then A114: c . n2 = c . (len c) by A82, A96, A110, ZFMISC_1:33;
( 1 <= len c & len c <= len c ) by A83, XXREAL_0:2;
then A115: n2 = len c by A85, A114, Lm2;
thus x = z :: thesis:

proof

( ( 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, A85, Lm3;
hence x = z by A1, A5, A82, A96, A110, A113, A115, MSSCYC_1:6, ZFMISC_1:33; :: thesis:

end;

suppose A116: ( S₂[x',y',n1] & S₁[z',u',n2] ) ; :: thesis:

thus x = z :: thesis:

proof

per cases by A116;

suppose ex k being Element of NAT st
( 1 <= k & n2 = k + 1 & ( ( vs . n2 = the Target of G . (c . k) & u' = [0 ,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u' = [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
A117: ( 1 <= k & n2 = k + 1 & ( ( vs . n2 = the Target of G . (c . k) & u' = [0 ,(c . k)] ) or ( vs . n2 = the Source of G . (c . k) & u' = [1,(c . k)] & the Target of G . (c . k) <> the Source of G . (c . k) ) ) ) ;
A118: c . n1 = c . k by A82, A96, A116, A117, ZFMISC_1:33;
k <= n2 by A117, NAT_1:12;
then k <= len c by A85, XXREAL_0:2;
then n1 = k by A83, A117, A118, Lm2;
hence x = z by A1, A82, A83, A96, A116, A117, Lm3, ZFMISC_1:33; :: thesis:

end;

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

then A120: c . n1 = c . (len c) by A82, A96, A116, ZFMISC_1:33;
( 1 <= len c & len c <= len c ) by A83, XXREAL_0:2;
then A121: n1 = len c by A83, A120, Lm2;
thus x = z :: thesis:

proof

( ( 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, A83, Lm3;
hence x = z by A1, A5, A82, A96, A116, A119, A121, MSSCYC_1:6, ZFMISC_1:33; :: thesis:

end;

suppose A122: ( S₂[x',y',n1] & S₂[z',u',n2] ) ; :: thesis:

then c . n1 = c . n2 by A82, A96, ZFMISC_1:33;
then n1 = n2 by A83, A85, Lm2;
hence x = z by A78, A80, A122, ZFMISC_1:33; :: thesis:

end;

then A123: [:2,ev:],[:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):] are_equipotent by TARSKI:def 6;
A124: [:{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 set such that
A125: x in [:{0 },(Edges_In v,rc):] /\ [:{1},(Edges_Out v,rc):] by XBOOLE_0:4;
A126: ( x in [:{0 },(Edges_In v,rc):] & x in [:{1},(Edges_Out v,rc):] ) by A125, XBOOLE_0:def 4;
then consider x11, x12 being set such that
A127: ( x11 in {0 } & x12 in Edges_In v,rc & x = [x11,x12] ) by ZFMISC_1:def 2;
consider x21, x22 being set such that
A128: ( x21 in {1} & x22 in Edges_Out v,rc & x = [x21,x22] ) by A126, ZFMISC_1:def 2;
( x11 = 0 & x21 = 1 & x11 = x21 ) by A127, A128, TARSKI:def 1, ZFMISC_1:33;
hence contradiction ; :: thesis:

end;

card [:2,ev:] = card ([:{0 },(Edges_In v,rc):] \/ [:{1},(Edges_Out v,rc):]) by A123, CARD_1:21
.= (card [:{0 },(Edges_In v,rc):]) + (card [:{1},(Edges_Out v,rc):]) by A124, CARD_2:53 ;
then Degree v,rc = (card 2) * (card ev) by A10, A11, CARD_2:65
.= 2 * (card ev) by CARD_1:def 5 ;
hence Degree v,(rng c) is even ; :: thesis:

end;