:: GRAPH_4 semantic presentation begin definition let G be Graph; let x, y be Element of G; let e be set ; prede orientedly_joins x,y means :Def1: :: GRAPH_4:def 1 ( the Source of G . e = x & the Target of G . e = y ); end; :: deftheorem Def1 defines orientedly_joins GRAPH_4:def_1_:_ for G being Graph for x, y being Element of G for e being set holds ( e orientedly_joins x,y iff ( the Source of G . e = x & the Target of G . e = y ) ); theorem Th1: :: GRAPH_4:1 for e being set for G being Graph for v1, v2 being Element of G st e orientedly_joins v1,v2 holds e joins v1,v2 proof let e be set ; ::_thesis: for G being Graph for v1, v2 being Element of G st e orientedly_joins v1,v2 holds e joins v1,v2 let G be Graph; ::_thesis: for v1, v2 being Element of G st e orientedly_joins v1,v2 holds e joins v1,v2 let v1, v2 be Element of G; ::_thesis: ( e orientedly_joins v1,v2 implies e joins v1,v2 ) assume A1: e orientedly_joins v1,v2 ; ::_thesis: e joins v1,v2 then A2: the Source of G . e = v1 by Def1; the Target of G . e = v2 by A1, Def1; hence e joins v1,v2 by A2, GRAPH_1:def_12; ::_thesis: verum end; definition let G be Graph; let x, y be Element of the carrier of G; predx,y are_orientedly_incident means :: GRAPH_4:def 2 ex v being set st ( v in the carrier' of G & v orientedly_joins x,y ); end; :: deftheorem defines are_orientedly_incident GRAPH_4:def_2_:_ for G being Graph for x, y being Element of the carrier of G holds ( x,y are_orientedly_incident iff ex v being set st ( v in the carrier' of G & v orientedly_joins x,y ) ); theorem Th2: :: GRAPH_4:2 for e being set for G being Graph for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds ( v1 = v3 & v2 = v4 ) proof let e be set ; ::_thesis: for G being Graph for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds ( v1 = v3 & v2 = v4 ) let G be Graph; ::_thesis: for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds ( v1 = v3 & v2 = v4 ) let v1, v2, v3, v4 be Element of G; ::_thesis: ( e orientedly_joins v1,v2 & e orientedly_joins v3,v4 implies ( v1 = v3 & v2 = v4 ) ) assume that A1: e orientedly_joins v1,v2 and A2: e orientedly_joins v3,v4 ; ::_thesis: ( v1 = v3 & v2 = v4 ) A3: the Source of G . e = v1 by A1, Def1; the Target of G . e = v2 by A1, Def1; hence ( v1 = v3 & v2 = v4 ) by A2, A3, Def1; ::_thesis: verum end; definition let G be Graph; let X be set ; funcG -SVSet X -> set equals :: GRAPH_4:def 3 { v where v is Element of G : ex e being Element of the carrier' of G st ( e in X & v = the Source of G . e ) } ; correctness coherence { v where v is Element of G : ex e being Element of the carrier' of G st ( e in X & v = the Source of G . e ) } is set ; ; end; :: deftheorem defines -SVSet GRAPH_4:def_3_:_ for G being Graph for X being set holds G -SVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st ( e in X & v = the Source of G . e ) } ; definition let G be Graph; let X be set ; funcG -TVSet X -> set equals :: GRAPH_4:def 4 { v where v is Element of G : ex e being Element of the carrier' of G st ( e in X & v = the Target of G . e ) } ; correctness coherence { v where v is Element of G : ex e being Element of the carrier' of G st ( e in X & v = the Target of G . e ) } is set ; ; end; :: deftheorem defines -TVSet GRAPH_4:def_4_:_ for G being Graph for X being set holds G -TVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st ( e in X & v = the Target of G . e ) } ; theorem :: GRAPH_4:3 for G being Graph holds ( G -SVSet {} = {} & G -TVSet {} = {} ) proof let G be Graph; ::_thesis: ( G -SVSet {} = {} & G -TVSet {} = {} ) set X = {} ; A1: now__::_thesis:_not_G_-SVSet_{}_<>_{} assume A2: G -SVSet {} <> {} ; ::_thesis: contradiction set x = the Element of G -SVSet {}; the Element of G -SVSet {} in G -SVSet {} by A2; then ex v being Element of G st ( v = the Element of G -SVSet {} & ex e being Element of the carrier' of G st ( e in {} & v = the Source of G . e ) ) ; hence contradiction ; ::_thesis: verum end; now__::_thesis:_not_G_-TVSet_{}_<>_{} assume A3: G -TVSet {} <> {} ; ::_thesis: contradiction set x = the Element of G -TVSet {}; the Element of G -TVSet {} in G -TVSet {} by A3; then ex v being Element of G st ( v = the Element of G -TVSet {} & ex e being Element of the carrier' of G st ( e in {} & v = the Target of G . e ) ) ; hence contradiction ; ::_thesis: verum end; hence ( G -SVSet {} = {} & G -TVSet {} = {} ) by A1; ::_thesis: verum end; definition let G be Graph; let vs be FinSequence of the carrier of G; let c be FinSequence; predvs is_oriented_vertex_seq_of c means :Def5: :: GRAPH_4:def 5 ( len vs = (len c) + 1 & ( for n being Element of NAT st 1 <= n & n <= len c holds c . n orientedly_joins vs /. n,vs /. (n + 1) ) ); end; :: deftheorem Def5 defines is_oriented_vertex_seq_of GRAPH_4:def_5_:_ for G being Graph for vs being FinSequence of the carrier of G for c being FinSequence holds ( vs is_oriented_vertex_seq_of c iff ( len vs = (len c) + 1 & ( for n being Element of NAT st 1 <= n & n <= len c holds c . n orientedly_joins vs /. n,vs /. (n + 1) ) ) ); theorem Th4: :: GRAPH_4:4 for G being Graph for vs being FinSequence of the carrier of G for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds vs is_vertex_seq_of c proof let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds vs is_vertex_seq_of c let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds vs is_vertex_seq_of c let c be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c implies vs is_vertex_seq_of c ) assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: vs is_vertex_seq_of c then A2: len vs = (len c) + 1 by Def5; for n being Element of NAT st 1 <= n & n <= len c holds c . n joins vs /. n,vs /. (n + 1) proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len c implies c . n joins vs /. n,vs /. (n + 1) ) assume that A3: 1 <= n and A4: n <= len c ; ::_thesis: c . n joins vs /. n,vs /. (n + 1) c . n orientedly_joins vs /. n,vs /. (n + 1) by A1, A3, A4, Def5; hence c . n joins vs /. n,vs /. (n + 1) by Th1; ::_thesis: verum end; hence vs is_vertex_seq_of c by A2, GRAPH_2:def_6; ::_thesis: verum end; theorem :: GRAPH_4:5 for G being Graph for vs being FinSequence of the carrier of G for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds G -SVSet (rng c) c= rng vs proof let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds G -SVSet (rng c) c= rng vs let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds G -SVSet (rng c) c= rng vs let c be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c implies G -SVSet (rng c) c= rng vs ) assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: G -SVSet (rng c) c= rng vs then A2: len vs = (len c) + 1 by Def5; G -SVSet (rng c) c= rng vs proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G -SVSet (rng c) or y in rng vs ) assume y in G -SVSet (rng c) ; ::_thesis: y in rng vs then consider v being Element of G such that A3: v = y and A4: ex e being Element of the carrier' of G st ( e in rng c & v = the Source of G . e ) ; consider e being Element of the carrier' of G such that A5: e in rng c and A6: v = the Source of G . e by A4; consider x being set such that A7: x in dom c and A8: e = c . x by A5, FUNCT_1:def_3; reconsider x = x as Element of NAT by A7; A9: 1 <= x by A7, FINSEQ_3:25; A10: x <= len c by A7, FINSEQ_3:25; then A11: x <= len vs by A2, NAT_1:12; set v1 = vs /. x; set v2 = vs /. (x + 1); A12: vs /. x = vs . x by A9, A11, FINSEQ_4:15; c . x orientedly_joins vs /. x,vs /. (x + 1) by A1, A9, A10, Def5; then A13: v = vs /. x by A6, A8, Def1; x in dom vs by A9, A11, FINSEQ_3:25; hence y in rng vs by A3, A12, A13, FUNCT_1:def_3; ::_thesis: verum end; hence G -SVSet (rng c) c= rng vs ; ::_thesis: verum end; theorem :: GRAPH_4:6 for G being Graph for vs being FinSequence of the carrier of G for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds G -TVSet (rng c) c= rng vs proof let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds G -TVSet (rng c) c= rng vs let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds G -TVSet (rng c) c= rng vs let c be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c implies G -TVSet (rng c) c= rng vs ) assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: G -TVSet (rng c) c= rng vs then A2: len vs = (len c) + 1 by Def5; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G -TVSet (rng c) or y in rng vs ) assume y in G -TVSet (rng c) ; ::_thesis: y in rng vs then consider v being Element of G such that A3: v = y and A4: ex e being Element of the carrier' of G st ( e in rng c & v = the Target of G . e ) ; consider e being Element of the carrier' of G such that A5: e in rng c and A6: v = the Target of G . e by A4; consider x being set such that A7: x in dom c and A8: e = c . x by A5, FUNCT_1:def_3; reconsider x = x as Element of NAT by A7; A9: 1 <= x by A7, FINSEQ_3:25; A10: x <= len c by A7, FINSEQ_3:25; A11: 1 <= x + 1 by NAT_1:12; A12: x + 1 <= len vs by A2, A10, XREAL_1:7; set v1 = vs /. x; set v2 = vs /. (x + 1); A13: vs /. (x + 1) = vs . (x + 1) by A2, A10, A11, FINSEQ_4:15, XREAL_1:7; c . x orientedly_joins vs /. x,vs /. (x + 1) by A1, A9, A10, Def5; then A14: v = vs /. (x + 1) by A6, A8, Def1; x + 1 in dom vs by A11, A12, FINSEQ_3:25; hence y in rng vs by A3, A13, A14, FUNCT_1:def_3; ::_thesis: verum end; theorem :: GRAPH_4:7 for G being Graph for vs being FinSequence of the carrier of G for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c)) proof let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c)) let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c)) let c be oriented Chain of G; ::_thesis: ( c <> {} & vs is_oriented_vertex_seq_of c implies rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c)) ) assume that A1: c <> {} and A2: vs is_oriented_vertex_seq_of c ; ::_thesis: rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c)) A3: len vs = (len c) + 1 by A2, Def5; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng vs or y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) ) assume y in rng vs ; ::_thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) then consider x being set such that A4: x in dom vs and A5: y = vs . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A4; A6: 1 <= x by A4, FINSEQ_3:25; A7: x <= len vs by A4, FINSEQ_3:25; percases ( x <= len c or x = (len c) + 1 ) by A3, A7, NAT_1:8; supposeA8: x <= len c ; ::_thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) then x in dom c by A6, FINSEQ_3:25; then A9: c . x in rng c by FUNCT_1:def_3; rng c c= the carrier' of G by FINSEQ_1:def_4; then reconsider e = c . x as Element of the carrier' of G by A9; set v1 = vs /. x; set v2 = vs /. (x + 1); A10: vs /. x = vs . x by A6, A7, FINSEQ_4:15; c . x orientedly_joins vs /. x,vs /. (x + 1) by A2, A6, A8, Def5; then A11: vs /. x = the Source of G . e by Def1; x in dom c by A6, A8, FINSEQ_3:25; then e in rng c by FUNCT_1:def_3; then y in G -SVSet (rng c) by A5, A10, A11; hence y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) by XBOOLE_0:def_3; ::_thesis: verum end; supposeA12: x = (len c) + 1 ; ::_thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) set l = len c; 0 + 1 = 1 ; then A13: 1 <= len c by A1, NAT_1:13; then len c in dom c by FINSEQ_3:25; then A14: c . (len c) in rng c by FUNCT_1:def_3; rng c c= the carrier' of G by FINSEQ_1:def_4; then reconsider e = c . (len c) as Element of the carrier' of G by A14; set v1 = vs /. (len c); set v2 = vs /. ((len c) + 1); A15: vs /. ((len c) + 1) = vs . ((len c) + 1) by A3, A6, A12, FINSEQ_4:15; c . (len c) orientedly_joins vs /. (len c),vs /. ((len c) + 1) by A2, A13, Def5; then A16: vs /. ((len c) + 1) = the Target of G . e by Def1; len c in dom c by A13, FINSEQ_3:25; then e in rng c by FUNCT_1:def_3; then y in G -TVSet (rng c) by A5, A12, A15, A16; hence y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; begin theorem :: GRAPH_4:8 for G being Graph for v being Element of G holds <*v*> is_oriented_vertex_seq_of {} proof let G be Graph; ::_thesis: for v being Element of G holds <*v*> is_oriented_vertex_seq_of {} let v be Element of G; ::_thesis: <*v*> is_oriented_vertex_seq_of {} set c = {} ; thus len <*v*> = (len {}) + 1 by FINSEQ_1:40; :: according to GRAPH_4:def_5 ::_thesis: for n being Element of NAT st 1 <= n & n <= len {} holds {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len {} implies {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) ) assume that A1: 1 <= n and A2: n <= len {} ; ::_thesis: {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) thus {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) by A1, A2; ::_thesis: verum end; theorem Th9: :: GRAPH_4:9 for G being Graph for c being oriented Chain of G ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c proof let G be Graph; ::_thesis: for c being oriented Chain of G ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c let c be oriented Chain of G; ::_thesis: ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c now__::_thesis:_(_(_c_<>_{}_&_ex_vs_being_FinSequence_of_the_carrier_of_G_st_vs_is_oriented_vertex_seq_of_c_)_or_(_c_=_{}_&_ex_vs_being_FinSequence_of_the_carrier_of_G_st_vs_is_oriented_vertex_seq_of_c_)_) percases ( c <> {} or c = {} ) ; caseA1: c <> {} ; ::_thesis: ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c defpred S1[ Nat, set ] means ( ( \$1 = (len c) + 1 implies \$2 = the Target of G . (c . (len c)) ) & ( \$1 <> (len c) + 1 implies \$2 = the Source of G . (c . \$1) ) ); A2: for k being Nat st k in Seg ((len c) + 1) holds ex x being set st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg ((len c) + 1) implies ex x being set st S1[k,x] ) assume k in Seg ((len c) + 1) ; ::_thesis: ex x being set st S1[k,x] now__::_thesis:_(_(_k_=_(len_c)_+_1_&_ex_x_being_set_st_S1[k,x]_)_or_(_k_<>_(len_c)_+_1_&_ex_x_being_set_st_S1[k,x]_)_) percases ( k = (len c) + 1 or k <> (len c) + 1 ) ; case k = (len c) + 1 ; ::_thesis: ex x being set st S1[k,x] hence ex x being set st S1[k,x] ; ::_thesis: verum end; case k <> (len c) + 1 ; ::_thesis: ex x being set st S1[k,x] hence ex x being set st S1[k,x] ; ::_thesis: verum end; end; end; hence ex x being set st S1[k,x] ; ::_thesis: verum end; ex p being FinSequence st ( dom p = Seg ((len c) + 1) & ( for k being Nat st k in Seg ((len c) + 1) holds S1[k,p . k] ) ) from FINSEQ_1:sch_1(A2); then consider p being FinSequence such that A3: dom p = Seg ((len c) + 1) and A4: for k being Nat st k in Seg ((len c) + 1) holds ( ( k = (len c) + 1 implies p . k = the Target of G . (c . (len c)) ) & ( k <> (len c) + 1 implies p . k = the Source of G . (c . k) ) ) ; A5: len p = (len c) + 1 by A3, FINSEQ_1:def_3; rng p c= the carrier of G proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in the carrier of G ) assume y in rng p ; ::_thesis: y in the carrier of G then consider x being set such that A6: x in dom p and A7: y = p . x by FUNCT_1:def_3; reconsider k = x as Element of NAT by A6; A8: 1 <= k by A3, A6, FINSEQ_1:1; A9: k <= (len c) + 1 by A3, A6, FINSEQ_1:1; now__::_thesis:_(_(_k_=_(len_c)_+_1_&_y_in_the_carrier_of_G_)_or_(_k_<>_(len_c)_+_1_&_y_in_the_carrier_of_G_)_) percases ( k = (len c) + 1 or k <> (len c) + 1 ) ; case k = (len c) + 1 ; ::_thesis: y in the carrier of G then A10: y = the Target of G . (c . (len c)) by A3, A4, A6, A7; len c >= 0 + 1 by A1, NAT_1:13; then len c in Seg (len c) by FINSEQ_1:1; then len c in dom c by FINSEQ_1:def_3; then A11: c . (len c) in rng c by FUNCT_1:def_3; rng c c= the carrier' of G by FINSEQ_1:def_4; hence y in the carrier of G by A10, A11, FUNCT_2:5; ::_thesis: verum end; caseA12: k <> (len c) + 1 ; ::_thesis: y in the carrier of G then A13: y = the Source of G . (c . k) by A3, A4, A6, A7; k < (len c) + 1 by A9, A12, XXREAL_0:1; then k <= len c by NAT_1:13; then k in Seg (len c) by A8, FINSEQ_1:1; then k in dom c by FINSEQ_1:def_3; then A14: c . k in rng c by FUNCT_1:def_3; rng c c= the carrier' of G by FINSEQ_1:def_4; hence y in the carrier of G by A13, A14, FUNCT_2:5; ::_thesis: verum end; end; end; hence y in the carrier of G ; ::_thesis: verum end; then reconsider vs = p as FinSequence of the carrier of G by FINSEQ_1:def_4; for n being Element of NAT st 1 <= n & n <= len c holds c . n orientedly_joins vs /. n,vs /. (n + 1) proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len c implies c . n orientedly_joins vs /. n,vs /. (n + 1) ) assume that A15: 1 <= n and A16: n <= len c ; ::_thesis: c . n orientedly_joins vs /. n,vs /. (n + 1) percases ( n = len c or n <> len c ) ; supposeA17: n = len c ; ::_thesis: c . n orientedly_joins vs /. n,vs /. (n + 1) then A18: n < (len c) + 1 by NAT_1:13; then n in Seg ((len c) + 1) by A15, FINSEQ_1:1; then A19: p . n = the Source of G . (c . n) by A4, A18; 1 < n + 1 by A15, NAT_1:13; then n + 1 in Seg ((len c) + 1) by A17, FINSEQ_1:1; then A20: p . (n + 1) = the Target of G . (c . (len c)) by A4, A17; A21: the Source of G . (c . n) = vs /. n by A5, A15, A18, A19, FINSEQ_4:15; 1 < n + 1 by A15, NAT_1:13; then the Target of G . (c . n) = vs /. (n + 1) by A5, A17, A20, FINSEQ_4:15; hence c . n orientedly_joins vs /. n,vs /. (n + 1) by A21, Def1; ::_thesis: verum end; suppose n <> len c ; ::_thesis: c . n orientedly_joins vs /. n,vs /. (n + 1) then A22: n < len c by A16, XXREAL_0:1; then n + 1 <= len c by NAT_1:13; then A23: n + 1 < (len c) + 1 by NAT_1:13; A24: n < (len c) + 1 by A16, NAT_1:13; then n in Seg ((len c) + 1) by A15, FINSEQ_1:1; then A25: p . n = the Source of G . (c . n) by A4, A24; 1 < n + 1 by A15, NAT_1:13; then n + 1 in Seg ((len c) + 1) by A23, FINSEQ_1:1; then A26: p . (n + 1) = the Source of G . (c . (n + 1)) by A4, A23; A27: the Source of G . (c . n) = vs /. n by A5, A15, A24, A25, FINSEQ_4:15; 1 < n + 1 by A15, NAT_1:13; then vs /. (n + 1) = p . (n + 1) by A5, A23, FINSEQ_4:15; then the Target of G . (c . n) = vs /. (n + 1) by A15, A22, A26, GRAPH_1:def_15; hence c . n orientedly_joins vs /. n,vs /. (n + 1) by A27, Def1; ::_thesis: verum end; end; end; then vs is_oriented_vertex_seq_of c by A5, Def5; hence ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c ; ::_thesis: verum end; caseA28: c = {} ; ::_thesis: ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c set x = the Element of G; set vs = <* the Element of G*>; len c = 0 by A28; then A29: len <* the Element of G*> = (len c) + 1 by FINSEQ_1:40; for n being Element of NAT st 1 <= n & n <= len c holds c . n orientedly_joins <* the Element of G*> /. n,<* the Element of G*> /. (n + 1) by A28; then <* the Element of G*> is_oriented_vertex_seq_of c by A29, Def5; hence ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c ; ::_thesis: verum end; end; end; hence ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c ; ::_thesis: verum end; theorem Th10: :: GRAPH_4:10 for G being Graph for vs1, vs2 being FinSequence of the carrier of G for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds vs1 = vs2 proof let G be Graph; ::_thesis: for vs1, vs2 being FinSequence of the carrier of G for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds vs1 = vs2 let vs1, vs2 be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds vs1 = vs2 let c be oriented Chain of G; ::_thesis: ( c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c implies vs1 = vs2 ) assume that A1: c <> {} and A2: vs1 is_oriented_vertex_seq_of c and A3: vs2 is_oriented_vertex_seq_of c ; ::_thesis: vs1 = vs2 A4: len vs1 = (len c) + 1 by A2, Def5; A5: len vs2 = (len c) + 1 by A3, Def5; for n being Nat st 1 <= n & n <= len vs1 holds vs1 . n = vs2 . n proof let n be Nat; ::_thesis: ( 1 <= n & n <= len vs1 implies vs1 . n = vs2 . n ) assume that A6: 1 <= n and A7: n <= len vs1 ; ::_thesis: vs1 . n = vs2 . n A8: n <= (len c) + 1 by A2, A7, Def5; A9: n in NAT by ORDINAL1:def_12; percases ( n < (len c) + 1 or n >= (len c) + 1 ) ; suppose n < (len c) + 1 ; ::_thesis: vs1 . n = vs2 . n then A10: n <= len c by NAT_1:13; then c . n orientedly_joins vs1 /. n,vs1 /. (n + 1) by A2, A6, A9, Def5; then A11: the Source of G . (c . n) = vs1 /. n by Def1; c . n orientedly_joins vs2 /. n,vs2 /. (n + 1) by A3, A6, A9, A10, Def5; then A12: the Source of G . (c . n) = vs2 /. n by Def1; vs1 . n = vs1 /. n by A6, A7, FINSEQ_4:15; hence vs1 . n = vs2 . n by A4, A5, A6, A7, A11, A12, FINSEQ_4:15; ::_thesis: verum end; suppose n >= (len c) + 1 ; ::_thesis: vs1 . n = vs2 . n then A13: n = (len c) + 1 by A8, XXREAL_0:1; then A14: n - 1 = len c ; A15: 0 + 1 <= len c by A1, NAT_1:13; then A16: n - 1 = n -' 1 by A13, NAT_D:39; A17: n -' 1 = len c by A14, A15, NAT_D:39; then c . (n -' 1) orientedly_joins vs1 /. (n -' 1),vs1 /. ((n -' 1) + 1) by A2, A15, Def5; then A18: the Target of G . (c . (n -' 1)) = vs1 /. ((n -' 1) + 1) by Def1; c . (n -' 1) orientedly_joins vs2 /. (n -' 1),vs2 /. ((n -' 1) + 1) by A3, A15, A17, Def5; then A19: the Target of G . (c . (n -' 1)) = vs2 /. ((n -' 1) + 1) by Def1; vs1 . n = vs1 /. n by A6, A7, FINSEQ_4:15; hence vs1 . n = vs2 . n by A4, A5, A6, A7, A16, A18, A19, FINSEQ_4:15; ::_thesis: verum end; end; end; hence vs1 = vs2 by A4, A5, FINSEQ_1:14; ::_thesis: verum end; definition let G be Graph; let c be oriented Chain of G; assume A1: c <> {} ; func oriented-vertex-seq c -> FinSequence of the carrier of G means :: GRAPH_4:def 6 it is_oriented_vertex_seq_of c; existence ex b1 being FinSequence of the carrier of G st b1 is_oriented_vertex_seq_of c by Th9; uniqueness for b1, b2 being FinSequence of the carrier of G st b1 is_oriented_vertex_seq_of c & b2 is_oriented_vertex_seq_of c holds b1 = b2 by A1, Th10; end; :: deftheorem defines oriented-vertex-seq GRAPH_4:def_6_:_ for G being Graph for c being oriented Chain of G st c <> {} holds for b3 being FinSequence of the carrier of G holds ( b3 = oriented-vertex-seq c iff b3 is_oriented_vertex_seq_of c ); theorem :: GRAPH_4:11 for n being Element of NAT for G being Graph for vs, vs1 being FinSequence of the carrier of G for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds vs1 is_oriented_vertex_seq_of c1 proof let n be Element of NAT ; ::_thesis: for G being Graph for vs, vs1 being FinSequence of the carrier of G for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds vs1 is_oriented_vertex_seq_of c1 let G be Graph; ::_thesis: for vs, vs1 being FinSequence of the carrier of G for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds vs1 is_oriented_vertex_seq_of c1 let vs, vs1 be FinSequence of the carrier of G; ::_thesis: for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds vs1 is_oriented_vertex_seq_of c1 let c, c1 be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) implies vs1 is_oriented_vertex_seq_of c1 ) assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: ( not c1 = c | (Seg n) or not vs1 = vs | (Seg (n + 1)) or vs1 is_oriented_vertex_seq_of c1 ) then A2: len vs = (len c) + 1 by Def5; assume that A3: c1 = c | (Seg n) and A4: vs1 = vs | (Seg (n + 1)) ; ::_thesis: vs1 is_oriented_vertex_seq_of c1 now__::_thesis:_(_len_vs1_=_(len_c1)_+_1_&_(_for_k_being_Element_of_NAT_st_1_<=_k_&_k_<=_len_c1_holds_ c1_._k_orientedly_joins_vs1_/._k,vs1_/._(k_+_1)_)_) percases ( n <= len c or len c <= n ) ; supposeA5: n <= len c ; ::_thesis: ( len vs1 = (len c1) + 1 & ( for k being Element of NAT st 1 <= k & k <= len c1 holds c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) ) then A6: n + 1 <= len vs by A2, XREAL_1:6; A7: len c1 = n by A3, A5, FINSEQ_1:17; A8: len vs1 = n + 1 by A4, A6, FINSEQ_1:17; thus len vs1 = (len c1) + 1 by A4, A6, A7, FINSEQ_1:17; ::_thesis: for k being Element of NAT st 1 <= k & k <= len c1 holds c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len c1 implies c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) assume that A9: 1 <= k and A10: k <= len c1 ; ::_thesis: c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) A11: k <= len c by A5, A7, A10, XXREAL_0:2; k in Seg n by A7, A9, A10, FINSEQ_1:1; then A12: c1 . k = c . k by A3, FUNCT_1:49; A13: k <= len vs by A2, A11, NAT_1:12; A14: k <= n + 1 by A7, A10, NAT_1:12; then A15: k in Seg (n + 1) by A9, FINSEQ_1:1; A16: 1 <= k + 1 by NAT_1:12; k + 1 <= (len c1) + 1 by A10, XREAL_1:7; then A17: k + 1 in Seg (n + 1) by A7, A16, FINSEQ_1:1; A18: vs1 . k = vs . k by A4, A15, FUNCT_1:49; A19: vs1 . (k + 1) = vs . (k + 1) by A4, A17, FUNCT_1:49; A20: vs /. k = vs . k by A9, A13, FINSEQ_4:15; A21: vs /. (k + 1) = vs . (k + 1) by A2, A11, A16, FINSEQ_4:15, XREAL_1:7; A22: vs1 /. k = vs1 . k by A8, A9, A14, FINSEQ_4:15; vs1 /. (k + 1) = vs1 . (k + 1) by A7, A8, A10, A16, FINSEQ_4:15, XREAL_1:7; hence c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) by A1, A9, A11, A12, A18, A19, A20, A21, A22, Def5; ::_thesis: verum end; supposeA23: len c <= n ; ::_thesis: ( len vs1 = (len c1) + 1 & ( for k being Element of NAT st 1 <= k & k <= len c1 holds c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) ) then A24: len vs <= n + 1 by A2, XREAL_1:6; A25: c1 = c by A3, A23, FINSEQ_2:20; vs1 = vs by A4, A24, FINSEQ_2:20; hence ( len vs1 = (len c1) + 1 & ( for k being Element of NAT st 1 <= k & k <= len c1 holds c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) ) by A1, A25, Def5; ::_thesis: verum end; end; end; hence vs1 is_oriented_vertex_seq_of c1 by Def5; ::_thesis: verum end; theorem Th12: :: GRAPH_4:12 for q being FinSequence for m, n being Element of NAT for G being Graph for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds q is oriented Chain of G proof let q be FinSequence; ::_thesis: for m, n being Element of NAT for G being Graph for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds q is oriented Chain of G let m, n be Element of NAT ; ::_thesis: for G being Graph for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds q is oriented Chain of G let G be Graph; ::_thesis: for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds q is oriented Chain of G let c be oriented Chain of G; ::_thesis: ( 1 <= m & m <= n & n <= len c & q = (m,n) -cut c implies q is oriented Chain of G ) assume that A1: 1 <= m and A2: m <= n and A3: n <= len c and A4: q = (m,n) -cut c ; ::_thesis: q is oriented Chain of G consider vs being FinSequence of the carrier of G such that A5: vs is_oriented_vertex_seq_of c by Th9; A6: ((len q) + m) - m = (n + 1) - m by A1, A2, A3, A4, GRAPH_2:def_1; reconsider qq = q as Chain of G by A1, A2, A3, A4, GRAPH_2:41; for n being Element of NAT st 1 <= n & n < len q holds the Source of G . (q . (n + 1)) = the Target of G . (q . n) proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k < len q implies the Source of G . (q . (k + 1)) = the Target of G . (q . k) ) assume that A7: 1 <= k and A8: k < len q ; ::_thesis: the Source of G . (q . (k + 1)) = the Target of G . (q . k) 1 - 1 <= m - 1 by A1, XREAL_1:9; then m - 1 = m -' 1 by XREAL_0:def_2; then reconsider m1 = m - 1 as Element of NAT ; reconsider i = m1 + k as Element of NAT ; set v1 = vs /. i; set v2 = vs /. (i + 1); 0 + 1 <= k by A7; then consider j being Element of NAT such that 0 <= j and A9: j < len q and A10: k = j + 1 by A8, GRAPH_2:1; A11: i = m + j by A10; i + 1 = m + (j + 1) by A10; then A12: c . (i + 1) = q . (k + 1) by A1, A2, A3, A4, A8, GRAPH_2:def_1; A13: c . i = q . k by A1, A2, A3, A4, A9, A10, A11, GRAPH_2:def_1; 1 - 1 <= m - 1 by A1, XREAL_1:9; then A14: 0 + 1 <= (m - 1) + k by A7, XREAL_1:7; i <= (m - 1) + (n - (m - 1)) by A6, A8, XREAL_1:6; then i <= len c by A3, XXREAL_0:2; then c . i orientedly_joins vs /. i,vs /. (i + 1) by A5, A14, Def5; then A15: the Target of G . (c . i) = vs /. (i + 1) by Def1; A16: 1 < i + 1 by A14, NAT_1:13; k + m < n + 1 by A6, A8, XREAL_1:6; then k + m <= n by NAT_1:13; then m + k <= len c by A3, XXREAL_0:2; then c . (i + 1) orientedly_joins vs /. (i + 1),vs /. ((i + 1) + 1) by A5, A16, Def5; hence the Source of G . (q . (k + 1)) = the Target of G . (q . k) by A12, A13, A15, Def1; ::_thesis: verum end; then qq is oriented by GRAPH_1:def_15; hence q is oriented Chain of G ; ::_thesis: verum end; theorem Th13: :: GRAPH_4:13 for m, n being Element of NAT for G being Graph for vs, vs1 being FinSequence of the carrier of G for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds vs1 is_oriented_vertex_seq_of c1 proof let m, n be Element of NAT ; ::_thesis: for G being Graph for vs, vs1 being FinSequence of the carrier of G for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds vs1 is_oriented_vertex_seq_of c1 let G be Graph; ::_thesis: for vs, vs1 being FinSequence of the carrier of G for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds vs1 is_oriented_vertex_seq_of c1 let vs, vs1 be FinSequence of the carrier of G; ::_thesis: for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds vs1 is_oriented_vertex_seq_of c1 let c, c1 be oriented Chain of G; ::_thesis: ( 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs implies vs1 is_oriented_vertex_seq_of c1 ) assume that A1: 1 <= m and A2: m <= n and A3: n <= len c ; ::_thesis: ( not c1 = (m,n) -cut c or not vs is_oriented_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_oriented_vertex_seq_of c1 ) assume A4: c1 = (m,n) -cut c ; ::_thesis: ( not vs is_oriented_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_oriented_vertex_seq_of c1 ) assume that A5: vs is_oriented_vertex_seq_of c and A6: vs1 = (m,(n + 1)) -cut vs ; ::_thesis: vs1 is_oriented_vertex_seq_of c1 A7: len vs = (len c) + 1 by A5, Def5; A8: m <= n + 1 by A2, NAT_1:12; A9: n + 1 <= len vs by A3, A7, XREAL_1:6; A10: (len c1) + m = n + 1 by A1, A2, A3, A4, GRAPH_2:def_1; (len vs1) + m = (n + 1) + 1 by A1, A6, A8, A9, GRAPH_2:def_1; hence A11: len vs1 = (len c1) + 1 by A10; :: according to GRAPH_4:def_5 ::_thesis: for n being Element of NAT st 1 <= n & n <= len c1 holds c1 . n orientedly_joins vs1 /. n,vs1 /. (n + 1) let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len c1 implies c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) assume that A12: 1 <= k and A13: k <= len c1 ; ::_thesis: c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) 0 + 1 <= k by A12; then consider j being Element of NAT such that 0 <= j and A14: j < len c1 and A15: k = j + 1 by A13, GRAPH_2:1; set i = m + j; set v1 = vs /. (m + j); set v2 = vs /. ((m + j) + 1); m + k <= (len c1) + m by A13, XREAL_1:7; then A16: ((m + j) + 1) - 1 <= ((len c1) + m) - 1 by A15, XREAL_1:9; A17: 1 <= m + j by A1, NAT_1:12; A18: m + j <= len c by A3, A10, A16, XXREAL_0:2; then A19: c . (m + j) orientedly_joins vs /. (m + j),vs /. ((m + j) + 1) by A5, A17, Def5; j < len vs1 by A11, A14, NAT_1:13; then A20: vs1 . k = vs . (m + j) by A1, A6, A8, A9, A15, GRAPH_2:def_1; A21: j + 1 < len vs1 by A11, A14, XREAL_1:6; (m + j) + 1 = m + (j + 1) ; then A22: vs1 . (k + 1) = vs . ((m + j) + 1) by A1, A6, A8, A9, A15, A21, GRAPH_2:def_1; A23: m + j <= len vs by A7, A18, NAT_1:12; A24: 1 <= (m + j) + 1 by NAT_1:12; A25: vs /. (m + j) = vs . (m + j) by A1, A23, FINSEQ_4:15, NAT_1:12; A26: vs /. ((m + j) + 1) = vs . ((m + j) + 1) by A7, A18, A24, FINSEQ_4:15, XREAL_1:7; 0 + 1 = 1 ; then A27: 1 <= k by A15, NAT_1:13; A28: k <= len c1 by A14, A15, NAT_1:13; then A29: k <= len vs1 by A11, NAT_1:12; A30: 1 <= k + 1 by NAT_1:12; A31: vs1 /. k = vs1 . k by A27, A29, FINSEQ_4:15; vs1 /. (k + 1) = vs1 . (k + 1) by A11, A28, A30, FINSEQ_4:15, XREAL_1:7; hence c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) by A1, A2, A3, A4, A14, A15, A19, A20, A22, A25, A26, A31, GRAPH_2:def_1; ::_thesis: verum end; theorem Th14: :: GRAPH_4:14 for G being Graph for vs1, vs2 being FinSequence of the carrier of G for c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds c1 ^ c2 is oriented Chain of G proof let G be Graph; ::_thesis: for vs1, vs2 being FinSequence of the carrier of G for c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds c1 ^ c2 is oriented Chain of G let vs1, vs2 be FinSequence of the carrier of G; ::_thesis: for c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds c1 ^ c2 is oriented Chain of G let c1, c2 be oriented Chain of G; ::_thesis: ( vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 implies c1 ^ c2 is oriented Chain of G ) assume that A1: vs1 is_oriented_vertex_seq_of c1 and A2: vs2 is_oriented_vertex_seq_of c2 and A3: vs1 . (len vs1) = vs2 . 1 ; ::_thesis: c1 ^ c2 is oriented Chain of G A4: vs1 is_vertex_seq_of c1 by A1, Th4; A5: vs2 is_vertex_seq_of c2 by A2, Th4; A6: len vs1 = (len c1) + 1 by A1, Def5; A7: len vs2 = (len c2) + 1 by A2, Def5; set q = c1 ^ c2; set p = vs1 ^' vs2; thus c1 ^ c2 is oriented Chain of G ::_thesis: verum proof reconsider cc = c1 ^ c2 as Chain of G by A3, A4, A5, GRAPH_2:43; for n being Element of NAT st 1 <= n & n < len (c1 ^ c2) holds the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n) proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len (c1 ^ c2) implies the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n) ) assume that A8: 1 <= n and A9: n < len (c1 ^ c2) ; ::_thesis: the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n) A10: n in dom (c1 ^ c2) by A8, A9, FINSEQ_3:25; A11: n + 1 <= len (c1 ^ c2) by A9, NAT_1:13; A12: 1 < n + 1 by A8, NAT_1:13; now__::_thesis:_(_(_n_in_dom_c1_&_ex_v1,_v2_being_Element_of_G_st_ (_v1_=_(vs1_^'_vs2)_._n_&_v2_=_(vs1_^'_vs2)_._(n_+_1)_&_(c1_^_c2)_._n_orientedly_joins_v1,v2_)_)_or_(_ex_k_being_Nat_st_ (_k_in_dom_c2_&_n_=_(len_c1)_+_k_)_&_ex_v1,_v2_being_Element_of_G_st_ (_v1_=_(vs1_^'_vs2)_._n_&_v2_=_(vs1_^'_vs2)_._(n_+_1)_&_(c1_^_c2)_._n_orientedly_joins_v1,v2_)_)_) percases ( n in dom c1 or ex k being Nat st ( k in dom c2 & n = (len c1) + k ) ) by A10, FINSEQ_1:25; caseA13: n in dom c1 ; ::_thesis: ex v1, v2 being Element of G st ( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) then A14: (c1 ^ c2) . n = c1 . n by FINSEQ_1:def_7; set v1 = vs1 /. n; set v2 = vs1 /. (n + 1); A15: 1 <= n by A13, FINSEQ_3:25; A16: n <= len c1 by A13, FINSEQ_3:25; then A17: c1 . n orientedly_joins vs1 /. n,vs1 /. (n + 1) by A1, A15, Def5; A18: n <= len vs1 by A6, A16, NAT_1:12; n + 1 <= (len c1) + 1 by A16, XREAL_1:6; then A19: n + 1 <= len vs1 by A1, Def5; A20: vs1 /. n = vs1 . n by A15, A18, FINSEQ_4:15; A21: vs1 /. (n + 1) = vs1 . (n + 1) by A19, FINSEQ_4:15, NAT_1:12; A22: (vs1 ^' vs2) . n = vs1 . n by A15, A18, GRAPH_2:14; (vs1 ^' vs2) . (n + 1) = vs1 . (n + 1) by A19, GRAPH_2:14, NAT_1:12; hence ex v1, v2 being Element of G st ( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) by A14, A17, A20, A21, A22; ::_thesis: verum end; case ex k being Nat st ( k in dom c2 & n = (len c1) + k ) ; ::_thesis: ex v1, v2 being Element of G st ( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) then consider k being Nat such that A23: k in dom c2 and A24: n = (len c1) + k ; reconsider k = k as Element of NAT by ORDINAL1:def_12; A25: (c1 ^ c2) . n = c2 . k by A23, A24, FINSEQ_1:def_7; A26: 1 <= k by A23, FINSEQ_3:25; A27: k <= len c2 by A23, FINSEQ_3:25; A28: 1 <= k + 1 by NAT_1:12; A29: k <= len vs2 by A7, A27, NAT_1:12; set v1 = vs2 /. k; set v2 = vs2 /. (k + 1); A30: vs2 /. k = vs2 . k by A26, A29, FINSEQ_4:15; A31: vs2 /. (k + 1) = vs2 . (k + 1) by A7, A27, A28, FINSEQ_4:15, XREAL_1:7; A32: c2 . k orientedly_joins vs2 /. k,vs2 /. (k + 1) by A2, A26, A27, Def5; A33: k <= len vs2 by A7, A27, NAT_1:12; 0 + 1 <= k by A23, FINSEQ_3:25; then consider j being Element of NAT such that 0 <= j and A34: j < len vs2 and A35: k = j + 1 by A33, GRAPH_2:1; A36: (vs1 ^' vs2) . n = vs2 . k proof percases ( 1 = k or 1 < k ) by A26, XXREAL_0:1; supposeA37: 1 = k ; ::_thesis: (vs1 ^' vs2) . n = vs2 . k A38: 0 + 1 <= len vs1 by A6, NAT_1:13; thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . (len vs1) by A1, A24, A37, Def5 .= vs2 . k by A3, A37, A38, GRAPH_2:14 ; ::_thesis: verum end; suppose 1 < k ; ::_thesis: (vs1 ^' vs2) . n = vs2 . k then A39: 1 <= j by A35, NAT_1:13; thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . (((len c1) + 1) + j) by A24, A35 .= (vs1 ^' vs2) . ((len vs1) + j) by A1, Def5 .= vs2 . k by A34, A35, A39, GRAPH_2:15 ; ::_thesis: verum end; end; end; A40: k < len vs2 by A7, A27, NAT_1:13; (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + k) by A24 .= (vs1 ^' vs2) . ((len vs1) + k) by A1, Def5 .= vs2 . (k + 1) by A26, A40, GRAPH_2:15 ; hence ex v1, v2 being Element of G st ( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) by A25, A30, A31, A32, A36; ::_thesis: verum end; end; end; then consider v1, v2 being Element of G such that v1 = (vs1 ^' vs2) . n and A41: v2 = (vs1 ^' vs2) . (n + 1) and A42: (c1 ^ c2) . n orientedly_joins v1,v2 ; A43: n + 1 in dom (c1 ^ c2) by A11, A12, FINSEQ_3:25; A44: now__::_thesis:_(_(_n_+_1_in_dom_c1_&_ex_v299,_v39_being_Element_of_G_st_ (_v299_=_(vs1_^'_vs2)_._(n_+_1)_&_v39_=_(vs1_^'_vs2)_._((n_+_1)_+_1)_&_(c1_^_c2)_._(n_+_1)_orientedly_joins_v299,v39_)_)_or_(_ex_k_being_Nat_st_ (_k_in_dom_c2_&_n_+_1_=_(len_c1)_+_k_)_&_ex_v299,_v39_being_Element_of_G_st_ (_v299_=_(vs1_^'_vs2)_._(n_+_1)_&_v39_=_(vs1_^'_vs2)_._((n_+_1)_+_1)_&_(c1_^_c2)_._(n_+_1)_orientedly_joins_v299,v39_)_)_) percases ( n + 1 in dom c1 or ex k being Nat st ( k in dom c2 & n + 1 = (len c1) + k ) ) by A43, FINSEQ_1:25; caseA45: n + 1 in dom c1 ; ::_thesis: ex v299, v39 being Element of G st ( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 ) then A46: (c1 ^ c2) . (n + 1) = c1 . (n + 1) by FINSEQ_1:def_7; set v29 = vs1 /. (n + 1); set v3 = vs1 /. ((n + 1) + 1); A47: 1 <= n + 1 by A45, FINSEQ_3:25; A48: n + 1 <= len c1 by A45, FINSEQ_3:25; then A49: c1 . (n + 1) orientedly_joins vs1 /. (n + 1),vs1 /. ((n + 1) + 1) by A1, A47, Def5; A50: n + 1 <= len vs1 by A6, A48, NAT_1:12; (n + 1) + 1 <= (len c1) + 1 by A48, XREAL_1:6; then A51: (n + 1) + 1 <= len vs1 by A1, Def5; A52: vs1 /. (n + 1) = vs1 . (n + 1) by A47, A50, FINSEQ_4:15; A53: vs1 /. ((n + 1) + 1) = vs1 . ((n + 1) + 1) by A51, FINSEQ_4:15, NAT_1:12; A54: (vs1 ^' vs2) . (n + 1) = vs1 . (n + 1) by A47, A50, GRAPH_2:14; (vs1 ^' vs2) . ((n + 1) + 1) = vs1 . ((n + 1) + 1) by A51, GRAPH_2:14, NAT_1:12; hence ex v299, v39 being Element of G st ( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 ) by A46, A49, A52, A53, A54; ::_thesis: verum end; case ex k being Nat st ( k in dom c2 & n + 1 = (len c1) + k ) ; ::_thesis: ex v299, v39 being Element of G st ( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 ) then consider k being Nat such that A55: k in dom c2 and A56: n + 1 = (len c1) + k ; reconsider k = k as Element of NAT by ORDINAL1:def_12; A57: (c1 ^ c2) . (n + 1) = c2 . k by A55, A56, FINSEQ_1:def_7; A58: 1 <= k by A55, FINSEQ_3:25; A59: k <= len c2 by A55, FINSEQ_3:25; A60: 1 <= k + 1 by NAT_1:12; A61: k <= len vs2 by A7, A59, NAT_1:12; set v29 = vs2 /. k; set v3 = vs2 /. (k + 1); A62: vs2 /. k = vs2 . k by A58, A61, FINSEQ_4:15; A63: vs2 /. (k + 1) = vs2 . (k + 1) by A7, A59, A60, FINSEQ_4:15, XREAL_1:7; A64: c2 . k orientedly_joins vs2 /. k,vs2 /. (k + 1) by A2, A58, A59, Def5; A65: k <= len vs2 by A7, A59, NAT_1:12; 0 + 1 <= k by A55, FINSEQ_3:25; then consider j being Element of NAT such that 0 <= j and A66: j < len vs2 and A67: k = j + 1 by A65, GRAPH_2:1; A68: (vs1 ^' vs2) . (n + 1) = vs2 . k proof percases ( 1 = k or 1 < k ) by A58, XXREAL_0:1; supposeA69: 1 = k ; ::_thesis: (vs1 ^' vs2) . (n + 1) = vs2 . k A70: 0 + 1 <= len vs1 by A6, NAT_1:13; thus (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (len vs1) by A1, A56, A69, Def5 .= vs2 . k by A3, A69, A70, GRAPH_2:14 ; ::_thesis: verum end; suppose 1 < k ; ::_thesis: (vs1 ^' vs2) . (n + 1) = vs2 . k then A71: 1 <= j by A67, NAT_1:13; thus (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + j) by A56, A67 .= (vs1 ^' vs2) . ((len vs1) + j) by A1, Def5 .= vs2 . k by A66, A67, A71, GRAPH_2:15 ; ::_thesis: verum end; end; end; A72: k < len vs2 by A7, A59, NAT_1:13; (vs1 ^' vs2) . ((n + 1) + 1) = (vs1 ^' vs2) . (((len c1) + 1) + k) by A56 .= (vs1 ^' vs2) . ((len vs1) + k) by A1, Def5 .= vs2 . (k + 1) by A58, A72, GRAPH_2:15 ; hence ex v299, v39 being Element of G st ( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 ) by A57, A62, A63, A64, A68; ::_thesis: verum end; end; end; the Target of G . ((c1 ^ c2) . n) = v2 by A42, Def1; hence the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n) by A41, A44, Def1; ::_thesis: verum end; then cc is oriented by GRAPH_1:def_15; hence c1 ^ c2 is oriented Chain of G ; ::_thesis: verum end; end; theorem Th15: :: GRAPH_4:15 for G being Graph for vs1, vs2, vs being FinSequence of the carrier of G for c1, c2, c being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds vs is_oriented_vertex_seq_of c proof let G be Graph; ::_thesis: for vs1, vs2, vs being FinSequence of the carrier of G for c1, c2, c being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds vs is_oriented_vertex_seq_of c let vs1, vs2, vs be FinSequence of the carrier of G; ::_thesis: for c1, c2, c being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds vs is_oriented_vertex_seq_of c let c1, c2, c be oriented Chain of G; ::_thesis: ( vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 implies vs is_oriented_vertex_seq_of c ) assume that A1: vs1 is_oriented_vertex_seq_of c1 and A2: vs2 is_oriented_vertex_seq_of c2 and A3: vs1 . (len vs1) = vs2 . 1 ; ::_thesis: ( not c = c1 ^ c2 or not vs = vs1 ^' vs2 or vs is_oriented_vertex_seq_of c ) assume that A4: c = c1 ^ c2 and A5: vs = vs1 ^' vs2 ; ::_thesis: vs is_oriented_vertex_seq_of c A6: len vs1 = (len c1) + 1 by A1, Def5; A7: len vs2 = (len c2) + 1 by A2, Def5; then A8: vs2 <> {} ; set q = c1 ^ c2; set p = vs1 ^' vs2; (len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2) by A8, GRAPH_2:13; then A9: len (vs1 ^' vs2) = ((len c1) + (len c2)) + 1 by A6, A7 .= (len (c1 ^ c2)) + 1 by FINSEQ_1:22 ; reconsider p = vs1 ^' vs2 as FinSequence of the carrier of G ; now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_(c1_^_c2)_holds_ (c1_^_c2)_._n_orientedly_joins_p_/._n,p_/._(n_+_1) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1) ) assume that A10: 1 <= n and A11: n <= len (c1 ^ c2) ; ::_thesis: (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1) A12: n <= len p by A9, A11, NAT_1:12; A13: 1 <= n + 1 by NAT_1:12; A14: p /. n = p . n by A10, A12, FINSEQ_4:15; A15: p /. (n + 1) = p . (n + 1) by A9, A11, A13, FINSEQ_4:15, XREAL_1:7; A16: n in dom (c1 ^ c2) by A10, A11, FINSEQ_3:25; percases ( n in dom c1 or ex k being Nat st ( k in dom c2 & n = (len c1) + k ) ) by A16, FINSEQ_1:25; supposeA17: n in dom c1 ; ::_thesis: (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1) set v1 = vs1 /. n; set v2 = vs1 /. (n + 1); A18: 1 <= n by A17, FINSEQ_3:25; A19: n <= len c1 by A17, FINSEQ_3:25; then A20: c1 . n orientedly_joins vs1 /. n,vs1 /. (n + 1) by A1, A18, Def5; A21: n <= len vs1 by A6, A19, NAT_1:12; n + 1 <= (len c1) + 1 by A19, XREAL_1:6; then A22: n + 1 <= len vs1 by A1, Def5; A23: vs1 /. n = vs1 . n by A18, A21, FINSEQ_4:15; A24: vs1 /. (n + 1) = vs1 . (n + 1) by A22, FINSEQ_4:15, NAT_1:12; A25: p . n = vs1 . n by A18, A21, GRAPH_2:14; p . (n + 1) = vs1 . (n + 1) by A22, GRAPH_2:14, NAT_1:12; hence (c1 ^ c2) . n orientedly_joins p /. n,p /. (n + 1) by A14, A15, A17, A20, A23, A24, A25, FINSEQ_1:def_7; ::_thesis: verum end; suppose ex k being Nat st ( k in dom c2 & n = (len c1) + k ) ; ::_thesis: (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1) then consider k being Nat such that A26: k in dom c2 and A27: n = (len c1) + k ; reconsider k = k as Element of NAT by ORDINAL1:def_12; A28: (c1 ^ c2) . n = c2 . k by A26, A27, FINSEQ_1:def_7; A29: 1 <= k by A26, FINSEQ_3:25; A30: k <= len c2 by A26, FINSEQ_3:25; A31: 1 <= k + 1 by NAT_1:12; k <= len vs2 by A7, A30, NAT_1:12; then A32: vs2 /. k = vs2 . k by A29, FINSEQ_4:15; A33: vs2 /. (k + 1) = vs2 . (k + 1) by A7, A30, A31, FINSEQ_4:15, XREAL_1:7; A34: k <= len vs2 by A7, A30, NAT_1:12; 0 + 1 <= k by A26, FINSEQ_3:25; then consider j being Element of NAT such that 0 <= j and A35: j < len vs2 and A36: k = j + 1 by A34, GRAPH_2:1; A37: p . n = vs2 . k proof percases ( 1 = k or 1 < k ) by A29, XXREAL_0:1; supposeA38: 1 = k ; ::_thesis: p . n = vs2 . k A39: 0 + 1 <= len vs1 by A6, NAT_1:13; thus p . n = p . (len vs1) by A1, A27, A38, Def5 .= vs2 . k by A3, A38, A39, GRAPH_2:14 ; ::_thesis: verum end; suppose 1 < k ; ::_thesis: p . n = vs2 . k then A40: 1 <= j by A36, NAT_1:13; thus p . n = p . (((len c1) + 1) + j) by A27, A36 .= p . ((len vs1) + j) by A1, Def5 .= vs2 . k by A35, A36, A40, GRAPH_2:15 ; ::_thesis: verum end; end; end; A41: k < len vs2 by A7, A30, NAT_1:13; p . (n + 1) = p . (((len c1) + 1) + k) by A27 .= p . ((len vs1) + k) by A1, Def5 .= vs2 . (k + 1) by A29, A41, GRAPH_2:15 ; hence (c1 ^ c2) . n orientedly_joins p /. n,p /. (n + 1) by A2, A14, A15, A28, A29, A30, A32, A33, A37, Def5; ::_thesis: verum end; end; end; hence vs is_oriented_vertex_seq_of c by A4, A5, A9, Def5; ::_thesis: verum end; begin Lm1: for G being Graph for v being Element of G holds <*v*> is_oriented_vertex_seq_of {} proof let G be Graph; ::_thesis: for v being Element of G holds <*v*> is_oriented_vertex_seq_of {} let v be Element of G; ::_thesis: <*v*> is_oriented_vertex_seq_of {} set p = <*v*>; set ec = {} ; A1: len <*v*> = 0 + 1 by FINSEQ_1:39 .= (len {}) + 1 ; for n being Element of NAT st 1 <= n & n <= len {} holds {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) ; hence <*v*> is_oriented_vertex_seq_of {} by A1, Def5; ::_thesis: verum end; definition let G be Graph; let IT be oriented Chain of G; attrIT is Simple means :Def7: :: GRAPH_4:def 7 ex vs being FinSequence of the carrier of G st ( vs is_oriented_vertex_seq_of IT & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds ( n = 1 & m = len vs ) ) ); end; :: deftheorem Def7 defines Simple GRAPH_4:def_7_:_ for G being Graph for IT being oriented Chain of G holds ( IT is Simple iff ex vs being FinSequence of the carrier of G st ( vs is_oriented_vertex_seq_of IT & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds ( n = 1 & m = len vs ) ) ) ); registration let G be Graph; cluster Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple for Chain of G; existence ex b1 being oriented Chain of G st b1 is Simple proof set q = the empty oriented Chain of G; set x = the Element of G; reconsider p = <* the Element of G*> as FinSequence of the carrier of G ; A1: p is_oriented_vertex_seq_of the empty oriented Chain of G by Lm1; for n, m being Element of NAT st 1 <= n & n < m & m <= len p & p . n = p . m holds ( n = 1 & m = len p ) proof let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len p & p . n = p . m implies ( n = 1 & m = len p ) ) assume that A2: 1 <= n and A3: n < m and A4: m <= len p and p . n = p . m ; ::_thesis: ( n = 1 & m = len p ) 1 < m by A2, A3, XXREAL_0:2; hence ( n = 1 & m = len p ) by A4, FINSEQ_1:39; ::_thesis: verum end; then the empty oriented Chain of G is Simple by A1, Def7; hence ex b1 being oriented Chain of G st b1 is Simple ; ::_thesis: verum end; end; registration let G be Graph; cluster Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple for Chain of G; existence ex b1 being Chain of G st ( b1 is oriented & b1 is simple ) proof set q = the empty oriented Chain of G; set x = the Element of G; reconsider p = <* the Element of G*> as FinSequence of the carrier of G ; A1: p is_vertex_seq_of the empty oriented Chain of G by Lm1, Th4; reconsider q9 = the empty oriented Chain of G as Chain of G ; for n, m being Element of NAT st 1 <= n & n < m & m <= len p & p . n = p . m holds ( n = 1 & m = len p ) proof let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len p & p . n = p . m implies ( n = 1 & m = len p ) ) assume that A2: 1 <= n and A3: n < m and A4: m <= len p and p . n = p . m ; ::_thesis: ( n = 1 & m = len p ) 1 < m by A2, A3, XXREAL_0:2; hence ( n = 1 & m = len p ) by A4, FINSEQ_1:39; ::_thesis: verum end; then q9 is simple by A1, GRAPH_2:def_9; hence ex b1 being Chain of G st ( b1 is oriented & b1 is simple ) ; ::_thesis: verum end; end; theorem Th16: :: GRAPH_4:16 for n being Element of NAT for G being Graph for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G proof let n be Element of NAT ; ::_thesis: for G being Graph for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G let G be Graph; ::_thesis: for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G let q be oriented Chain of G; ::_thesis: q | (Seg n) is oriented Chain of G reconsider q9 = q | (Seg n) as FinSequence by FINSEQ_1:15; for i being Element of NAT st 1 <= i & i < len q9 holds the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len q9 implies the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) ) assume that A1: 1 <= i and A2: i < len q9 ; ::_thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) percases ( n >= len q or n < len q ) ; suppose n >= len q ; ::_thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) then q | (Seg n) = q by FINSEQ_3:49; hence the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) by A1, A2, GRAPH_1:def_15; ::_thesis: verum end; supposeA3: n < len q ; ::_thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) then A4: len q9 = n by FINSEQ_1:17; then A5: i < len q by A2, A3, XXREAL_0:2; i in Seg n by A1, A2, A4, FINSEQ_1:1; then A6: (q | (Seg n)) . i = q . i by FUNCT_1:49; A7: i + 1 <= n by A2, A4, NAT_1:13; 1 < i + 1 by A1, NAT_1:13; then i + 1 in Seg n by A7, FINSEQ_1:1; then (q | (Seg n)) . (i + 1) = q . (i + 1) by FUNCT_1:49; hence the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) by A1, A5, A6, GRAPH_1:def_15; ::_thesis: verum end; end; end; hence q | (Seg n) is oriented Chain of G by GRAPH_1:4, GRAPH_1:def_15; ::_thesis: verum end; theorem :: GRAPH_4:17 for n being Element of NAT for G being Graph for sc being oriented simple Chain of G holds sc | (Seg n) is oriented simple Chain of G by Th16, GRAPH_2:45; theorem Th18: :: GRAPH_4:18 for G being Graph for sc being oriented simple Chain of G for sc9 being oriented Chain of G st sc9 = sc holds sc9 is Simple proof let G be Graph; ::_thesis: for sc being oriented simple Chain of G for sc9 being oriented Chain of G st sc9 = sc holds sc9 is Simple let sc be oriented simple Chain of G; ::_thesis: for sc9 being oriented Chain of G st sc9 = sc holds sc9 is Simple let sc9 be oriented Chain of G; ::_thesis: ( sc9 = sc implies sc9 is Simple ) assume A1: sc9 = sc ; ::_thesis: sc9 is Simple consider vs being FinSequence of the carrier of G such that A2: vs is_oriented_vertex_seq_of sc9 by Th9; vs is_vertex_seq_of sc by A1, A2, Th4; then for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds ( n = 1 & m = len vs ) by GRAPH_2:47; hence sc9 is Simple by A2, Def7; ::_thesis: verum end; theorem Th19: :: GRAPH_4:19 for G being Graph for sc9 being oriented Simple Chain of G holds sc9 is oriented simple Chain of G proof let G be Graph; ::_thesis: for sc9 being oriented Simple Chain of G holds sc9 is oriented simple Chain of G let sc9 be oriented Simple Chain of G; ::_thesis: sc9 is oriented simple Chain of G consider vs being FinSequence of the carrier of G such that A1: vs is_oriented_vertex_seq_of sc9 and A2: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds ( n = 1 & m = len vs ) by Def7; vs is_vertex_seq_of sc9 by A1, Th4; hence sc9 is oriented simple Chain of G by A2, GRAPH_2:def_9; ::_thesis: verum end; Lm2: for p being FinSequence for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) proof let p be FinSequence; ::_thesis: for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) let m, n be Element of NAT ; ::_thesis: ( 1 <= m & m <= n + 1 & n <= len p implies ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) ) assume that A1: 1 <= m and A2: m <= n + 1 and A3: n <= len p ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) A4: ( m = n + 1 or m < n + 1 ) by A2, XXREAL_0:1; percases ( m = n + 1 or m <= n ) by A4, NAT_1:13; supposeA5: m = n + 1 ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) then A6: n < m by XREAL_1:29; A7: ( not 1 <= m or not m <= n or not n <= len p ) by A5, XREAL_1:29; (m,n) -cut p = {} by A6, GRAPH_2:def_1; hence (len ((m,n) -cut p)) + m = n + 1 by A5, CARD_1:27; ::_thesis: for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) thus for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) by A7, CARD_1:27, GRAPH_2:def_1; ::_thesis: verum end; suppose m <= n ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) hence ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) by A1, A3, GRAPH_2:def_1; ::_thesis: verum end; end; end; theorem Th20: :: GRAPH_4:20 for G being Graph for vs being FinSequence of the carrier of G for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) proof let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) let c be oriented Chain of G; ::_thesis: ( not c is Simple & vs is_oriented_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) ) assume that A1: not c is Simple and A2: vs is_oriented_vertex_seq_of c ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) consider n, m being Element of NAT such that A3: 1 <= n and A4: n < m and A5: m <= len vs and A6: vs . n = vs . m and A7: ( n <> 1 or m <> len vs ) by A1, A2, Def7; A8: len vs = (len c) + 1 by A2, Def5; A9: m - n > n - n by A4, XREAL_1:9; reconsider n1 = n -' 1 as Element of NAT ; A10: 1 - 1 <= n - 1 by A3, XREAL_1:9; then A11: n - 1 = n -' 1 by XREAL_0:def_2; A12: n1 + 1 = (n - 1) + 1 by A10, XREAL_0:def_2 .= n ; percases ( ( n <> 1 & m <> len vs ) or ( n = 1 & m <> len vs ) or ( n <> 1 & m = len vs ) ) by A7; supposeA13: ( n <> 1 & m <> len vs ) ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) then 1 < n by A3, XXREAL_0:1; then 1 + 1 <= n by NAT_1:13; then A14: (1 + 1) - 1 <= n - 1 by XREAL_1:9; n < len vs by A4, A5, XXREAL_0:2; then A15: n - 1 < ((len c) + 1) - 1 by A8, XREAL_1:9; A16: 1 <= n1 + 1 by NAT_1:12; A17: m < len vs by A5, A13, XXREAL_0:1; then A18: m <= len c by A8, NAT_1:13; A19: 1 <= m by A3, A4, XXREAL_0:2; A20: m <= len c by A8, A17, NAT_1:13; reconsider c1 = (1,n1) -cut c as oriented Chain of G by A11, A14, A15, Th12; reconsider c2 = (m,(len c)) -cut c as oriented Chain of G by A19, A20, Th12; set pp = (1,n) -cut vs; set p2 = (m,((len c) + 1)) -cut vs; set p29 = ((m + 1),((len c) + 1)) -cut vs; reconsider pp = (1,n) -cut vs as FinSequence of the carrier of G ; reconsider p2 = (m,((len c) + 1)) -cut vs as FinSequence of the carrier of G ; A21: n <= len vs by A4, A5, XXREAL_0:2; A22: 1 <= m by A3, A4, XXREAL_0:2; A23: m <= (len c) + 1 by A2, A5, Def5; A24: (len c) + 1 <= len vs by A2, Def5; A25: pp is_oriented_vertex_seq_of c1 by A2, A12, A14, A15, Th13; A26: p2 is_oriented_vertex_seq_of c2 by A2, A19, A20, Th13; A27: len pp = (len c1) + 1 by A25, Def5; A28: len p2 = (len c2) + 1 by A26, Def5; 1 - 1 <= m - 1 by A19, XREAL_1:9; then m -' 1 = m - 1 by XREAL_0:def_2; then reconsider m1 = m - 1 as Element of NAT ; A29: m = m1 + 1 ; A30: (len c2) + m = (len c) + 1 by A19, A20, GRAPH_2:def_1; A31: m - m <= (len c) - m by A18, XREAL_1:9; then (len c2) -' 1 = (len c2) - 1 by A30, XREAL_0:def_2; then reconsider lc21 = (len c2) - 1 as Element of NAT ; A32: m + lc21 = m1 + (len c2) ; 0 + 1 = 1 ; then A33: 1 <= len p2 by A28, NAT_1:13; A34: p2 = ((0 + 1),(len p2)) -cut p2 by GRAPH_2:7 .= (((0 + 1),1) -cut p2) ^ (((1 + 1),(len p2)) -cut p2) by A33, GRAPH_2:8 ; m1 <= m by A29, NAT_1:12; then A35: p2 = (((m1 + 1),m) -cut vs) ^ (((m + 1),((len c) + 1)) -cut vs) by A5, A8, GRAPH_2:8; (1,1) -cut p2 = <*(p2 . (0 + 1))*> by A33, GRAPH_2:6 .= <*(vs . (m + 0))*> by A22, A23, A24, A28, GRAPH_2:def_1 .= (m,m) -cut vs by A5, A19, GRAPH_2:6 ; then A36: ((m + 1),((len c) + 1)) -cut vs = (2,(len p2)) -cut p2 by A34, A35, FINSEQ_1:33; set domfc = { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; deffunc H1( set ) -> set = c . \$1; consider fc being Function such that A37: dom fc = { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } and A38: for x being set st x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } holds fc . x = H1(x) from FUNCT_1:sch_3(); { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } c= Seg (len c) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } or x in Seg (len c) ) assume x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; ::_thesis: x in Seg (len c) then consider kk being Element of NAT such that A39: x = kk and A40: ( ( 1 <= kk & kk <= n1 ) or ( m <= kk & kk <= len c ) ) ; A41: 1 <= kk by A19, A40, XXREAL_0:2; kk <= len c by A11, A15, A40, XXREAL_0:2; hence x in Seg (len c) by A39, A41, FINSEQ_1:1; ::_thesis: verum end; then reconsider fc = fc as FinSubsequence by A37, FINSEQ_1:def_12; fc c= c proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fc or p in c ) assume A42: p in fc ; ::_thesis: p in c then consider x, y being set such that A43: [x,y] = p by RELAT_1:def_1; A44: x in dom fc by A42, A43, FUNCT_1:1; A45: y = fc . x by A42, A43, FUNCT_1:1; consider kk being Element of NAT such that A46: x = kk and A47: ( ( 1 <= kk & kk <= n1 ) or ( m <= kk & kk <= len c ) ) by A37, A44; A48: 1 <= kk by A19, A47, XXREAL_0:2; kk <= len c by A11, A15, A47, XXREAL_0:2; then A49: x in dom c by A46, A48, FINSEQ_3:25; y = c . kk by A37, A38, A44, A45, A46; hence p in c by A43, A46, A49, FUNCT_1:1; ::_thesis: verum end; then reconsider fc = fc as Subset of c ; take fc ; ::_thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) set domfvs = { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; deffunc H2( set ) -> set = vs . \$1; consider fvs being Function such that A50: dom fvs = { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } and A51: for x being set st x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } holds fvs . x = H2(x) from FUNCT_1:sch_3(); { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } c= Seg (len vs) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } or x in Seg (len vs) ) assume x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; ::_thesis: x in Seg (len vs) then consider kk being Element of NAT such that A52: x = kk and A53: ( ( 1 <= kk & kk <= n ) or ( m + 1 <= kk & kk <= len vs ) ) ; 1 <= m + 1 by NAT_1:12; then A54: 1 <= kk by A53, XXREAL_0:2; kk <= len vs by A21, A53, XXREAL_0:2; hence x in Seg (len vs) by A52, A54, FINSEQ_1:1; ::_thesis: verum end; then reconsider fvs = fvs as FinSubsequence by A50, FINSEQ_1:def_12; fvs c= vs proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fvs or p in vs ) assume A55: p in fvs ; ::_thesis: p in vs then consider x, y being set such that A56: [x,y] = p by RELAT_1:def_1; A57: x in dom fvs by A55, A56, FUNCT_1:1; A58: y = fvs . x by A55, A56, FUNCT_1:1; consider kk being Element of NAT such that A59: x = kk and A60: ( ( 1 <= kk & kk <= n ) or ( m + 1 <= kk & kk <= len vs ) ) by A50, A57; 1 <= m + 1 by NAT_1:12; then A61: 1 <= kk by A60, XXREAL_0:2; kk <= len vs by A21, A60, XXREAL_0:2; then A62: x in dom vs by A59, A61, FINSEQ_3:25; y = vs . kk by A50, A51, A57, A58, A59; hence p in vs by A56, A59, A62, FUNCT_1:1; ::_thesis: verum end; then reconsider fvs = fvs as Subset of vs ; take fvs ; ::_thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) A63: p2 . 1 = vs . m by A22, A23, A24, GRAPH_2:12; A64: pp . (len pp) = vs . n by A3, A21, GRAPH_2:12; then reconsider c9 = c1 ^ c2 as oriented Chain of G by A6, A25, A26, A63, Th14; take c9 ; ::_thesis: ex vs1 being FinSequence of the carrier of G st ( len c9 < len c & vs1 is_oriented_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 ) take p1 = pp ^' p2; ::_thesis: ( len c9 < len c & p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) A65: p1 = pp ^ (((m + 1),((len c) + 1)) -cut vs) by A36, GRAPH_2:def_2; A66: (len c1) + 1 = n1 + 1 by A11, A15, A16, Lm2; - (- (m - n)) = m - n ; then A67: - (m - n) < 0 by A9; len c9 = (n - 1) + (((len c) - m) + 1) by A11, A30, A66, FINSEQ_1:22 .= (len c) + (n + (- m)) ; hence A68: len c9 < len c by A67, XREAL_1:30; ::_thesis: ( p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) thus p1 is_oriented_vertex_seq_of c9 by A6, A25, A26, A63, A64, Th15; ::_thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) then len p1 = (len c9) + 1 by Def5; hence len p1 < len vs by A8, A68, XREAL_1:6; ::_thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) 1 <= 1 + (len c1) by NAT_1:12; then 1 <= len pp by A25, Def5; then p1 . 1 = pp . 1 by GRAPH_2:14; hence vs . 1 = p1 . 1 by A3, A21, GRAPH_2:12; ::_thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) A69: p2 . (len p2) = vs . ((len c) + 1) by A22, A23, A24, GRAPH_2:12; m - m <= (len c) - m by A20, XREAL_1:9; then 0 + 1 <= ((len c) - m) + 1 by XREAL_1:6; then 1 < len p2 by A28, A30, NAT_1:13; hence vs . (len vs) = p1 . (len p1) by A8, A69, GRAPH_2:16; ::_thesis: ( Seq fc = c9 & Seq fvs = p1 ) set DL = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } ; set DR = { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in__{__k_where_k_is_Element_of_NAT_:_(_(_1_<=_k_&_k_<=_n1_)_or_(_m_<=_k_&_k_<=_len_c_)_)__}__implies_x_in__{__kk_where_kk_is_Element_of_NAT_:_(_1_<=_kk_&_kk_<=_n1_)__}__\/__{__kk_where_kk_is_Element_of_NAT_:_(_m_<=_kk_&_kk_<=_len_c_)__}__)_&_(_x_in__{__kk_where_kk_is_Element_of_NAT_:_(_1_<=_kk_&_kk_<=_n1_)__}__\/__{__kk_where_kk_is_Element_of_NAT_:_(_m_<=_kk_&_kk_<=_len_c_)__}__implies_x_in__{__k_where_k_is_Element_of_NAT_:_(_(_1_<=_k_&_k_<=_n1_)_or_(_m_<=_k_&_k_<=_len_c_)_)__}__)_) let x be set ; ::_thesis: ( ( x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } implies x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ) & ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } implies b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } ) ) hereby ::_thesis: ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } implies b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } ) assume x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; ::_thesis: x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } then ex k being Element of NAT st ( x = k & ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) ) ; then ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } or x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ) ; hence x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } by XBOOLE_0:def_3; ::_thesis: verum end; assume A70: x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } percases ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } or x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ) by A70, XBOOLE_0:def_3; suppose x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } then ex k being Element of NAT st ( x = k & 1 <= k & k <= n1 ) ; hence x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; ::_thesis: verum end; suppose x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } then ex k being Element of NAT st ( x = k & m <= k & k <= len c ) ; hence x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; ::_thesis: verum end; end; end; then A71: { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } by TARSKI:1; A72: ( { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } c= Seg (len c) & { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } c= Seg (len c) ) proof hereby :: according to TARSKI:def_3 ::_thesis: { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } c= Seg (len c) let x be set ; ::_thesis: ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } implies x in Seg (len c) ) assume x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } ; ::_thesis: x in Seg (len c) then consider k being Element of NAT such that A73: x = k and A74: 1 <= k and A75: k <= n1 ; k <= len c by A11, A15, A75, XXREAL_0:2; hence x in Seg (len c) by A73, A74, FINSEQ_1:1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } or x in Seg (len c) ) assume x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ; ::_thesis: x in Seg (len c) then consider k being Element of NAT such that A76: x = k and A77: m <= k and A78: k <= len c ; 1 <= k by A22, A77, XXREAL_0:2; hence x in Seg (len c) by A76, A78, FINSEQ_1:1; ::_thesis: verum end; then reconsider DL = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } as finite set by FINSET_1:1; reconsider DR = { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } as finite set by A72, FINSET_1:1; now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_DL_&_j_in_DR_holds_ i_<_j let i, j be Element of NAT ; ::_thesis: ( i in DL & j in DR implies i < j ) assume i in DL ; ::_thesis: ( j in DR implies i < j ) then consider k being Element of NAT such that A79: k = i and 1 <= k and A80: k <= n1 ; assume j in DR ; ::_thesis: i < j then A81: ex l being Element of NAT st ( l = j & m <= l & l <= len c ) ; n1 < m by A4, A12, NAT_1:13; then k < m by A80, XXREAL_0:2; hence i < j by A79, A81, XXREAL_0:2; ::_thesis: verum end; then A82: Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR) by A72, FINSEQ_3:42; m + lc21 = len c by A30; then A83: card DR = ((len c2) + (- 1)) + 1 by GRAPH_2:4 .= len c2 ; A84: len (Sgm DR) = card DR by A72, FINSEQ_3:39; DL = Seg n1 by FINSEQ_1:def_1; then A85: Sgm DL = idseq n1 by FINSEQ_3:48; then A86: dom (Sgm DL) = Seg n1 by RELAT_1:45; rng (Sgm DL) = DL by A72, FINSEQ_1:def_13; then A87: rng (Sgm DL) c= dom fc by A37, A71, XBOOLE_1:7; rng (Sgm DR) = DR by A72, FINSEQ_1:def_13; then A88: rng (Sgm DR) c= dom fc by A37, A71, XBOOLE_1:7; set SL = Sgm DL; set SR = Sgm DR; now__::_thesis:_for_p_being_set_holds_ (_(_p_in_c1_implies_p_in_fc_*_(Sgm_DL)_)_&_(_p_in_fc_*_(Sgm_DL)_implies_p_in_c1_)_) let p be set ; ::_thesis: ( ( p in c1 implies p in fc * (Sgm DL) ) & ( p in fc * (Sgm DL) implies p in c1 ) ) hereby ::_thesis: ( p in fc * (Sgm DL) implies p in c1 ) assume A89: p in c1 ; ::_thesis: p in fc * (Sgm DL) then consider x, y being set such that A90: p = [x,y] by RELAT_1:def_1; A91: x in dom c1 by A89, A90, FUNCT_1:1; A92: y = c1 . x by A89, A90, FUNCT_1:1; reconsider k = x as Element of NAT by A91; A93: 1 <= k by A91, FINSEQ_3:25; A94: k <= len c1 by A91, FINSEQ_3:25; then A95: x in dom (Sgm DL) by A66, A86, A93, FINSEQ_1:1; then A96: k = (Sgm DL) . k by A85, A86, FUNCT_1:18; A97: k in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } by A66, A93, A94; then A98: x in dom (fc * (Sgm DL)) by A37, A95, A96, FUNCT_1:11; 0 + 1 <= k by A91, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A99: i < n1 and A100: k = i + 1 by A66, A94, GRAPH_2:1; (fc * (Sgm DL)) . x = fc . k by A96, A98, FUNCT_1:12 .= c . (1 + i) by A37, A97, A100, GRFUNC_1:2 .= y by A11, A15, A16, A66, A92, A99, A100, Lm2 ; hence p in fc * (Sgm DL) by A90, A98, FUNCT_1:1; ::_thesis: verum end; assume A101: p in fc * (Sgm DL) ; ::_thesis: p in c1 then consider x, y being set such that A102: p = [x,y] by RELAT_1:def_1; A103: x in dom (fc * (Sgm DL)) by A101, A102, FUNCT_1:1; A104: y = (fc * (Sgm DL)) . x by A101, A102, FUNCT_1:1; A105: (fc * (Sgm DL)) . x = fc . ((Sgm DL) . x) by A103, FUNCT_1:12; A106: x in dom (Sgm DL) by A103, FUNCT_1:11; then x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } by A86, FINSEQ_1:def_1; then consider k being Element of NAT such that A107: k = x and A108: 1 <= k and A109: k <= n1 ; A110: k in dom fc by A37, A108, A109; A111: k = (Sgm DL) . k by A85, A86, A106, A107, FUNCT_1:18; A112: k in dom c1 by A66, A108, A109, FINSEQ_3:25; 0 + 1 <= k by A108; then ex i being Element of NAT st ( 0 <= i & i < n1 & k = i + 1 ) by A109, GRAPH_2:1; then c1 . k = c . k by A11, A15, A16, A66, Lm2 .= y by A104, A105, A107, A110, A111, GRFUNC_1:2 ; hence p in c1 by A102, A107, A112, FUNCT_1:1; ::_thesis: verum end; then A113: c1 = fc * (Sgm DL) by TARSKI:1; now__::_thesis:_for_p_being_set_holds_ (_(_p_in_c2_implies_p_in_fc_*_(Sgm_DR)_)_&_(_p_in_fc_*_(Sgm_DR)_implies_p_in_c2_)_) let p be set ; ::_thesis: ( ( p in c2 implies p in fc * (Sgm DR) ) & ( p in fc * (Sgm DR) implies p in c2 ) ) hereby ::_thesis: ( p in fc * (Sgm DR) implies p in c2 ) assume A114: p in c2 ; ::_thesis: p in fc * (Sgm DR) then consider x, y being set such that A115: p = [x,y] by RELAT_1:def_1; A116: x in dom c2 by A114, A115, FUNCT_1:1; A117: y = c2 . x by A114, A115, FUNCT_1:1; reconsider k = x as Element of NAT by A116; A118: 1 <= k by A116, FINSEQ_3:25; A119: k <= len c2 by A116, FINSEQ_3:25; A120: x in dom (Sgm DR) by A83, A84, A116, FINSEQ_3:29; A121: m1 + k = (Sgm DR) . k by A29, A30, A32, A118, A119, GRAPH_2:5; A122: (Sgm DR) . k in rng (Sgm DR) by A120, FUNCT_1:def_3; then A123: x in dom (fc * (Sgm DR)) by A88, A120, FUNCT_1:11; 0 + 1 <= k by A116, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A124: i < len c2 and A125: k = i + 1 by A119, GRAPH_2:1; (fc * (Sgm DR)) . x = fc . (m1 + k) by A121, A123, FUNCT_1:12 .= c . (m + i) by A88, A121, A122, A125, GRFUNC_1:2 .= y by A19, A20, A117, A124, A125, GRAPH_2:def_1 ; hence p in fc * (Sgm DR) by A115, A123, FUNCT_1:1; ::_thesis: verum end; assume A126: p in fc * (Sgm DR) ; ::_thesis: p in c2 then consider x, y being set such that A127: p = [x,y] by RELAT_1:def_1; A128: x in dom (fc * (Sgm DR)) by A126, A127, FUNCT_1:1; A129: y = (fc * (Sgm DR)) . x by A126, A127, FUNCT_1:1; A130: x in dom (Sgm DR) by A128, FUNCT_1:11; A131: (Sgm DR) . x in dom fc by A128, FUNCT_1:11; reconsider k = x as Element of NAT by A130; A132: k in dom c2 by A83, A84, A130, FINSEQ_3:29; A133: 1 <= k by A130, FINSEQ_3:25; A134: k <= len c2 by A83, A84, A130, FINSEQ_3:25; then A135: m1 + k = (Sgm DR) . k by A29, A30, A32, A133, GRAPH_2:5; 0 + 1 <= k by A130, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A136: i < len c2 and A137: k = i + 1 by A134, GRAPH_2:1; c2 . k = c . ((m1 + 1) + i) by A19, A20, A136, A137, GRAPH_2:def_1 .= fc . ((Sgm DR) . k) by A131, A135, A137, GRFUNC_1:2 .= y by A129, A130, FUNCT_1:13 ; hence p in c2 by A127, A132, FUNCT_1:1; ::_thesis: verum end; then A138: c2 = fc * (Sgm DR) by TARSKI:1; Seq fc = fc * ((Sgm DL) ^ (Sgm DR)) by A37, A71, A82, FINSEQ_1:def_14; hence Seq fc = c9 by A87, A88, A113, A138, GRAPH_2:24; ::_thesis: Seq fvs = p1 set DL = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } ; set DR = { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in__{__k_where_k_is_Element_of_NAT_:_(_(_1_<=_k_&_k_<=_n_)_or_(_m_+_1_<=_k_&_k_<=_len_vs_)_)__}__implies_x_in__{__kk_where_kk_is_Element_of_NAT_:_(_1_<=_kk_&_kk_<=_n_)__}__\/__{__kk_where_kk_is_Element_of_NAT_:_(_m_+_1_<=_kk_&_kk_<=_len_vs_)__}__)_&_(_x_in__{__kk_where_kk_is_Element_of_NAT_:_(_1_<=_kk_&_kk_<=_n_)__}__\/__{__kk_where_kk_is_Element_of_NAT_:_(_m_+_1_<=_kk_&_kk_<=_len_vs_)__}__implies_x_in__{__k_where_k_is_Element_of_NAT_:_(_(_1_<=_k_&_k_<=_n_)_or_(_m_+_1_<=_k_&_k_<=_len_vs_)_)__}__)_) let x be set ; ::_thesis: ( ( x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } implies x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ) & ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } implies b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } ) ) hereby ::_thesis: ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } implies b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } ) assume x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; ::_thesis: x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } then ex k being Element of NAT st ( x = k & ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) ) ; then ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } or x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ) ; hence x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } by XBOOLE_0:def_3; ::_thesis: verum end; assume A139: x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } percases ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } or x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ) by A139, XBOOLE_0:def_3; suppose x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } then ex k being Element of NAT st ( x = k & 1 <= k & k <= n ) ; hence x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; ::_thesis: verum end; suppose x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } then ex k being Element of NAT st ( x = k & m + 1 <= k & k <= len vs ) ; hence x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; ::_thesis: verum end; end; end; then A140: { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } by TARSKI:1; A141: ( { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } c= Seg (len vs) & { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } c= Seg (len vs) ) proof hereby :: according to TARSKI:def_3 ::_thesis: { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } c= Seg (len vs) let x be set ; ::_thesis: ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } implies x in Seg (len vs) ) assume x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } ; ::_thesis: x in Seg (len vs) then consider k being Element of NAT such that A142: x = k and A143: 1 <= k and A144: k <= n ; k <= len vs by A21, A144, XXREAL_0:2; hence x in Seg (len vs) by A142, A143, FINSEQ_1:1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } or x in Seg (len vs) ) assume x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ; ::_thesis: x in Seg (len vs) then consider k being Element of NAT such that A145: x = k and A146: m + 1 <= k and A147: k <= len vs ; 1 <= m + 1 by NAT_1:12; then 1 <= k by A146, XXREAL_0:2; hence x in Seg (len vs) by A145, A147, FINSEQ_1:1; ::_thesis: verum end; then reconsider DL = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } as finite set by FINSET_1:1; reconsider DR = { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } as finite set by A141, FINSET_1:1; now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_DL_&_j_in_DR_holds_ i_<_j let i, j be Element of NAT ; ::_thesis: ( i in DL & j in DR implies i < j ) assume i in DL ; ::_thesis: ( j in DR implies i < j ) then consider k being Element of NAT such that A148: k = i and 1 <= k and A149: k <= n ; assume j in DR ; ::_thesis: i < j then consider l being Element of NAT such that A150: l = j and A151: m + 1 <= l and l <= len vs ; m <= m + 1 by NAT_1:12; then A152: m <= l by A151, XXREAL_0:2; k < m by A4, A149, XXREAL_0:2; hence i < j by A148, A150, A152, XXREAL_0:2; ::_thesis: verum end; then A153: Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR) by A141, FINSEQ_3:42; 1 <= len p2 by A28, NAT_1:12; then 1 - 1 <= (len p2) - 1 by XREAL_1:9; then (len p2) -' 1 = (len p2) - 1 by XREAL_0:def_2; then reconsider lp21 = (len p2) - 1 as Element of NAT ; lp21 -' 1 = lp21 - 1 by A28, A30, A31, XREAL_0:def_2; then reconsider lp22 = lp21 - 1 as Element of NAT ; A154: (m + 1) + lp22 = m + ((lp21 - 1) + 1) .= m + (((((len c) - m) + 1) + 1) - 1) by A26, A30, Def5 .= (len c) + 1 ; then A155: card DR = lp22 + 1 by A8, GRAPH_2:4 .= lp21 ; A156: 1 <= m + 1 by NAT_1:12; A157: m + 1 <= ((len c) + 1) + 1 by A23, XREAL_1:6; A158: (len p2) + m = ((len c) + 1) + 1 by A22, A23, A24, GRAPH_2:def_1 .= (len (((m + 1),((len c) + 1)) -cut vs)) + (m + 1) by A24, A156, A157, Lm2 .= ((len (((m + 1),((len c) + 1)) -cut vs)) + 1) + m ; A159: len (Sgm DR) = card DR by A141, FINSEQ_3:39; DL = Seg n by FINSEQ_1:def_1; then A160: Sgm DL = idseq n by FINSEQ_3:48; then A161: dom (Sgm DL) = Seg n by RELAT_1:45; rng (Sgm DL) = DL by A141, FINSEQ_1:def_13; then A162: rng (Sgm DL) c= dom fvs by A50, A140, XBOOLE_1:7; rng (Sgm DR) = DR by A141, FINSEQ_1:def_13; then A163: rng (Sgm DR) c= dom fvs by A50, A140, XBOOLE_1:7; set SL = Sgm DL; set SR = Sgm DR; now__::_thesis:_for_p_being_set_holds_ (_(_p_in_pp_implies_p_in_fvs_*_(Sgm_DL)_)_&_(_p_in_fvs_*_(Sgm_DL)_implies_p_in_pp_)_) let p be set ; ::_thesis: ( ( p in pp implies p in fvs * (Sgm DL) ) & ( p in fvs * (Sgm DL) implies p in pp ) ) hereby ::_thesis: ( p in fvs * (Sgm DL) implies p in pp ) assume A164: p in pp ; ::_thesis: p in fvs * (Sgm DL) then consider x, y being set such that A165: p = [x,y] by RELAT_1:def_1; A166: x in dom pp by A164, A165, FUNCT_1:1; A167: y = pp . x by A164, A165, FUNCT_1:1; reconsider k = x as Element of NAT by A166; A168: 1 <= k by A166, FINSEQ_3:25; A169: k <= len pp by A166, FINSEQ_3:25; then A170: x in dom (Sgm DL) by A11, A27, A66, A161, A168, FINSEQ_1:1; then A171: k = (Sgm DL) . k by A160, A161, FUNCT_1:18; A172: k in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } by A11, A27, A66, A168, A169; then A173: x in dom (fvs * (Sgm DL)) by A50, A170, A171, FUNCT_1:11; 0 + 1 <= k by A166, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A174: i < n and A175: k = i + 1 by A11, A27, A66, A169, GRAPH_2:1; (fvs * (Sgm DL)) . x = fvs . k by A171, A173, FUNCT_1:12 .= vs . (1 + i) by A50, A172, A175, GRFUNC_1:2 .= y by A3, A11, A21, A27, A66, A167, A174, A175, GRAPH_2:def_1 ; hence p in fvs * (Sgm DL) by A165, A173, FUNCT_1:1; ::_thesis: verum end; assume A176: p in fvs * (Sgm DL) ; ::_thesis: p in pp then consider x, y being set such that A177: p = [x,y] by RELAT_1:def_1; A178: x in dom (fvs * (Sgm DL)) by A176, A177, FUNCT_1:1; A179: y = (fvs * (Sgm DL)) . x by A176, A177, FUNCT_1:1; A180: (fvs * (Sgm DL)) . x = fvs . ((Sgm DL) . x) by A178, FUNCT_1:12; A181: x in dom (Sgm DL) by A178, FUNCT_1:11; then x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } by A161, FINSEQ_1:def_1; then consider k being Element of NAT such that A182: k = x and A183: 1 <= k and A184: k <= n ; A185: k in dom fvs by A50, A183, A184; A186: k = (Sgm DL) . k by A160, A161, A181, A182, FUNCT_1:18; A187: k in dom pp by A11, A27, A66, A183, A184, FINSEQ_3:25; 0 + 1 <= k by A183; then ex i being Element of NAT st ( 0 <= i & i < n & k = i + 1 ) by A184, GRAPH_2:1; then pp . k = vs . k by A3, A11, A21, A27, A66, GRAPH_2:def_1 .= y by A179, A180, A182, A185, A186, GRFUNC_1:2 ; hence p in pp by A177, A182, A187, FUNCT_1:1; ::_thesis: verum end; then A188: pp = fvs * (Sgm DL) by TARSKI:1; A189: (m + 1) + lp22 = m + lp21 ; A190: 1 <= m + 1 by NAT_1:12; A191: m + 1 <= ((len c) + 1) + 1 by A5, A8, XREAL_1:7; now__::_thesis:_for_p_being_set_holds_ (_(_p_in_((m_+_1),((len_c)_+_1))_-cut_vs_implies_p_in_fvs_*_(Sgm_DR)_)_&_(_p_in_fvs_*_(Sgm_DR)_implies_p_in_((m_+_1),((len_c)_+_1))_-cut_vs_)_) let p be set ; ::_thesis: ( ( p in ((m + 1),((len c) + 1)) -cut vs implies p in fvs * (Sgm DR) ) & ( p in fvs * (Sgm DR) implies p in ((m + 1),((len c) + 1)) -cut vs ) ) hereby ::_thesis: ( p in fvs * (Sgm DR) implies p in ((m + 1),((len c) + 1)) -cut vs ) assume A192: p in ((m + 1),((len c) + 1)) -cut vs ; ::_thesis: p in fvs * (Sgm DR) then consider x, y being set such that A193: p = [x,y] by RELAT_1:def_1; A194: x in dom (((m + 1),((len c) + 1)) -cut vs) by A192, A193, FUNCT_1:1; A195: y = (((m + 1),((len c) + 1)) -cut vs) . x by A192, A193, FUNCT_1:1; reconsider k = x as Element of NAT by A194; A196: 1 <= k by A194, FINSEQ_3:25; A197: k <= len (((m + 1),((len c) + 1)) -cut vs) by A194, FINSEQ_3:25; A198: x in dom (Sgm DR) by A155, A158, A159, A194, FINSEQ_3:29; A199: m + k = (Sgm DR) . k by A8, A154, A158, A189, A196, A197, GRAPH_2:5; A200: (Sgm DR) . k in rng (Sgm DR) by A198, FUNCT_1:def_3; then A201: x in dom (fvs * (Sgm DR)) by A163, A198, FUNCT_1:11; 0 + 1 <= k by A194, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A202: i < len (((m + 1),((len c) + 1)) -cut vs) and A203: k = i + 1 by A197, GRAPH_2:1; (fvs * (Sgm DR)) . x = fvs . (m + k) by A199, A201, FUNCT_1:12 .= vs . ((m + 1) + i) by A163, A199, A200, A203, GRFUNC_1:2 .= y by A8, A190, A191, A195, A202, A203, Lm2 ; hence p in fvs * (Sgm DR) by A193, A201, FUNCT_1:1; ::_thesis: verum end; assume A204: p in fvs * (Sgm DR) ; ::_thesis: p in ((m + 1),((len c) + 1)) -cut vs then consider x, y being set such that A205: p = [x,y] by RELAT_1:def_1; A206: x in dom (fvs * (Sgm DR)) by A204, A205, FUNCT_1:1; A207: y = (fvs * (Sgm DR)) . x by A204, A205, FUNCT_1:1; A208: x in dom (Sgm DR) by A206, FUNCT_1:11; A209: (Sgm DR) . x in dom fvs by A206, FUNCT_1:11; reconsider k = x as Element of NAT by A208; A210: k in dom (((m + 1),((len c) + 1)) -cut vs) by A155, A158, A159, A208, FINSEQ_3:29; A211: 1 <= k by A208, FINSEQ_3:25; A212: k <= len (((m + 1),((len c) + 1)) -cut vs) by A155, A158, A159, A208, FINSEQ_3:25; then A213: m + k = (Sgm DR) . k by A8, A154, A158, A189, A211, GRAPH_2:5; 0 + 1 <= k by A208, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A214: i < len (((m + 1),((len c) + 1)) -cut vs) and A215: k = i + 1 by A212, GRAPH_2:1; (((m + 1),((len c) + 1)) -cut vs) . k = vs . ((m + 1) + i) by A8, A190, A191, A214, A215, Lm2 .= fvs . ((Sgm DR) . k) by A209, A213, A215, GRFUNC_1:2 .= y by A207, A208, FUNCT_1:13 ; hence p in ((m + 1),((len c) + 1)) -cut vs by A205, A210, FUNCT_1:1; ::_thesis: verum end; then A216: ((m + 1),((len c) + 1)) -cut vs = fvs * (Sgm DR) by TARSKI:1; Seq fvs = fvs * ((Sgm DL) ^ (Sgm DR)) by A50, A140, A153, FINSEQ_1:def_14; hence Seq fvs = p1 by A65, A162, A163, A188, A216, GRAPH_2:24; ::_thesis: verum end; supposeA217: ( n = 1 & m <> len vs ) ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) then A218: m < len vs by A5, XXREAL_0:1; then A219: m <= len c by A8, NAT_1:13; A220: 1 < m by A3, A4, XXREAL_0:2; A221: 1 <= m by A3, A4, XXREAL_0:2; A222: m <= len c by A8, A218, NAT_1:13; reconsider c2 = (m,(len c)) -cut c as oriented Chain of G by A219, A220, Th12; set p2 = (m,((len c) + 1)) -cut vs; A223: (m,((len c) + 1)) -cut vs is_oriented_vertex_seq_of c2 by A2, A219, A220, Th13; set domfc = { k where k is Element of NAT : ( m <= k & k <= len c ) } ; deffunc H1( set ) -> set = c . \$1; consider fc being Function such that A224: dom fc = { k where k is Element of NAT : ( m <= k & k <= len c ) } and A225: for x being set st x in { k where k is Element of NAT : ( m <= k & k <= len c ) } holds fc . x = H1(x) from FUNCT_1:sch_3(); { k where k is Element of NAT : ( m <= k & k <= len c ) } c= Seg (len c) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= len c ) } or x in Seg (len c) ) assume x in { k where k is Element of NAT : ( m <= k & k <= len c ) } ; ::_thesis: x in Seg (len c) then consider kk being Element of NAT such that A226: x = kk and A227: m <= kk and A228: kk <= len c ; 1 <= kk by A220, A227, XXREAL_0:2; hence x in Seg (len c) by A226, A228, FINSEQ_1:1; ::_thesis: verum end; then reconsider fc = fc as FinSubsequence by A224, FINSEQ_1:def_12; fc c= c proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fc or p in c ) assume A229: p in fc ; ::_thesis: p in c then consider x, y being set such that A230: [x,y] = p by RELAT_1:def_1; A231: x in dom fc by A229, A230, FUNCT_1:1; A232: y = fc . x by A229, A230, FUNCT_1:1; consider kk being Element of NAT such that A233: x = kk and A234: m <= kk and A235: kk <= len c by A224, A231; 1 <= kk by A220, A234, XXREAL_0:2; then A236: x in dom c by A233, A235, FINSEQ_3:25; y = c . kk by A224, A225, A231, A232, A233; hence p in c by A230, A233, A236, FUNCT_1:1; ::_thesis: verum end; then reconsider fc = fc as Subset of c ; take fc ; ::_thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) set domfvs = { k where k is Element of NAT : ( m <= k & k <= len vs ) } ; deffunc H2( set ) -> set = vs . \$1; consider fvs being Function such that A237: dom fvs = { k where k is Element of NAT : ( m <= k & k <= len vs ) } and A238: for x being set st x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } holds fvs . x = H2(x) from FUNCT_1:sch_3(); { k where k is Element of NAT : ( m <= k & k <= len vs ) } c= Seg (len vs) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } or x in Seg (len vs) ) assume x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } ; ::_thesis: x in Seg (len vs) then consider kk being Element of NAT such that A239: x = kk and A240: m <= kk and A241: kk <= len vs ; 1 <= kk by A220, A240, XXREAL_0:2; hence x in Seg (len vs) by A239, A241, FINSEQ_1:1; ::_thesis: verum end; then reconsider fvs = fvs as FinSubsequence by A237, FINSEQ_1:def_12; fvs c= vs proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fvs or p in vs ) assume A242: p in fvs ; ::_thesis: p in vs then consider x, y being set such that A243: [x,y] = p by RELAT_1:def_1; A244: x in dom fvs by A242, A243, FUNCT_1:1; A245: y = fvs . x by A242, A243, FUNCT_1:1; consider kk being Element of NAT such that A246: x = kk and A247: m <= kk and A248: kk <= len vs by A237, A244; 1 <= kk by A220, A247, XXREAL_0:2; then A249: x in dom vs by A246, A248, FINSEQ_3:25; y = vs . kk by A237, A238, A244, A245, A246; hence p in vs by A243, A246, A249, FUNCT_1:1; ::_thesis: verum end; then reconsider fvs = fvs as Subset of vs ; take fvs ; ::_thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) take c1 = c2; ::_thesis: ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) take p1 = (m,((len c) + 1)) -cut vs; ::_thesis: ( len c1 < len c & p1 is_oriented_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 ) A250: (len c2) + m = (len c) + 1 by A4, A5, A8, A217, Lm2; A251: m - m <= (len c) - m by A219, XREAL_1:9; 1 - 1 <= m - 1 by A220, XREAL_1:9; then m -' 1 = m - 1 by XREAL_0:def_2; then reconsider m1 = m - 1 as Element of NAT ; A252: m = m1 + 1 ; (len c2) -' 1 = (len c2) - 1 by A250, A251, XREAL_0:def_2; then reconsider lc21 = (len c2) - 1 as Element of NAT ; A253: m + lc21 = m1 + (len c2) ; A254: m <= ((len c) + 1) + 1 by A5, A8, NAT_1:12; A255: (len c) + 1 <= len vs by A2, Def5; then A256: (len ((m,((len c) + 1)) -cut vs)) + m = ((len c) + 1) + 1 by A4, A217, A254, Lm2; then len ((m,((len c) + 1)) -cut vs) = (((len c) - m) + 1) + 1 ; then A257: 1 <= len ((m,((len c) + 1)) -cut vs) by A250, NAT_1:12; A258: len c2 = (len c) + ((- m) + 1) by A250; 1 - 1 < m - 1 by A220, XREAL_1:9; then 0 < - (- (m - 1)) ; then - (m - 1) < 0 ; hence A259: len c1 < len c by A258, XREAL_1:30; ::_thesis: ( p1 is_oriented_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 ) thus p1 is_oriented_vertex_seq_of c1 by A2, A221, A222, Th13; ::_thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 ) len p1 = (len c1) + 1 by A223, Def5; hence len p1 < len vs by A8, A259, XREAL_1:6; ::_thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 ) thus vs . 1 = p1 . 1 by A4, A5, A6, A8, A217, GRAPH_2:12; ::_thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 ) thus vs . (len vs) = p1 . (len p1) by A4, A5, A8, A217, GRAPH_2:12; ::_thesis: ( Seq fc = c1 & Seq fvs = p1 ) A260: { k where k is Element of NAT : ( m <= k & k <= len c ) } c= Seg (len c) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= len c ) } or x in Seg (len c) ) assume x in { k where k is Element of NAT : ( m <= k & k <= len c ) } ; ::_thesis: x in Seg (len c) then consider k being Element of NAT such that A261: x = k and A262: m <= k and A263: k <= len c ; 1 <= k by A220, A262, XXREAL_0:2; hence x in Seg (len c) by A261, A263, FINSEQ_1:1; ::_thesis: verum end; then reconsider domfc = { k where k is Element of NAT : ( m <= k & k <= len c ) } as finite set by FINSET_1:1; (len c2) -' 1 = (len c2) - 1 by A250, A251, XREAL_0:def_2; then reconsider lc21 = (len c2) - 1 as Element of NAT ; m + lc21 = len c by A250; then A264: card domfc = ((len c2) + (- 1)) + 1 by GRAPH_2:4 .= len c2 ; A265: len (Sgm domfc) = card domfc by A260, FINSEQ_3:39; A266: rng (Sgm domfc) c= dom fc by A224, A260, FINSEQ_1:def_13; set SR = Sgm domfc; now__::_thesis:_for_p_being_set_holds_ (_(_p_in_c2_implies_p_in_fc_*_(Sgm_domfc)_)_&_(_p_in_fc_*_(Sgm_domfc)_implies_p_in_c2_)_) let p be set ; ::_thesis: ( ( p in c2 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c2 ) ) hereby ::_thesis: ( p in fc * (Sgm domfc) implies p in c2 ) assume A267: p in c2 ; ::_thesis: p in fc * (Sgm domfc) then consider x, y being set such that A268: p = [x,y] by RELAT_1:def_1; A269: x in dom c2 by A267, A268, FUNCT_1:1; A270: y = c2 . x by A267, A268, FUNCT_1:1; reconsider k = x as Element of NAT by A269; A271: 1 <= k by A269, FINSEQ_3:25; A272: k <= len c2 by A269, FINSEQ_3:25; A273: x in dom (Sgm domfc) by A264, A265, A269, FINSEQ_3:29; A274: m1 + k = (Sgm domfc) . k by A250, A252, A253, A271, A272, GRAPH_2:5; A275: (Sgm domfc) . k in rng (Sgm domfc) by A273, FUNCT_1:def_3; then A276: x in dom (fc * (Sgm domfc)) by A266, A273, FUNCT_1:11; 0 + 1 <= k by A269, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A277: i < len c2 and A278: k = i + 1 by A272, GRAPH_2:1; (fc * (Sgm domfc)) . x = fc . (m1 + k) by A274, A276, FUNCT_1:12 .= c . (m + i) by A266, A274, A275, A278, GRFUNC_1:2 .= y by A4, A5, A8, A217, A270, A277, A278, Lm2 ; hence p in fc * (Sgm domfc) by A268, A276, FUNCT_1:1; ::_thesis: verum end; assume A279: p in fc * (Sgm domfc) ; ::_thesis: p in c2 then consider x, y being set such that A280: p = [x,y] by RELAT_1:def_1; A281: x in dom (fc * (Sgm domfc)) by A279, A280, FUNCT_1:1; A282: y = (fc * (Sgm domfc)) . x by A279, A280, FUNCT_1:1; A283: x in dom (Sgm domfc) by A281, FUNCT_1:11; A284: (Sgm domfc) . x in dom fc by A281, FUNCT_1:11; reconsider k = x as Element of NAT by A283; A285: k in dom c2 by A264, A265, A283, FINSEQ_3:29; A286: 1 <= k by A283, FINSEQ_3:25; A287: k <= len c2 by A264, A265, A283, FINSEQ_3:25; then A288: m1 + k = (Sgm domfc) . k by A250, A252, A253, A286, GRAPH_2:5; 0 + 1 <= k by A283, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A289: i < len c2 and A290: k = i + 1 by A287, GRAPH_2:1; c2 . k = c . ((m1 + 1) + i) by A4, A5, A8, A217, A289, A290, Lm2 .= fc . ((Sgm domfc) . k) by A284, A288, A290, GRFUNC_1:2 .= y by A282, A283, FUNCT_1:13 ; hence p in c2 by A280, A285, FUNCT_1:1; ::_thesis: verum end; then c2 = fc * (Sgm domfc) by TARSKI:1; hence Seq fc = c1 by A224, FINSEQ_1:def_14; ::_thesis: Seq fvs = p1 A291: { k where k is Element of NAT : ( m <= k & k <= len vs ) } c= Seg (len vs) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } or x in Seg (len vs) ) assume x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } ; ::_thesis: x in Seg (len vs) then consider k being Element of NAT such that A292: x = k and A293: m <= k and A294: k <= len vs ; 1 <= k by A220, A293, XXREAL_0:2; hence x in Seg (len vs) by A292, A294, FINSEQ_1:1; ::_thesis: verum end; then reconsider domfvs = { k where k is Element of NAT : ( m <= k & k <= len vs ) } as finite set by FINSET_1:1; 1 - 1 <= (len ((m,((len c) + 1)) -cut vs)) - 1 by A257, XREAL_1:9; then (len ((m,((len c) + 1)) -cut vs)) -' 1 = (len ((m,((len c) + 1)) -cut vs)) - 1 by XREAL_0:def_2; then reconsider lp21 = (len ((m,((len c) + 1)) -cut vs)) - 1 as Element of NAT ; A295: m + lp21 = (len c) + 1 by A256; A296: m + lp21 = m1 + (len ((m,((len c) + 1)) -cut vs)) ; A297: card domfvs = ((len ((m,((len c) + 1)) -cut vs)) + (- 1)) + 1 by A8, A295, GRAPH_2:4 .= len ((m,((len c) + 1)) -cut vs) ; A298: len (Sgm domfvs) = card domfvs by A291, FINSEQ_3:39; A299: rng (Sgm domfvs) c= dom fvs by A237, A291, FINSEQ_1:def_13; set SR = Sgm domfvs; now__::_thesis:_for_p_being_set_holds_ (_(_p_in_(m,((len_c)_+_1))_-cut_vs_implies_p_in_fvs_*_(Sgm_domfvs)_)_&_(_p_in_fvs_*_(Sgm_domfvs)_implies_p_in_(m,((len_c)_+_1))_-cut_vs_)_) let p be set ; ::_thesis: ( ( p in (m,((len c) + 1)) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs ) ) hereby ::_thesis: ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs ) assume A300: p in (m,((len c) + 1)) -cut vs ; ::_thesis: p in fvs * (Sgm domfvs) then consider x, y being set such that A301: p = [x,y] by RELAT_1:def_1; A302: x in dom ((m,((len c) + 1)) -cut vs) by A300, A301, FUNCT_1:1; A303: y = ((m,((len c) + 1)) -cut vs) . x by A300, A301, FUNCT_1:1; reconsider k = x as Element of NAT by A302; A304: 1 <= k by A302, FINSEQ_3:25; A305: k <= len ((m,((len c) + 1)) -cut vs) by A302, FINSEQ_3:25; A306: x in dom (Sgm domfvs) by A297, A298, A302, FINSEQ_3:29; A307: m1 + k = (Sgm domfvs) . k by A8, A252, A256, A296, A304, A305, GRAPH_2:5; A308: (Sgm domfvs) . k in rng (Sgm domfvs) by A306, FUNCT_1:def_3; then A309: x in dom (fvs * (Sgm domfvs)) by A299, A306, FUNCT_1:11; 0 + 1 <= k by A302, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A310: i < len ((m,((len c) + 1)) -cut vs) and A311: k = i + 1 by A305, GRAPH_2:1; (fvs * (Sgm domfvs)) . x = fvs . (m1 + k) by A307, A309, FUNCT_1:12 .= vs . (m + i) by A299, A307, A308, A311, GRFUNC_1:2 .= y by A4, A217, A254, A255, A303, A310, A311, Lm2 ; hence p in fvs * (Sgm domfvs) by A301, A309, FUNCT_1:1; ::_thesis: verum end; assume A312: p in fvs * (Sgm domfvs) ; ::_thesis: p in (m,((len c) + 1)) -cut vs then consider x, y being set such that A313: p = [x,y] by RELAT_1:def_1; A314: x in dom (fvs * (Sgm domfvs)) by A312, A313, FUNCT_1:1; A315: y = (fvs * (Sgm domfvs)) . x by A312, A313, FUNCT_1:1; A316: x in dom (Sgm domfvs) by A314, FUNCT_1:11; A317: (Sgm domfvs) . x in dom fvs by A314, FUNCT_1:11; reconsider k = x as Element of NAT by A316; A318: k in dom ((m,((len c) + 1)) -cut vs) by A297, A298, A316, FINSEQ_3:29; A319: 1 <= k by A316, FINSEQ_3:25; A320: k <= len ((m,((len c) + 1)) -cut vs) by A297, A298, A316, FINSEQ_3:25; then A321: m1 + k = (Sgm domfvs) . k by A8, A252, A256, A296, A319, GRAPH_2:5; 0 + 1 <= k by A316, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A322: i < len ((m,((len c) + 1)) -cut vs) and A323: k = i + 1 by A320, GRAPH_2:1; ((m,((len c) + 1)) -cut vs) . k = vs . ((m1 + 1) + i) by A4, A217, A254, A255, A322, A323, Lm2 .= fvs . ((Sgm domfvs) . k) by A317, A321, A323, GRFUNC_1:2 .= y by A315, A316, FUNCT_1:13 ; hence p in (m,((len c) + 1)) -cut vs by A313, A318, FUNCT_1:1; ::_thesis: verum end; then (m,((len c) + 1)) -cut vs = fvs * (Sgm domfvs) by TARSKI:1; hence Seq fvs = p1 by A237, FINSEQ_1:def_14; ::_thesis: verum end; supposeA324: ( n <> 1 & m = len vs ) ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) then 1 < n by A3, XXREAL_0:1; then 1 + 1 <= n by NAT_1:13; then A325: (1 + 1) - 1 <= n - 1 by XREAL_1:9; n < len vs by A4, A5, XXREAL_0:2; then A326: n - 1 < ((len c) + 1) - 1 by A8, XREAL_1:9; A327: 1 <= n1 + 1 by NAT_1:12; reconsider c1 = (1,n1) -cut c as oriented Chain of G by A11, A325, A326, Th12; set pp = (1,n) -cut vs; A328: n <= len vs by A4, A5, XXREAL_0:2; A329: (1,n) -cut vs is_oriented_vertex_seq_of c1 by A2, A12, A325, A326, Th13; then A330: len ((1,n) -cut vs) = (len c1) + 1 by Def5; set domfc = { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } ; deffunc H1( set ) -> set = c . \$1; consider fc being Function such that A331: dom fc = { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } and A332: for x being set st x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } holds fc . x = H1(x) from FUNCT_1:sch_3(); { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } c= Seg (len c) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } or x in Seg (len c) ) assume x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } ; ::_thesis: x in Seg (len c) then consider kk being Element of NAT such that A333: x = kk and A334: 1 <= kk and A335: kk <= n1 ; kk <= len c by A11, A326, A335, XXREAL_0:2; hence x in Seg (len c) by A333, A334, FINSEQ_1:1; ::_thesis: verum end; then reconsider fc = fc as FinSubsequence by A331, FINSEQ_1:def_12; fc c= c proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fc or p in c ) assume A336: p in fc ; ::_thesis: p in c then consider x, y being set such that A337: [x,y] = p by RELAT_1:def_1; A338: x in dom fc by A336, A337, FUNCT_1:1; A339: y = fc . x by A336, A337, FUNCT_1:1; consider kk being Element of NAT such that A340: x = kk and A341: 1 <= kk and A342: kk <= n1 by A331, A338; kk <= len c by A11, A326, A342, XXREAL_0:2; then A343: x in dom c by A340, A341, FINSEQ_3:25; y = c . kk by A331, A332, A338, A339, A340; hence p in c by A337, A340, A343, FUNCT_1:1; ::_thesis: verum end; then reconsider fc = fc as Subset of c ; take fc ; ::_thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) set domfvs = { k where k is Element of NAT : ( 1 <= k & k <= n ) } ; deffunc H2( set ) -> set = vs . \$1; consider fvs being Function such that A344: dom fvs = { k where k is Element of NAT : ( 1 <= k & k <= n ) } and A345: for x being set st x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } holds fvs . x = H2(x) from FUNCT_1:sch_3(); { k where k is Element of NAT : ( 1 <= k & k <= n ) } c= Seg (len vs) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } or x in Seg (len vs) ) assume x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } ; ::_thesis: x in Seg (len vs) then consider kk being Element of NAT such that A346: x = kk and A347: 1 <= kk and A348: kk <= n ; kk <= len vs by A328, A348, XXREAL_0:2; hence x in Seg (len vs) by A346, A347, FINSEQ_1:1; ::_thesis: verum end; then reconsider fvs = fvs as FinSubsequence by A344, FINSEQ_1:def_12; fvs c= vs proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fvs or p in vs ) assume A349: p in fvs ; ::_thesis: p in vs then consider x, y being set such that A350: [x,y] = p by RELAT_1:def_1; A351: x in dom fvs by A349, A350, FUNCT_1:1; A352: y = fvs . x by A349, A350, FUNCT_1:1; consider kk being Element of NAT such that A353: x = kk and A354: 1 <= kk and A355: kk <= n by A344, A351; kk <= len vs by A328, A355, XXREAL_0:2; then A356: x in dom vs by A353, A354, FINSEQ_3:25; y = vs . kk by A344, A345, A351, A352, A353; hence p in vs by A350, A353, A356, FUNCT_1:1; ::_thesis: verum end; then reconsider fvs = fvs as Subset of vs ; take fvs ; ::_thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) take c9 = c1; ::_thesis: ex vs1 being FinSequence of the carrier of G st ( len c9 < len c & vs1 is_oriented_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 ) take p1 = (1,n) -cut vs; ::_thesis: ( len c9 < len c & p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) A357: (len c1) + 1 = n1 + 1 by A11, A326, A327, Lm2; then A358: len c1 = n - 1 by A10, XREAL_0:def_2; thus len c9 < len c by A10, A326, A357, XREAL_0:def_2; ::_thesis: ( p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) thus p1 is_oriented_vertex_seq_of c9 by A2, A12, A325, A326, Th13; ::_thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) len p1 = (len c1) + 1 by A329, Def5; hence len p1 < len vs by A4, A5, A358, XXREAL_0:2; ::_thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) thus vs . 1 = p1 . 1 by A3, A328, GRAPH_2:12; ::_thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 ) thus vs . (len vs) = p1 . (len p1) by A3, A4, A6, A324, GRAPH_2:12; ::_thesis: ( Seq fc = c9 & Seq fvs = p1 ) { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } c= Seg (len c) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } or x in Seg (len c) ) assume x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } ; ::_thesis: x in Seg (len c) then consider k being Element of NAT such that A359: x = k and A360: 1 <= k and A361: k <= n1 ; k <= len c by A11, A326, A361, XXREAL_0:2; hence x in Seg (len c) by A359, A360, FINSEQ_1:1; ::_thesis: verum end; then reconsider domfc = { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } as finite set by FINSET_1:1; domfc = Seg n1 by FINSEQ_1:def_1; then A362: Sgm domfc = idseq n1 by FINSEQ_3:48; then A363: dom (Sgm domfc) = Seg n1 by RELAT_1:45; set SL = Sgm domfc; now__::_thesis:_for_p_being_set_holds_ (_(_p_in_c1_implies_p_in_fc_*_(Sgm_domfc)_)_&_(_p_in_fc_*_(Sgm_domfc)_implies_p_in_c1_)_) let p be set ; ::_thesis: ( ( p in c1 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c1 ) ) hereby ::_thesis: ( p in fc * (Sgm domfc) implies p in c1 ) assume A364: p in c1 ; ::_thesis: p in fc * (Sgm domfc) then consider x, y being set such that A365: p = [x,y] by RELAT_1:def_1; A366: x in dom c1 by A364, A365, FUNCT_1:1; A367: y = c1 . x by A364, A365, FUNCT_1:1; reconsider k = x as Element of NAT by A366; A368: 1 <= k by A366, FINSEQ_3:25; A369: k <= len c1 by A366, FINSEQ_3:25; then A370: x in dom (Sgm domfc) by A357, A363, A368, FINSEQ_1:1; then A371: k = (Sgm domfc) . k by A362, A363, FUNCT_1:18; A372: k in domfc by A357, A368, A369; then A373: x in dom (fc * (Sgm domfc)) by A331, A370, A371, FUNCT_1:11; 0 + 1 <= k by A366, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A374: i < n1 and A375: k = i + 1 by A357, A369, GRAPH_2:1; (fc * (Sgm domfc)) . x = fc . k by A371, A373, FUNCT_1:12 .= c . (1 + i) by A331, A372, A375, GRFUNC_1:2 .= y by A11, A326, A327, A357, A367, A374, A375, Lm2 ; hence p in fc * (Sgm domfc) by A365, A373, FUNCT_1:1; ::_thesis: verum end; assume A376: p in fc * (Sgm domfc) ; ::_thesis: p in c1 then consider x, y being set such that A377: p = [x,y] by RELAT_1:def_1; A378: x in dom (fc * (Sgm domfc)) by A376, A377, FUNCT_1:1; A379: y = (fc * (Sgm domfc)) . x by A376, A377, FUNCT_1:1; A380: (fc * (Sgm domfc)) . x = fc . ((Sgm domfc) . x) by A378, FUNCT_1:12; A381: x in dom (Sgm domfc) by A378, FUNCT_1:11; then x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } by A363, FINSEQ_1:def_1; then consider k being Element of NAT such that A382: k = x and A383: 1 <= k and A384: k <= n1 ; A385: k in dom fc by A331, A383, A384; A386: k = (Sgm domfc) . k by A362, A363, A381, A382, FUNCT_1:18; A387: k in dom c1 by A357, A383, A384, FINSEQ_3:25; 0 + 1 <= k by A383; then ex i being Element of NAT st ( 0 <= i & i < n1 & k = i + 1 ) by A384, GRAPH_2:1; then c1 . k = c . k by A11, A326, A327, A357, Lm2 .= y by A379, A380, A382, A385, A386, GRFUNC_1:2 ; hence p in c1 by A377, A382, A387, FUNCT_1:1; ::_thesis: verum end; then c1 = fc * (Sgm domfc) by TARSKI:1; hence Seq fc = c9 by A331, FINSEQ_1:def_14; ::_thesis: Seq fvs = p1 { k where k is Element of NAT : ( 1 <= k & k <= n ) } c= Seg (len vs) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } or x in Seg (len vs) ) assume x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } ; ::_thesis: x in Seg (len vs) then consider k being Element of NAT such that A388: x = k and A389: 1 <= k and A390: k <= n ; k <= len vs by A328, A390, XXREAL_0:2; hence x in Seg (len vs) by A388, A389, FINSEQ_1:1; ::_thesis: verum end; then reconsider domfvs = { k where k is Element of NAT : ( 1 <= k & k <= n ) } as finite set by FINSET_1:1; domfvs = Seg n by FINSEQ_1:def_1; then A391: Sgm domfvs = idseq n by FINSEQ_3:48; then A392: dom (Sgm domfvs) = Seg n by RELAT_1:45; set SL = Sgm domfvs; now__::_thesis:_for_p_being_set_holds_ (_(_p_in_(1,n)_-cut_vs_implies_p_in_fvs_*_(Sgm_domfvs)_)_&_(_p_in_fvs_*_(Sgm_domfvs)_implies_p_in_(1,n)_-cut_vs_)_) let p be set ; ::_thesis: ( ( p in (1,n) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs ) ) hereby ::_thesis: ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs ) assume A393: p in (1,n) -cut vs ; ::_thesis: p in fvs * (Sgm domfvs) then consider x, y being set such that A394: p = [x,y] by RELAT_1:def_1; A395: x in dom ((1,n) -cut vs) by A393, A394, FUNCT_1:1; A396: y = ((1,n) -cut vs) . x by A393, A394, FUNCT_1:1; reconsider k = x as Element of NAT by A395; A397: 1 <= k by A395, FINSEQ_3:25; A398: k <= len ((1,n) -cut vs) by A395, FINSEQ_3:25; then A399: x in dom (Sgm domfvs) by A330, A358, A392, A397, FINSEQ_1:1; then A400: k = (Sgm domfvs) . k by A391, A392, FUNCT_1:18; A401: k in domfvs by A330, A358, A397, A398; then A402: x in dom (fvs * (Sgm domfvs)) by A344, A399, A400, FUNCT_1:11; 0 + 1 <= k by A395, FINSEQ_3:25; then consider i being Element of NAT such that 0 <= i and A403: i < n and A404: k = i + 1 by A330, A358, A398, GRAPH_2:1; (fvs * (Sgm domfvs)) . x = fvs . k by A400, A402, FUNCT_1:12 .= vs . (1 + i) by A344, A401, A404, GRFUNC_1:2 .= y by A3, A328, A330, A358, A396, A403, A404, GRAPH_2:def_1 ; hence p in fvs * (Sgm domfvs) by A394, A402, FUNCT_1:1; ::_thesis: verum end; assume A405: p in fvs * (Sgm domfvs) ; ::_thesis: p in (1,n) -cut vs then consider x, y being set such that A406: p = [x,y] by RELAT_1:def_1; A407: x in dom (fvs * (Sgm domfvs)) by A405, A406, FUNCT_1:1; A408: y = (fvs * (Sgm domfvs)) . x by A405, A406, FUNCT_1:1; A409: (fvs * (Sgm domfvs)) . x = fvs . ((Sgm domfvs) . x) by A407, FUNCT_1:12; A410: x in dom (Sgm domfvs) by A407, FUNCT_1:11; then x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } by A392, FINSEQ_1:def_1; then consider k being Element of NAT such that A411: k = x and A412: 1 <= k and A413: k <= n ; A414: k in dom fvs by A344, A412, A413; A415: k = (Sgm domfvs) . k by A391, A392, A410, A411, FUNCT_1:18; A416: k in dom ((1,n) -cut vs) by A330, A358, A412, A413, FINSEQ_3:25; 0 + 1 <= k by A412; then ex i being Element of NAT st ( 0 <= i & i < n & k = i + 1 ) by A413, GRAPH_2:1; then ((1,n) -cut vs) . k = vs . k by A3, A328, A330, A358, GRAPH_2:def_1 .= y by A408, A409, A411, A414, A415, GRFUNC_1:2 ; hence p in (1,n) -cut vs by A406, A411, A416, FUNCT_1:1; ::_thesis: verum end; then (1,n) -cut vs = fvs * (Sgm domfvs) by TARSKI:1; hence Seq fvs = p1 by A344, FINSEQ_1:def_14; ::_thesis: verum end; end; end; theorem :: GRAPH_4:21 for G being Graph for vs being FinSequence of the carrier of G for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) proof let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) let c be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) ) assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) percases ( c is Simple or not c is Simple ) ; supposeA2: c is Simple ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) reconsider fc = c as Subset of c by GRAPH_2:26; reconsider fvs = vs as Subset of vs by GRAPH_2:26; reconsider sc = c as oriented simple Chain of G by A2, Th19; take fc ; ::_thesis: ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) take fvs ; ::_thesis: ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) take sc ; ::_thesis: ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) take vs ; ::_thesis: ( Seq fc = sc & Seq fvs = vs & vs is_oriented_vertex_seq_of sc & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) thus ( Seq fc = sc & Seq fvs = vs ) by FINSEQ_3:116; ::_thesis: ( vs is_oriented_vertex_seq_of sc & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) thus vs is_oriented_vertex_seq_of sc by A1; ::_thesis: ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; ::_thesis: verum end; supposeA3: not c is Simple ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) defpred S1[ Nat] means ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = \$1 & not c1 is Simple ); S1[ len c] proof reconsider fc = c as Subset of c by GRAPH_2:26; reconsider fvs = vs as Subset of vs by GRAPH_2:26; take fc ; ::_thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = len c & not c1 is Simple ) take fvs ; ::_thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = len c & not c1 is Simple ) take c ; ::_thesis: ex vs1 being FinSequence of the carrier of G st ( Seq fc = c & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c = len c & not c is Simple ) take vs ; ::_thesis: ( Seq fc = c & Seq fvs = vs & vs is_oriented_vertex_seq_of c & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple ) thus ( Seq fc = c & Seq fvs = vs ) by FINSEQ_3:116; ::_thesis: ( vs is_oriented_vertex_seq_of c & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple ) thus vs is_oriented_vertex_seq_of c by A1; ::_thesis: ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple ) thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; ::_thesis: ( len c = len c & not c is Simple ) thus ( len c = len c & not c is Simple ) by A3; ::_thesis: verum end; then A4: ex k being Nat st S1[k] ; consider k being Nat such that A5: ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A4); consider fc being Subset of c, fvs being Subset of vs, c1 being oriented Chain of G, vs1 being FinSequence of the carrier of G such that A6: Seq fc = c1 and A7: Seq fvs = vs1 and A8: vs1 is_oriented_vertex_seq_of c1 and A9: vs . 1 = vs1 . 1 and A10: vs . (len vs) = vs1 . (len vs1) and A11: len c1 = k and A12: not c1 is Simple by A5; consider fc1 being Subset of c1, fvs1 being Subset of vs1, c2 being oriented Chain of G, vs2 being FinSequence of the carrier of G such that A13: len c2 < len c1 and A14: vs2 is_oriented_vertex_seq_of c2 and len vs2 < len vs1 and A15: vs1 . 1 = vs2 . 1 and A16: vs1 . (len vs1) = vs2 . (len vs2) and A17: Seq fc1 = c2 and A18: Seq fvs1 = vs2 by A8, A12, Th20; reconsider fc9 = fc | (rng ((Sgm (dom fc)) | (dom fc1))) as Subset of c by GRAPH_2:27; A19: Seq fc9 = c2 by A6, A17, GRAPH_2:28; reconsider fvs9 = fvs | (rng ((Sgm (dom fvs)) | (dom fvs1))) as Subset of vs by GRAPH_2:27; A20: Seq fvs9 = vs2 by A7, A18, GRAPH_2:28; now__::_thesis:_(_c2_is_oriented_Simple_Chain_of_G_implies_ex_fc9_being_Subset_of_c_ex_sc_being_oriented_simple_Chain_of_G_ex_fc_being_Subset_of_c_ex_fvs_being_Subset_of_vs_ex_sc_being_oriented_simple_Chain_of_G_ex_vs1_being_FinSequence_of_the_carrier_of_G_st_ (_Seq_fc_=_sc_&_Seq_fvs_=_vs1_&_vs1_is_oriented_vertex_seq_of_sc_&_vs_._1_=_vs1_._1_&_vs_._(len_vs)_=_vs1_._(len_vs1)_)_) assume c2 is oriented Simple Chain of G ; ::_thesis: ex fc9 being Subset of c ex sc being oriented simple Chain of G ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) then reconsider sc = c2 as oriented simple Chain of G by Th19; take fc9 = fc9; ::_thesis: ex sc being oriented simple Chain of G ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) take sc = sc; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) Seq fc9 = sc by A6, A17, GRAPH_2:28; hence ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) by A9, A10, A14, A15, A16, A20; ::_thesis: verum end; hence ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) by A5, A9, A10, A11, A13, A14, A15, A16, A19, A20; ::_thesis: verum end; end; end; theorem :: GRAPH_4:22 for p being FinSequence for n being Element of NAT for G being Graph st p is OrientedPath of G holds p | (Seg n) is OrientedPath of G proof let p be FinSequence; ::_thesis: for n being Element of NAT for G being Graph st p is OrientedPath of G holds p | (Seg n) is OrientedPath of G let n be Element of NAT ; ::_thesis: for G being Graph st p is OrientedPath of G holds p | (Seg n) is OrientedPath of G let G be Graph; ::_thesis: ( p is OrientedPath of G implies p | (Seg n) is OrientedPath of G ) assume A1: p is OrientedPath of G ; ::_thesis: p | (Seg n) is OrientedPath of G then reconsider p9 = p | (Seg n) as oriented Chain of G by Th16; reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15; now__::_thesis:_for_n1,_m1_being_Element_of_NAT_st_1_<=_n1_&_n1_<_m1_&_m1_<=_len_q_holds_ q_._n1_<>_q_._m1 let n1, m1 be Element of NAT ; ::_thesis: ( 1 <= n1 & n1 < m1 & m1 <= len q implies q . n1 <> q . m1 ) assume that A2: 1 <= n1 and A3: n1 < m1 and A4: m1 <= len q ; ::_thesis: q . n1 <> q . m1 1 < m1 by A2, A3, XXREAL_0:2; then m1 in dom q by A4, FINSEQ_3:25; then A5: q . m1 = p . m1 by FUNCT_1:47; n1 < len q by A3, A4, XXREAL_0:2; then n1 in dom q by A2, FINSEQ_3:25; then A6: q . n1 = p . n1 by FUNCT_1:47; dom q c= dom p by RELAT_1:60; then dom q c= Seg (len p) by FINSEQ_1:def_3; then Seg (len q) c= Seg (len p) by FINSEQ_1:def_3; then len q <= len p by FINSEQ_1:5; then m1 <= len p by A4, XXREAL_0:2; hence q . n1 <> q . m1 by A1, A2, A3, A5, A6, GRAPH_1:def_16; ::_thesis: verum end; then p9 is Path of G by GRAPH_1:def_16; hence p | (Seg n) is OrientedPath of G ; ::_thesis: verum end; theorem Th23: :: GRAPH_4:23 for G being Graph for sc being oriented simple Chain of G holds sc is OrientedPath of G proof let G be Graph; ::_thesis: for sc being oriented simple Chain of G holds sc is OrientedPath of G let sc be oriented simple Chain of G; ::_thesis: sc is OrientedPath of G assume sc is not OrientedPath of G ; ::_thesis: contradiction then consider m, n being Element of NAT such that A1: 1 <= m and A2: m < n and A3: n <= len sc and A4: sc . m = sc . n by GRAPH_1:def_16; sc is Simple by Th18; then consider vs being FinSequence of the carrier of G such that A5: vs is_oriented_vertex_seq_of sc and A6: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds ( n = 1 & m = len vs ) by Def7; A7: len vs = (len sc) + 1 by A5, Def5; A8: m <= len sc by A2, A3, XXREAL_0:2; A9: 1 <= n by A1, A2, XXREAL_0:2; A10: n <= len vs by A3, A7, NAT_1:12; A11: m + 1 < n + 1 by A2, XREAL_1:6; A12: n + 1 <= len vs by A3, A7, XREAL_1:6; A13: m < n + 1 by A11, NAT_1:12; set v1 = vs /. m; set v2 = vs /. (m + 1); A14: sc . m orientedly_joins vs /. m,vs /. (m + 1) by A1, A5, A8, Def5; set v19 = vs /. n; set v29 = vs /. (n + 1); A15: sc . n orientedly_joins vs /. n,vs /. (n + 1) by A3, A5, A9, Def5; then A16: vs /. m = vs /. n by A4, A14, Th2; A17: vs /. (m + 1) = vs /. (n + 1) by A4, A14, A15, Th2; A18: m <= len vs by A12, A13, XXREAL_0:2; A19: m + 1 <= len vs by A11, A12, XXREAL_0:2; A20: vs /. m = vs . m by A1, A18, FINSEQ_4:15; A21: vs /. (m + 1) = vs . (m + 1) by A19, FINSEQ_4:15, NAT_1:12; A22: vs /. n = vs . n by A9, A10, FINSEQ_4:15; A23: vs /. (n + 1) = vs . (n + 1) by A12, FINSEQ_4:15, NAT_1:12; m = 1 by A1, A2, A6, A10, A16, A20, A22; hence contradiction by A6, A11, A12, A17, A21, A23; ::_thesis: verum end; theorem :: GRAPH_4:24 for G being Graph for c1 being FinSequence holds ( ( c1 is oriented Simple Chain of G implies c1 is oriented simple Chain of G ) & ( c1 is oriented simple Chain of G implies c1 is oriented Simple Chain of G ) & ( c1 is oriented simple Chain of G implies c1 is OrientedPath of G ) ) by Th18, Th19, Th23;