:: GLIB_003 semantic presentation begin definition let D be set ; let fs be FinSequence of D; let fss be Subset of fs; :: original: Seq redefine func Seq fss -> FinSequence of D; correctness coherence Seq fss is FinSequence of D; proof now__::_thesis:_for_y_being_set_st_y_in_rng_(Seq_fss)_holds_ y_in_D let y be set ; ::_thesis: ( y in rng (Seq fss) implies y in D ) assume y in rng (Seq fss) ; ::_thesis: y in D then consider x being set such that A1: x in dom (Seq fss) and A2: (Seq fss) . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A1; ex n being Element of NAT st ( n in dom fs & x <= n & y = fs . n ) by A1, A2, GLIB_001:4; then y in rng fs by FUNCT_1:def_3; hence y in D ; ::_thesis: verum end; then rng (Seq fss) c= D by TARSKI:def_3; hence Seq fss is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum end; end; theorem :: GLIB_003:1 for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being set for p being FinSequence st p = ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ^ <*x10*> holds ( len p = 10 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 & p . 10 = x10 ) proof let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be set ; ::_thesis: for p being FinSequence st p = ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ^ <*x10*> holds ( len p = 10 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 & p . 10 = x10 ) let p be FinSequence; ::_thesis: ( p = ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ^ <*x10*> implies ( len p = 10 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 & p . 10 = x10 ) ) set pa = (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>; A1: ( ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 1 = x1 & ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 2 = x2 ) by FINSEQ_1:71; A2: ( ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 5 = x5 & ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 6 = x6 ) by FINSEQ_1:71; A3: ( ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 7 = x7 & ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 8 = x8 ) by FINSEQ_1:71; A4: len ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) = 9 by FINSEQ_1:71; then A5: dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) = Seg 9 by FINSEQ_1:def_3; then A6: ( 3 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) & 4 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ) by FINSEQ_1:1; A7: ( ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 9 = x9 & 9 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ) by A5, FINSEQ_1:1, FINSEQ_1:71; assume A8: p = ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ^ <*x10*> ; ::_thesis: ( len p = 10 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 & p . 10 = x10 ) hence len p = (len ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>)) + (len <*x10*>) by FINSEQ_1:22 .= 9 + 1 by A4, FINSEQ_1:40 .= 10 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 & p . 10 = x10 ) A9: ( ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 3 = x3 & ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) . 4 = x4 ) by FINSEQ_1:71; A10: ( 7 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) & 8 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ) by A5, FINSEQ_1:1; A11: ( 5 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) & 6 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ) by A5, FINSEQ_1:1; ( 1 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) & 2 in dom ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ) by A5, FINSEQ_1:1; hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 ) by A8, A1, A9, A2, A3, A6, A11, A10, A7, FINSEQ_1:def_7; ::_thesis: p . 10 = x10 thus p . 10 = p . ((len ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>)) + 1) by A4 .= x10 by A8, FINSEQ_1:42 ; ::_thesis: verum end; theorem Th2: :: GLIB_003:2 for fs being FinSequence of REAL for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) holds Sum (Seq fss) <= Sum fs proof let fs be FinSequence of REAL ; ::_thesis: for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) holds Sum (Seq fss) <= Sum fs let fss be Subset of fs; ::_thesis: ( ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) implies Sum (Seq fss) <= Sum fs ) defpred S1[ Element of NAT ] means for fs being FinSequence of REAL for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) & len (Seq fss) = $1 holds Sum (Seq fss) <= Sum fs; assume A1: for i being Element of NAT st i in dom fs holds 0 <= fs . i ; ::_thesis: Sum (Seq fss) <= Sum fs A2: len (Seq fss) = len (Seq fss) ; now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ for_fs_being_FinSequence_of_REAL_ for_fss_being_Subset_of_fs_st_(_for_i_being_Element_of_NAT_st_i_in_dom_fs_holds_ 0_<=_fs_._i_)_&_len_(Seq_fss)_=_k_+_1_holds_ Sum_(Seq_fss)_<=_Sum_fs let k be Element of NAT ; ::_thesis: ( S1[k] implies for fs being FinSequence of REAL for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) & len (Seq fss) = k + 1 holds Sum (Seq fss) <= Sum fs ) assume A3: S1[k] ; ::_thesis: for fs being FinSequence of REAL for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) & len (Seq fss) = k + 1 holds Sum (Seq fss) <= Sum fs let fs be FinSequence of REAL ; ::_thesis: for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) & len (Seq fss) = k + 1 holds Sum (Seq fss) <= Sum fs let fss be Subset of fs; ::_thesis: ( ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) & len (Seq fss) = k + 1 implies Sum (Seq fss) <= Sum fs ) assume that A4: for i being Element of NAT st i in dom fs holds 0 <= fs . i and A5: len (Seq fss) = k + 1 ; ::_thesis: Sum (Seq fss) <= Sum fs consider q being FinSequence of REAL , z being Real such that A6: Seq fss = q ^ <*z*> by A5, FINSEQ_2:19; card fss = k + 1 by A5, GLIB_001:5; then dom fss <> {} by CARD_1:27, RELAT_1:41; then consider d being set such that A7: d in dom fss by XBOOLE_0:def_1; A8: dom fss c= dom fs by GRAPH_2:25; then A9: d in dom fs by A7; defpred S2[ Nat] means $1 in dom fss; consider L being Nat such that A10: dom fss c= Seg L by FINSEQ_1:def_12; A11: for n being Nat st S2[n] holds n <= L by A10, FINSEQ_1:1; reconsider d = d as Element of NAT by A9; d in dom fss by A7; then A12: ex d being Nat st S2[d] ; consider x being Nat such that A13: ( S2[x] & ( for n being Nat st S2[n] holds n <= x ) ) from NAT_1:sch_6(A11, A12); set y = fs . x; A14: len (Seq fss) = (len q) + (len <*z*>) by A6, FINSEQ_1:22; then A15: k + 1 = (len q) + 1 by A5, FINSEQ_1:39; now__::_thesis:_fs_._x_=_z set g = Sgm (dom fss); 1 <= k + 1 by NAT_1:12; then A16: len (Seq fss) in dom (Seq fss) by A5, FINSEQ_3:25; A17: len (Seq fss) = card fss by GLIB_001:5 .= card (dom fss) by CARD_1:62 .= len (Sgm (dom fss)) by A10, FINSEQ_3:39 ; A18: now__::_thesis:_not_(Sgm_(dom_fss))_._(len_(Seq_fss))_<>_x set k2 = (Sgm (dom fss)) . (len (Sgm (dom fss))); assume A19: (Sgm (dom fss)) . (len (Seq fss)) <> x ; ::_thesis: contradiction 1 <= len (Sgm (dom fss)) by A5, A17, NAT_1:12; then len (Sgm (dom fss)) in dom (Sgm (dom fss)) by FINSEQ_3:25; then A20: (Sgm (dom fss)) . (len (Sgm (dom fss))) in rng (Sgm (dom fss)) by FUNCT_1:def_3; reconsider k2 = (Sgm (dom fss)) . (len (Sgm (dom fss))) as Element of NAT ; A21: rng (Sgm (dom fss)) = dom fss by A10, FINSEQ_1:def_13; then consider v being set such that A22: v in dom (Sgm (dom fss)) and A23: (Sgm (dom fss)) . v = x by A13, FUNCT_1:def_3; reconsider v = v as Element of NAT by A22; v <= len (Sgm (dom fss)) by A22, FINSEQ_3:25; then A24: v < len (Sgm (dom fss)) by A17, A19, A23, XXREAL_0:1; 1 <= v by A22, FINSEQ_3:25; then x < k2 by A10, A23, A24, FINSEQ_1:def_13; hence contradiction by A13, A21, A20; ::_thesis: verum end; ( (Seq fss) . (len (Seq fss)) = z & Seq fss = fss * (Sgm (dom fss)) ) by A5, A6, A15, FINSEQ_1:42, FINSEQ_1:def_14; then fss . ((Sgm (dom fss)) . (len (Seq fss))) = z by A16, FUNCT_1:12; then [x,z] in fss by A13, A18, FUNCT_1:1; hence fs . x = z by FUNCT_1:1; ::_thesis: verum end; then A25: Sum (Seq fss) = (fs . x) + (Sum q) by A6, RVSUM_1:74; A26: x <= len fs by A8, A13, FINSEQ_3:25; then consider j being Nat such that A27: x + j = len fs by NAT_1:10; A28: 1 <= x by A8, A13, FINSEQ_3:25; then reconsider xx1 = x - 1 as Element of NAT by INT_1:5; set fssq = fss | (Seg xx1); reconsider fssq = fss | (Seg xx1) as Subset of fs by GRAPH_2:27; consider fsD, fsC being FinSequence of REAL such that A29: len fsD = x and len fsC = j and A30: fs = fsD ^ fsC by A27, FINSEQ_2:23; A31: xx1 + 1 = x ; then consider fsA, fsB being FinSequence of REAL such that A32: len fsA = xx1 and A33: len fsB = 1 and A34: fsD = fsA ^ fsB by A29, FINSEQ_2:23; x in dom fsD by A28, A29, FINSEQ_3:25; then A35: fs . x = fsD . x by A30, FINSEQ_1:def_7; now__::_thesis:_for_z_being_set_st_z_in_fssq_holds_ z_in_fsA let z be set ; ::_thesis: ( z in fssq implies z in fsA ) assume A36: z in fssq ; ::_thesis: z in fsA then consider a, b being set such that A37: z = [a,b] by RELAT_1:def_1; A38: a in Seg xx1 by A36, A37, RELAT_1:def_11; then reconsider a = a as Element of NAT ; A39: a <= xx1 by A38, FINSEQ_1:1; A40: 1 <= a by A38, FINSEQ_1:1; then A41: a in dom fsA by A32, A39, FINSEQ_3:25; A42: b = fs . a by A36, A37, FUNCT_1:1; a + 0 <= x by A31, A39, XREAL_1:7; then a in dom fsD by A29, A40, FINSEQ_3:25; then b = fsD . a by A30, A42, FINSEQ_1:def_7; then b = fsA . a by A34, A41, FINSEQ_1:def_7; hence z in fsA by A37, A41, FUNCT_1:1; ::_thesis: verum end; then reconsider fssq = fssq as Subset of fsA by TARSKI:def_3; now__::_thesis:_(_len_q_=_len_(Seq_fssq)_&_(_for_n_being_Nat_st_1_<=_n_&_n_<=_len_q_holds_ q_._n_=_(Seq_fssq)_._n_)_) A43: now__::_thesis:_for_z_being_set_st_z_in_{[x,(fs_._x)]}_holds_ z_in_fss let z be set ; ::_thesis: ( z in {[x,(fs . x)]} implies z in fss ) assume z in {[x,(fs . x)]} ; ::_thesis: z in fss then A44: z = [x,(fs . x)] by TARSKI:def_1; [x,(fss . x)] in fss by A13, FUNCT_1:1; hence z in fss by A44, FUNCT_1:1; ::_thesis: verum end; now__::_thesis:_for_z_being_set_holds_ (_(_z_in_fssq_implies_z_in_fss_\_{[x,(fs_._x)]}_)_&_(_z_in_fss_\_{[x,(fs_._x)]}_implies_z_in_fssq_)_) [x,(fs . x)] in {[x,(fs . x)]} by TARSKI:def_1; then A45: [x,(fs . x)] in fss by A43; let z be set ; ::_thesis: ( ( z in fssq implies z in fss \ {[x,(fs . x)]} ) & ( z in fss \ {[x,(fs . x)]} implies z in fssq ) ) hereby ::_thesis: ( z in fss \ {[x,(fs . x)]} implies z in fssq ) assume A46: z in fssq ; ::_thesis: z in fss \ {[x,(fs . x)]} then consider a, b being set such that A47: z = [a,b] by RELAT_1:def_1; A48: a in Seg xx1 by A46, A47, RELAT_1:def_11; then reconsider a = a as Element of NAT ; a <= xx1 by A48, FINSEQ_1:1; then a < x by A31, NAT_1:13; then [a,b] <> [x,(fs . x)] by XTUPLE_0:1; then A49: not z in {[x,(fs . x)]} by A47, TARSKI:def_1; z in fss by A46, A47, RELAT_1:def_11; hence z in fss \ {[x,(fs . x)]} by A49, XBOOLE_0:def_5; ::_thesis: verum end; assume A50: z in fss \ {[x,(fs . x)]} ; ::_thesis: z in fssq then consider a, b being set such that A51: z = [a,b] by RELAT_1:def_1; A52: a in dom fs by A50, A51, FUNCT_1:1; A53: z in fss by A50, XBOOLE_0:def_5; then A54: a in dom fss by A51, FUNCT_1:1; reconsider a = a as Element of NAT by A52; A55: a <= x by A13, A54; not z in {[x,(fs . x)]} by A50, XBOOLE_0:def_5; then ( a <> x or b <> fs . x ) by A51, TARSKI:def_1; then a <> x by A50, A51, A45, FUNCT_1:def_1; then a < x by A55, XXREAL_0:1; then a + 1 <= x by NAT_1:13; then A56: (a + 1) - 1 <= x - 1 by XREAL_1:13; 1 <= a by A52, FINSEQ_3:25; then a in Seg xx1 by A56, FINSEQ_1:1; hence z in fssq by A51, A53, RELAT_1:def_11; ::_thesis: verum end; then A57: fssq = fss \ {[x,(fs . x)]} by TARSKI:1; now__::_thesis:_for_z_being_set_holds_ (_(_z_in_dom_fss_implies_z_in_(dom_fssq)_\/_{x}_)_&_(_z_in_(dom_fssq)_\/_{x}_implies_z_in_dom_fss_)_) let z be set ; ::_thesis: ( ( z in dom fss implies z in (dom fssq) \/ {x} ) & ( z in (dom fssq) \/ {x} implies z in dom fss ) ) hereby ::_thesis: ( z in (dom fssq) \/ {x} implies z in dom fss ) assume A58: z in dom fss ; ::_thesis: z in (dom fssq) \/ {x} then A59: [z,(fss . z)] in fss by FUNCT_1:1; then A60: z in dom fs by FUNCT_1:1; then reconsider z9 = z as Element of NAT ; A61: 1 <= z9 by A60, FINSEQ_3:25; A62: z9 <= x by A13, A58; now__::_thesis:_(_not_z_in_{x}_implies_z_in_dom_fssq_) assume not z in {x} ; ::_thesis: z in dom fssq then z <> x by TARSKI:def_1; then z9 < xx1 + 1 by A62, XXREAL_0:1; then z9 <= xx1 by NAT_1:13; then z9 in Seg xx1 by A61, FINSEQ_1:1; then [z,(fss . z)] in fssq by A59, RELAT_1:def_11; hence z in dom fssq by FUNCT_1:1; ::_thesis: verum end; hence z in (dom fssq) \/ {x} by XBOOLE_0:def_3; ::_thesis: verum end; assume A63: z in (dom fssq) \/ {x} ; ::_thesis: z in dom fss now__::_thesis:_z_in_dom_fss percases ( z in dom fssq or z in {x} ) by A63, XBOOLE_0:def_3; suppose z in dom fssq ; ::_thesis: z in dom fss then [z,(fssq . z)] in fssq by FUNCT_1:1; then [z,(fssq . z)] in fss by RELAT_1:def_11; hence z in dom fss by FUNCT_1:1; ::_thesis: verum end; suppose z in {x} ; ::_thesis: z in dom fss hence z in dom fss by A13, TARSKI:def_1; ::_thesis: verum end; end; end; hence z in dom fss ; ::_thesis: verum end; then A64: dom fss = (dom fssq) \/ {x} by TARSKI:1; A65: card fss = k + 1 by A5, GLIB_001:5; A66: now__::_thesis:_for_m,_n_being_Element_of_NAT_st_m_in_dom_fssq_&_n_in_{x}_holds_ m_<_n let m, n be Element of NAT ; ::_thesis: ( m in dom fssq & n in {x} implies m < n ) assume that A67: m in dom fssq and A68: n in {x} ; ::_thesis: m < n [m,(fssq . m)] in fssq by A67, FUNCT_1:1; then m in Seg xx1 by RELAT_1:def_11; then A69: m <= xx1 by FINSEQ_1:1; n = x by A68, TARSKI:def_1; hence m < n by A31, A69, NAT_1:13; ::_thesis: verum end; {[x,(fs . x)]} c= fss by A43, TARSKI:def_3; then A70: card fssq = (card fss) - (card {[x,(fs . x)]}) by A57, CARD_2:44 .= (k + 1) - 1 by A65, CARD_1:30 .= k ; hence len q = len (Seq fssq) by A15, GLIB_001:5; ::_thesis: for n being Nat st 1 <= n & n <= len q holds q . n = (Seq fssq) . n let n be Nat; ::_thesis: ( 1 <= n & n <= len q implies q . n = (Seq fssq) . n ) set x1 = (Sgm (dom fss)) . n; set x2 = (Sgm (dom fssq)) . n; assume that A71: 1 <= n and A72: n <= len q ; ::_thesis: q . n = (Seq fssq) . n n in dom q by A71, A72, FINSEQ_3:25; then A73: q . n = (Seq fss) . n by A6, FINSEQ_1:def_7; A74: ex lk being Nat st dom fssq c= Seg lk by FINSEQ_1:def_12; then len (Sgm (dom fssq)) = card (dom fssq) by FINSEQ_3:39 .= k by A70, CARD_1:62 ; then A75: n in dom (Sgm (dom fssq)) by A15, A71, A72, FINSEQ_3:25; then (Sgm (dom fssq)) . n in rng (Sgm (dom fssq)) by FUNCT_1:def_3; then (Sgm (dom fssq)) . n in dom fssq by A74, FINSEQ_1:def_13; then [((Sgm (dom fssq)) . n),(fssq . ((Sgm (dom fssq)) . n))] in fssq by FUNCT_1:1; then [((Sgm (dom fssq)) . n),(fssq . ((Sgm (dom fssq)) . n))] in fss by RELAT_1:def_11; then A76: fss . ((Sgm (dom fssq)) . n) = fssq . ((Sgm (dom fssq)) . n) by FUNCT_1:1; n <= k + 1 by A5, A14, A72, NAT_1:12; then A77: n in dom (Seq fss) by A5, A71, FINSEQ_3:25; Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def_14; then A78: q . n = fss . ((Sgm (dom fss)) . n) by A73, A77, FUNCT_1:12; A79: Seq fssq = fssq * (Sgm (dom fssq)) by FINSEQ_1:def_14; len (Seq fssq) = card fssq by GLIB_001:5; then n in dom (Seq fssq) by A15, A70, A71, A72, FINSEQ_3:25; then A80: (Seq fssq) . n = fssq . ((Sgm (dom fssq)) . n) by A79, FUNCT_1:12; now__::_thesis:_for_z_being_set_st_z_in_{x}_holds_ z_in_Seg_(len_fs) let z be set ; ::_thesis: ( z in {x} implies z in Seg (len fs) ) assume z in {x} ; ::_thesis: z in Seg (len fs) then z = x by TARSKI:def_1; hence z in Seg (len fs) by A28, A26, FINSEQ_1:1; ::_thesis: verum end; then {x} c= Seg (len fs) by TARSKI:def_3; then Sgm (dom fss) = (Sgm (dom fssq)) ^ (Sgm {x}) by A74, A64, A66, FINSEQ_3:42; hence q . n = (Seq fssq) . n by A78, A80, A75, A76, FINSEQ_1:def_7; ::_thesis: verum end; then A81: q = Seq fssq by FINSEQ_1:14; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_fsA_holds_ 0_<=_fsA_._i A82: dom fsD c= dom fs by A30, FINSEQ_1:26; let i be Element of NAT ; ::_thesis: ( i in dom fsA implies 0 <= fsA . i ) A83: dom fsA c= dom fsD by A34, FINSEQ_1:26; assume A84: i in dom fsA ; ::_thesis: 0 <= fsA . i then fsA . i = fsD . i by A34, FINSEQ_1:def_7; then A85: fsA . i = fs . i by A30, A84, A83, FINSEQ_1:def_7; i in dom fsD by A84, A83; hence 0 <= fsA . i by A4, A85, A82; ::_thesis: verum end; then Sum q <= Sum fsA by A3, A15, A81; then (Sum (Seq fss)) + (Sum q) <= ((fs . x) + (Sum q)) + (Sum fsA) by A25, XREAL_1:7; then (Sum (Seq fss)) + (Sum q) <= ((fs . x) + (Sum fsA)) + (Sum q) ; then A86: Sum (Seq fss) <= (Sum fsA) + (fs . x) by XREAL_1:6; now__::_thesis:_for_i_being_Nat_st_i_in_dom_fsC_holds_ 0_<=_fsC_._i let i be Nat; ::_thesis: ( i in dom fsC implies 0 <= fsC . i ) assume i in dom fsC ; ::_thesis: 0 <= fsC . i then ( fs . (x + i) = fsC . i & x + i in dom fs ) by A29, A30, FINSEQ_1:28, FINSEQ_1:def_7; hence 0 <= fsC . i by A4; ::_thesis: verum end; then A87: 0 <= Sum fsC by RVSUM_1:84; 1 in dom fsB by A33, FINSEQ_3:25; then fs . x = fsB . 1 by A31, A32, A34, A35, FINSEQ_1:def_7; then A88: fsB = <*(fs . x)*> by A33, FINSEQ_1:40; Sum fs = (Sum fsD) + (Sum fsC) by A30, RVSUM_1:75 .= ((Sum fsA) + (Sum <*(fs . x)*>)) + (Sum fsC) by A34, A88, RVSUM_1:75 .= ((Sum fsA) + (fs . x)) + (Sum fsC) by FINSOP_1:11 ; then ((Sum fsA) + (fs . x)) + 0 <= Sum fs by A87, XREAL_1:7; hence Sum (Seq fss) <= Sum fs by A86, XXREAL_0:2; ::_thesis: verum end; then A89: for k being Element of NAT st S1[k] holds S1[k + 1] ; now__::_thesis:_for_fs_being_FinSequence_of_REAL_ for_fss_being_Subset_of_fs_st_(_for_i_being_Element_of_NAT_st_i_in_dom_fs_holds_ 0_<=_fs_._i_)_&_len_(Seq_fss)_=_0_holds_ Sum_(Seq_fss)_<=_Sum_fs let fs be FinSequence of REAL ; ::_thesis: for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) & len (Seq fss) = 0 holds Sum (Seq fss) <= Sum fs let fss be Subset of fs; ::_thesis: ( ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) & len (Seq fss) = 0 implies Sum (Seq fss) <= Sum fs ) assume ( ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) & len (Seq fss) = 0 ) ; ::_thesis: Sum (Seq fss) <= Sum fs then ( ( for i being Nat st i in dom fs holds 0 <= fs . i ) & Seq fss = <*> REAL ) ; hence Sum (Seq fss) <= Sum fs by RVSUM_1:72, RVSUM_1:84; ::_thesis: verum end; then A90: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A90, A89); hence Sum (Seq fss) <= Sum fs by A1, A2; ::_thesis: verum end; begin definition func WeightSelector -> Element of NAT equals :: GLIB_003:def 1 5; coherence 5 is Element of NAT ; func ELabelSelector -> Element of NAT equals :: GLIB_003:def 2 6; coherence 6 is Element of NAT ; func VLabelSelector -> Element of NAT equals :: GLIB_003:def 3 7; coherence 7 is Element of NAT ; end; :: deftheorem defines WeightSelector GLIB_003:def_1_:_ WeightSelector = 5; :: deftheorem defines ELabelSelector GLIB_003:def_2_:_ ELabelSelector = 6; :: deftheorem defines VLabelSelector GLIB_003:def_3_:_ VLabelSelector = 7; definition let G be GraphStruct; attrG is [Weighted] means :Def4: :: GLIB_003:def 4 ( WeightSelector in dom G & G . WeightSelector is ManySortedSet of the_Edges_of G ); attrG is [ELabeled] means :Def5: :: GLIB_003:def 5 ( ELabelSelector in dom G & ex f being Function st ( G . ELabelSelector = f & dom f c= the_Edges_of G ) ); attrG is [VLabeled] means :Def6: :: GLIB_003:def 6 ( VLabelSelector in dom G & ex f being Function st ( G . VLabelSelector = f & dom f c= the_Vertices_of G ) ); end; :: deftheorem Def4 defines [Weighted] GLIB_003:def_4_:_ for G being GraphStruct holds ( G is [Weighted] iff ( WeightSelector in dom G & G . WeightSelector is ManySortedSet of the_Edges_of G ) ); :: deftheorem Def5 defines [ELabeled] GLIB_003:def_5_:_ for G being GraphStruct holds ( G is [ELabeled] iff ( ELabelSelector in dom G & ex f being Function st ( G . ELabelSelector = f & dom f c= the_Edges_of G ) ) ); :: deftheorem Def6 defines [VLabeled] GLIB_003:def_6_:_ for G being GraphStruct holds ( G is [VLabeled] iff ( VLabelSelector in dom G & ex f being Function st ( G . VLabelSelector = f & dom f c= the_Vertices_of G ) ) ); registration cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] for set ; existence ex b1 being GraphStruct st ( b1 is [Graph-like] & b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) proof set V5 = {1}; set E3 = {} ; set S1 = the Function of {},{1}; set W1 = the ManySortedSet of {} ; set EL8 = the PartFunc of {},REAL; set VL6 = the PartFunc of {1},REAL; set G = (((((<*{1}*> ^ <*{}*>) ^ <* the Function of {},{1}*>) ^ <* the Function of {},{1}*>) ^ <* the ManySortedSet of {} *>) ^ <* the PartFunc of {},REAL*>) ^ <* the PartFunc of {1},REAL*>; A1: dom the PartFunc of {1},REAL c= {1} ; A2: len ((((((<*{1}*> ^ <*{}*>) ^ <* the Function of {},{1}*>) ^ <* the Function of {},{1}*>) ^ <* the ManySortedSet of {} *>) ^ <* the PartFunc of {},REAL*>) ^ <* the PartFunc of {1},REAL*>) = 7 by FINSEQ_1:69; reconsider G = (((((<*{1}*> ^ <*{}*>) ^ <* the Function of {},{1}*>) ^ <* the Function of {},{1}*>) ^ <* the ManySortedSet of {} *>) ^ <* the PartFunc of {},REAL*>) ^ <* the PartFunc of {1},REAL*> as GraphStruct ; A3: dom G = Seg 7 by A2, FINSEQ_1:def_3; then A4: ( SourceSelector in dom G & TargetSelector in dom G ) by FINSEQ_1:1; A5: ( WeightSelector in dom G & ELabelSelector in dom G ) by A3, FINSEQ_1:1; A6: ( G . WeightSelector = the ManySortedSet of {} & G . ELabelSelector = the PartFunc of {},REAL ) by FINSEQ_1:69; take G ; ::_thesis: ( G is [Graph-like] & G is [Weighted] & G is [ELabeled] & G is [VLabeled] ) A7: ( the_Vertices_of G = {1} & the_Edges_of G = {} ) by FINSEQ_1:69; A8: ( the_Source_of G = the Function of {},{1} & the_Target_of G = the Function of {},{1} ) by FINSEQ_1:69; A9: VLabelSelector in dom G by A3, FINSEQ_1:1; A10: ( G . VLabelSelector = the PartFunc of {1},REAL & dom the PartFunc of {},REAL c= {} ) by FINSEQ_1:69; ( VertexSelector in dom G & EdgeSelector in dom G ) by A3, FINSEQ_1:1; hence ( G is [Graph-like] & G is [Weighted] & G is [ELabeled] & G is [VLabeled] ) by A4, A5, A9, A7, A8, A6, A10, A1, Def4, Def5, Def6, GLIB_000:def_10; ::_thesis: verum end; end; definition mode WGraph is [Weighted] _Graph; mode EGraph is [ELabeled] _Graph; mode VGraph is [VLabeled] _Graph; mode WEGraph is [Weighted] [ELabeled] _Graph; mode WVGraph is [Weighted] [VLabeled] _Graph; mode EVGraph is [ELabeled] [VLabeled] _Graph; mode WEVGraph is [Weighted] [ELabeled] [VLabeled] _Graph; end; definition let G be WGraph; func the_Weight_of G -> ManySortedSet of the_Edges_of G equals :: GLIB_003:def 7 G . WeightSelector; coherence G . WeightSelector is ManySortedSet of the_Edges_of G by Def4; end; :: deftheorem defines the_Weight_of GLIB_003:def_7_:_ for G being WGraph holds the_Weight_of G = G . WeightSelector; definition let G be EGraph; func the_ELabel_of G -> Function equals :: GLIB_003:def 8 G . ELabelSelector; coherence G . ELabelSelector is Function proof ex f being Function st ( G . ELabelSelector = f & dom f c= the_Edges_of G ) by Def5; hence G . ELabelSelector is Function ; ::_thesis: verum end; end; :: deftheorem defines the_ELabel_of GLIB_003:def_8_:_ for G being EGraph holds the_ELabel_of G = G . ELabelSelector; definition let G be VGraph; func the_VLabel_of G -> Function equals :: GLIB_003:def 9 G . VLabelSelector; coherence G . VLabelSelector is Function proof ex f being Function st ( G . VLabelSelector = f & dom f c= the_Vertices_of G ) by Def6; hence G . VLabelSelector is Function ; ::_thesis: verum end; end; :: deftheorem defines the_VLabel_of GLIB_003:def_9_:_ for G being VGraph holds the_VLabel_of G = G . VLabelSelector; Lm1: for G being EGraph holds dom (the_ELabel_of G) c= the_Edges_of G proof let G be EGraph; ::_thesis: dom (the_ELabel_of G) c= the_Edges_of G ex f being Function st ( G . ELabelSelector = f & dom f c= the_Edges_of G ) by Def5; hence dom (the_ELabel_of G) c= the_Edges_of G ; ::_thesis: verum end; Lm2: for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G proof let G be VGraph; ::_thesis: dom (the_VLabel_of G) c= the_Vertices_of G ex f being Function st ( G . VLabelSelector = f & dom f c= the_Vertices_of G ) by Def6; hence dom (the_VLabel_of G) c= the_Vertices_of G ; ::_thesis: verum end; registration let G be _Graph; let X be set ; clusterG .set (WeightSelector,X) -> [Graph-like] ; coherence G .set (WeightSelector,X) is [Graph-like] proof not WeightSelector in _GraphSelectors by ENUMSET1:def_2; hence G .set (WeightSelector,X) is [Graph-like] by GLIB_000:10; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> [Graph-like] ; coherence G .set (ELabelSelector,X) is [Graph-like] proof not ELabelSelector in _GraphSelectors by ENUMSET1:def_2; hence G .set (ELabelSelector,X) is [Graph-like] by GLIB_000:10; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> [Graph-like] ; coherence G .set (VLabelSelector,X) is [Graph-like] proof not VLabelSelector in _GraphSelectors by ENUMSET1:def_2; hence G .set (VLabelSelector,X) is [Graph-like] by GLIB_000:10; ::_thesis: verum end; end; Lm3: for G being _Graph for X being set holds ( G .set (WeightSelector,X) == G & G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G ) proof set GS = _GraphSelectors ; let G be _Graph; ::_thesis: for X being set holds ( G .set (WeightSelector,X) == G & G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G ) let X be set ; ::_thesis: ( G .set (WeightSelector,X) == G & G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G ) set G2 = G .set (WeightSelector,X); A1: not WeightSelector in _GraphSelectors by ENUMSET1:def_2; then A2: ( the_Source_of (G .set (WeightSelector,X)) = the_Source_of G & the_Target_of (G .set (WeightSelector,X)) = the_Target_of G ) by GLIB_000:10; ( the_Vertices_of (G .set (WeightSelector,X)) = the_Vertices_of G & the_Edges_of (G .set (WeightSelector,X)) = the_Edges_of G ) by A1, GLIB_000:10; hence G .set (WeightSelector,X) == G by A2, GLIB_000:def_34; ::_thesis: ( G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G ) set G2 = G .set (ELabelSelector,X); A3: not ELabelSelector in _GraphSelectors by ENUMSET1:def_2; then A4: ( the_Source_of (G .set (ELabelSelector,X)) = the_Source_of G & the_Target_of (G .set (ELabelSelector,X)) = the_Target_of G ) by GLIB_000:10; ( the_Vertices_of (G .set (ELabelSelector,X)) = the_Vertices_of G & the_Edges_of (G .set (ELabelSelector,X)) = the_Edges_of G ) by A3, GLIB_000:10; hence G .set (ELabelSelector,X) == G by A4, GLIB_000:def_34; ::_thesis: G .set (VLabelSelector,X) == G set G2 = G .set (VLabelSelector,X); A5: not VLabelSelector in _GraphSelectors by ENUMSET1:def_2; then A6: ( the_Source_of (G .set (VLabelSelector,X)) = the_Source_of G & the_Target_of (G .set (VLabelSelector,X)) = the_Target_of G ) by GLIB_000:10; ( the_Vertices_of (G .set (VLabelSelector,X)) = the_Vertices_of G & the_Edges_of (G .set (VLabelSelector,X)) = the_Edges_of G ) by A5, GLIB_000:10; hence G .set (VLabelSelector,X) == G by A6, GLIB_000:def_34; ::_thesis: verum end; registration let G be finite _Graph; let X be set ; clusterG .set (WeightSelector,X) -> finite ; coherence G .set (WeightSelector,X) is finite proof G .set (WeightSelector,X) == G by Lm3; hence G .set (WeightSelector,X) is finite by GLIB_000:89; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> finite ; coherence G .set (ELabelSelector,X) is finite proof G .set (ELabelSelector,X) == G by Lm3; hence G .set (ELabelSelector,X) is finite by GLIB_000:89; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> finite ; coherence G .set (VLabelSelector,X) is finite proof G .set (VLabelSelector,X) == G by Lm3; hence G .set (VLabelSelector,X) is finite by GLIB_000:89; ::_thesis: verum end; end; registration let G be loopless _Graph; let X be set ; clusterG .set (WeightSelector,X) -> loopless ; coherence G .set (WeightSelector,X) is loopless proof G .set (WeightSelector,X) == G by Lm3; hence G .set (WeightSelector,X) is loopless by GLIB_000:89; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> loopless ; coherence G .set (ELabelSelector,X) is loopless proof G .set (ELabelSelector,X) == G by Lm3; hence G .set (ELabelSelector,X) is loopless by GLIB_000:89; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> loopless ; coherence G .set (VLabelSelector,X) is loopless proof G .set (VLabelSelector,X) == G by Lm3; hence G .set (VLabelSelector,X) is loopless by GLIB_000:89; ::_thesis: verum end; end; registration let G be trivial _Graph; let X be set ; clusterG .set (WeightSelector,X) -> trivial ; coherence G .set (WeightSelector,X) is trivial proof G .set (WeightSelector,X) == G by Lm3; hence G .set (WeightSelector,X) is trivial by GLIB_000:89; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> trivial ; coherence G .set (ELabelSelector,X) is trivial proof G .set (ELabelSelector,X) == G by Lm3; hence G .set (ELabelSelector,X) is trivial by GLIB_000:89; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> trivial ; coherence G .set (VLabelSelector,X) is trivial proof G .set (VLabelSelector,X) == G by Lm3; hence G .set (VLabelSelector,X) is trivial by GLIB_000:89; ::_thesis: verum end; end; registration let G be non trivial _Graph; let X be set ; clusterG .set (WeightSelector,X) -> non trivial ; coherence not G .set (WeightSelector,X) is trivial proof G .set (WeightSelector,X) == G by Lm3; hence not G .set (WeightSelector,X) is trivial by GLIB_000:89; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> non trivial ; coherence not G .set (ELabelSelector,X) is trivial proof G .set (ELabelSelector,X) == G by Lm3; hence not G .set (ELabelSelector,X) is trivial by GLIB_000:89; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> non trivial ; coherence not G .set (VLabelSelector,X) is trivial proof G .set (VLabelSelector,X) == G by Lm3; hence not G .set (VLabelSelector,X) is trivial by GLIB_000:89; ::_thesis: verum end; end; registration let G be non-multi _Graph; let X be set ; clusterG .set (WeightSelector,X) -> non-multi ; coherence G .set (WeightSelector,X) is non-multi proof G .set (WeightSelector,X) == G by Lm3; hence G .set (WeightSelector,X) is non-multi by GLIB_000:89; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> non-multi ; coherence G .set (ELabelSelector,X) is non-multi proof G .set (ELabelSelector,X) == G by Lm3; hence G .set (ELabelSelector,X) is non-multi by GLIB_000:89; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> non-multi ; coherence G .set (VLabelSelector,X) is non-multi proof G .set (VLabelSelector,X) == G by Lm3; hence G .set (VLabelSelector,X) is non-multi by GLIB_000:89; ::_thesis: verum end; end; registration let G be non-Dmulti _Graph; let X be set ; clusterG .set (WeightSelector,X) -> non-Dmulti ; coherence G .set (WeightSelector,X) is non-Dmulti proof G .set (WeightSelector,X) == G by Lm3; hence G .set (WeightSelector,X) is non-Dmulti by GLIB_000:89; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> non-Dmulti ; coherence G .set (ELabelSelector,X) is non-Dmulti proof G .set (ELabelSelector,X) == G by Lm3; hence G .set (ELabelSelector,X) is non-Dmulti by GLIB_000:89; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> non-Dmulti ; coherence G .set (VLabelSelector,X) is non-Dmulti proof G .set (VLabelSelector,X) == G by Lm3; hence G .set (VLabelSelector,X) is non-Dmulti by GLIB_000:89; ::_thesis: verum end; end; registration let G be connected _Graph; let X be set ; clusterG .set (WeightSelector,X) -> connected ; coherence G .set (WeightSelector,X) is connected proof G .set (WeightSelector,X) == G by Lm3; hence G .set (WeightSelector,X) is connected by GLIB_002:8; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> connected ; coherence G .set (ELabelSelector,X) is connected proof G .set (ELabelSelector,X) == G by Lm3; hence G .set (ELabelSelector,X) is connected by GLIB_002:8; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> connected ; coherence G .set (VLabelSelector,X) is connected proof G .set (VLabelSelector,X) == G by Lm3; hence G .set (VLabelSelector,X) is connected by GLIB_002:8; ::_thesis: verum end; end; registration let G be acyclic _Graph; let X be set ; clusterG .set (WeightSelector,X) -> acyclic ; coherence G .set (WeightSelector,X) is acyclic proof G .set (WeightSelector,X) == G by Lm3; hence G .set (WeightSelector,X) is acyclic by GLIB_002:44; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> acyclic ; coherence G .set (ELabelSelector,X) is acyclic proof G .set (ELabelSelector,X) == G by Lm3; hence G .set (ELabelSelector,X) is acyclic by GLIB_002:44; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> acyclic ; coherence G .set (VLabelSelector,X) is acyclic proof G .set (VLabelSelector,X) == G by Lm3; hence G .set (VLabelSelector,X) is acyclic by GLIB_002:44; ::_thesis: verum end; end; registration let G be WGraph; let X be set ; clusterG .set (ELabelSelector,X) -> [Weighted] ; coherence G .set (ELabelSelector,X) is [Weighted] proof set G1 = G .set (ELabelSelector,X); ( dom G c= dom (G .set (ELabelSelector,X)) & WeightSelector in dom G ) by Def4, FUNCT_4:10; hence WeightSelector in dom (G .set (ELabelSelector,X)) ; :: according to GLIB_003:def_4 ::_thesis: (G .set (ELabelSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (ELabelSelector,X)) G == G .set (ELabelSelector,X) by Lm3; then A1: the_Edges_of (G .set (ELabelSelector,X)) = the_Edges_of G by GLIB_000:def_34; (G .set (ELabelSelector,X)) . WeightSelector = the_Weight_of G by GLIB_000:9; hence (G .set (ELabelSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (ELabelSelector,X)) by A1; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> [Weighted] ; coherence G .set (VLabelSelector,X) is [Weighted] proof set G1 = G .set (VLabelSelector,X); ( dom G c= dom (G .set (VLabelSelector,X)) & WeightSelector in dom G ) by Def4, FUNCT_4:10; hence WeightSelector in dom (G .set (VLabelSelector,X)) ; :: according to GLIB_003:def_4 ::_thesis: (G .set (VLabelSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (VLabelSelector,X)) G == G .set (VLabelSelector,X) by Lm3; then A2: the_Edges_of (G .set (VLabelSelector,X)) = the_Edges_of G by GLIB_000:def_34; (G .set (VLabelSelector,X)) . WeightSelector = the_Weight_of G by GLIB_000:9; hence (G .set (VLabelSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (VLabelSelector,X)) by A2; ::_thesis: verum end; end; registration let G be _Graph; let X be ManySortedSet of the_Edges_of G; clusterG .set (WeightSelector,X) -> [Weighted] ; coherence G .set (WeightSelector,X) is [Weighted] proof set G1 = G .set (WeightSelector,X); ( dom (G .set (WeightSelector,X)) = (dom G) \/ {WeightSelector} & WeightSelector in {WeightSelector} ) by GLIB_000:7, TARSKI:def_1; hence WeightSelector in dom (G .set (WeightSelector,X)) by XBOOLE_0:def_3; :: according to GLIB_003:def_4 ::_thesis: (G .set (WeightSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (WeightSelector,X)) G == G .set (WeightSelector,X) by Lm3; then the_Edges_of G = the_Edges_of (G .set (WeightSelector,X)) by GLIB_000:def_34; hence (G .set (WeightSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (WeightSelector,X)) by GLIB_000:8; ::_thesis: verum end; end; registration let G be _Graph; let WL be non empty set ; let W be Function of (the_Edges_of G),WL; clusterG .set (WeightSelector,W) -> [Weighted] ; coherence G .set (WeightSelector,W) is [Weighted] ; end; registration let G be EGraph; let X be set ; clusterG .set (WeightSelector,X) -> [ELabeled] ; coherence G .set (WeightSelector,X) is [ELabeled] proof set G1 = G .set (WeightSelector,X); ( dom G c= dom (G .set (WeightSelector,X)) & ELabelSelector in dom G ) by Def5, FUNCT_4:10; hence ELabelSelector in dom (G .set (WeightSelector,X)) ; :: according to GLIB_003:def_5 ::_thesis: ex f being Function st ( (G .set (WeightSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (WeightSelector,X)) ) G == G .set (WeightSelector,X) by Lm3; then A1: the_Edges_of G = the_Edges_of (G .set (WeightSelector,X)) by GLIB_000:def_34; ( (G .set (WeightSelector,X)) . ELabelSelector = the_ELabel_of G & dom (the_ELabel_of G) c= the_Edges_of G ) by Lm1, GLIB_000:9; hence ex f being Function st ( (G .set (WeightSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (WeightSelector,X)) ) by A1; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> [ELabeled] ; coherence G .set (VLabelSelector,X) is [ELabeled] proof set G1 = G .set (VLabelSelector,X); ( dom G c= dom (G .set (VLabelSelector,X)) & ELabelSelector in dom G ) by Def5, FUNCT_4:10; hence ELabelSelector in dom (G .set (VLabelSelector,X)) ; :: according to GLIB_003:def_5 ::_thesis: ex f being Function st ( (G .set (VLabelSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (VLabelSelector,X)) ) G == G .set (VLabelSelector,X) by Lm3; then A2: the_Edges_of G = the_Edges_of (G .set (VLabelSelector,X)) by GLIB_000:def_34; ( (G .set (VLabelSelector,X)) . ELabelSelector = the_ELabel_of G & dom (the_ELabel_of G) c= the_Edges_of G ) by Lm1, GLIB_000:9; hence ex f being Function st ( (G .set (VLabelSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (VLabelSelector,X)) ) by A2; ::_thesis: verum end; end; registration let G be _Graph; let Y be set ; let X be PartFunc of (the_Edges_of G),Y; clusterG .set (ELabelSelector,X) -> [ELabeled] ; coherence G .set (ELabelSelector,X) is [ELabeled] proof set G1 = G .set (ELabelSelector,X); ( dom (G .set (ELabelSelector,X)) = (dom G) \/ {ELabelSelector} & ELabelSelector in {ELabelSelector} ) by GLIB_000:7, TARSKI:def_1; hence ELabelSelector in dom (G .set (ELabelSelector,X)) by XBOOLE_0:def_3; :: according to GLIB_003:def_5 ::_thesis: ex f being Function st ( (G .set (ELabelSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (ELabelSelector,X)) ) G == G .set (ELabelSelector,X) by Lm3; then A1: the_Edges_of G = the_Edges_of (G .set (ELabelSelector,X)) by GLIB_000:def_34; dom X c= the_Edges_of G ; hence ex f being Function st ( (G .set (ELabelSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (ELabelSelector,X)) ) by A1, GLIB_000:8; ::_thesis: verum end; end; registration let G be _Graph; let X be ManySortedSet of the_Edges_of G; clusterG .set (ELabelSelector,X) -> [ELabeled] ; coherence G .set (ELabelSelector,X) is [ELabeled] proof set G1 = G .set (ELabelSelector,X); ( dom (G .set (ELabelSelector,X)) = (dom G) \/ {ELabelSelector} & ELabelSelector in {ELabelSelector} ) by GLIB_000:7, TARSKI:def_1; hence ELabelSelector in dom (G .set (ELabelSelector,X)) by XBOOLE_0:def_3; :: according to GLIB_003:def_5 ::_thesis: ex f being Function st ( (G .set (ELabelSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (ELabelSelector,X)) ) G == G .set (ELabelSelector,X) by Lm3; then A1: the_Edges_of G = the_Edges_of (G .set (ELabelSelector,X)) by GLIB_000:def_34; dom X = the_Edges_of G by PARTFUN1:def_2; hence ex f being Function st ( (G .set (ELabelSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (ELabelSelector,X)) ) by A1, GLIB_000:8; ::_thesis: verum end; end; registration let G be VGraph; let X be set ; clusterG .set (WeightSelector,X) -> [VLabeled] ; coherence G .set (WeightSelector,X) is [VLabeled] proof set G1 = G .set (WeightSelector,X); ( dom G c= dom (G .set (WeightSelector,X)) & VLabelSelector in dom G ) by Def6, FUNCT_4:10; hence VLabelSelector in dom (G .set (WeightSelector,X)) ; :: according to GLIB_003:def_6 ::_thesis: ex f being Function st ( (G .set (WeightSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (WeightSelector,X)) ) G == G .set (WeightSelector,X) by Lm3; then A1: the_Vertices_of G = the_Vertices_of (G .set (WeightSelector,X)) by GLIB_000:def_34; ( (G .set (WeightSelector,X)) . VLabelSelector = the_VLabel_of G & dom (the_VLabel_of G) c= the_Vertices_of G ) by Lm2, GLIB_000:9; hence ex f being Function st ( (G .set (WeightSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (WeightSelector,X)) ) by A1; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> [VLabeled] ; coherence G .set (ELabelSelector,X) is [VLabeled] proof set G1 = G .set (ELabelSelector,X); ( dom G c= dom (G .set (ELabelSelector,X)) & VLabelSelector in dom G ) by Def6, FUNCT_4:10; hence VLabelSelector in dom (G .set (ELabelSelector,X)) ; :: according to GLIB_003:def_6 ::_thesis: ex f being Function st ( (G .set (ELabelSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (ELabelSelector,X)) ) G == G .set (ELabelSelector,X) by Lm3; then A2: the_Vertices_of G = the_Vertices_of (G .set (ELabelSelector,X)) by GLIB_000:def_34; ( (G .set (ELabelSelector,X)) . VLabelSelector = the_VLabel_of G & dom (the_VLabel_of G) c= the_Vertices_of G ) by Lm2, GLIB_000:9; hence ex f being Function st ( (G .set (ELabelSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (ELabelSelector,X)) ) by A2; ::_thesis: verum end; end; registration let G be _Graph; let Y be set ; let X be PartFunc of (the_Vertices_of G),Y; clusterG .set (VLabelSelector,X) -> [VLabeled] ; coherence G .set (VLabelSelector,X) is [VLabeled] proof set G1 = G .set (VLabelSelector,X); ( dom (G .set (VLabelSelector,X)) = (dom G) \/ {VLabelSelector} & VLabelSelector in {VLabelSelector} ) by GLIB_000:7, TARSKI:def_1; hence VLabelSelector in dom (G .set (VLabelSelector,X)) by XBOOLE_0:def_3; :: according to GLIB_003:def_6 ::_thesis: ex f being Function st ( (G .set (VLabelSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (VLabelSelector,X)) ) G == G .set (VLabelSelector,X) by Lm3; then A1: the_Vertices_of G = the_Vertices_of (G .set (VLabelSelector,X)) by GLIB_000:def_34; dom X c= the_Vertices_of G ; hence ex f being Function st ( (G .set (VLabelSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (VLabelSelector,X)) ) by A1, GLIB_000:8; ::_thesis: verum end; end; registration let G be _Graph; let X be ManySortedSet of the_Vertices_of G; clusterG .set (VLabelSelector,X) -> [VLabeled] ; coherence G .set (VLabelSelector,X) is [VLabeled] proof set G1 = G .set (VLabelSelector,X); ( dom (G .set (VLabelSelector,X)) = (dom G) \/ {VLabelSelector} & VLabelSelector in {VLabelSelector} ) by GLIB_000:7, TARSKI:def_1; hence VLabelSelector in dom (G .set (VLabelSelector,X)) by XBOOLE_0:def_3; :: according to GLIB_003:def_6 ::_thesis: ex f being Function st ( (G .set (VLabelSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (VLabelSelector,X)) ) G == G .set (VLabelSelector,X) by Lm3; then A1: the_Vertices_of G = the_Vertices_of (G .set (VLabelSelector,X)) by GLIB_000:def_34; dom X = the_Vertices_of G by PARTFUN1:def_2; hence ex f being Function st ( (G .set (VLabelSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (VLabelSelector,X)) ) by A1, GLIB_000:8; ::_thesis: verum end; end; registration let G be _Graph; clusterG .set (ELabelSelector,{}) -> [ELabeled] ; coherence G .set (ELabelSelector,{}) is [ELabeled] proof reconsider X = {} as PartFunc of (the_Edges_of G),{} by RELSET_1:12; G .set (ELabelSelector,X) is [ELabeled] ; hence G .set (ELabelSelector,{}) is [ELabeled] ; ::_thesis: verum end; clusterG .set (VLabelSelector,{}) -> [VLabeled] ; coherence G .set (VLabelSelector,{}) is [VLabeled] proof reconsider X = {} as PartFunc of (the_Vertices_of G),{} by RELSET_1:12; G .set (VLabelSelector,X) is [VLabeled] ; hence G .set (VLabelSelector,{}) is [VLabeled] ; ::_thesis: verum end; end; registration let G be _Graph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] for Subgraph of G; existence ex b1 being Subgraph of G st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) proof set W = the ManySortedSet of the_Edges_of G; set G2 = G .set (WeightSelector, the ManySortedSet of the_Edges_of G); set E = the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL; set G3 = (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL); set V = the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL; set G4 = ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL); ( G == G .set (WeightSelector, the ManySortedSet of the_Edges_of G) & G .set (WeightSelector, the ManySortedSet of the_Edges_of G) == (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL) ) by Lm3; then A1: G == (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL) by GLIB_000:85; (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL) == ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL) by Lm3; then G == ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL) by A1, GLIB_000:85; then ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL) is Subgraph of G by GLIB_000:87; hence ex b1 being Subgraph of G st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) ; ::_thesis: verum end; end; definition let G be WGraph; let G2 be [Weighted] Subgraph of G; attrG2 is weight-inheriting means :Def10: :: GLIB_003:def 10 the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2); end; :: deftheorem Def10 defines weight-inheriting GLIB_003:def_10_:_ for G being WGraph for G2 being [Weighted] Subgraph of G holds ( G2 is weight-inheriting iff the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2) ); definition let G be EGraph; let G2 be [ELabeled] Subgraph of G; attrG2 is elabel-inheriting means :Def11: :: GLIB_003:def 11 the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2); end; :: deftheorem Def11 defines elabel-inheriting GLIB_003:def_11_:_ for G being EGraph for G2 being [ELabeled] Subgraph of G holds ( G2 is elabel-inheriting iff the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2) ); definition let G be VGraph; let G2 be [VLabeled] Subgraph of G; attrG2 is vlabel-inheriting means :Def12: :: GLIB_003:def 12 the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2); end; :: deftheorem Def12 defines vlabel-inheriting GLIB_003:def_12_:_ for G being VGraph for G2 being [VLabeled] Subgraph of G holds ( G2 is vlabel-inheriting iff the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2) ); registration let G be WGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] weight-inheriting for Subgraph of G; existence ex b1 being [Weighted] Subgraph of G st b1 is weight-inheriting proof reconsider GG = G as [Weighted] Subgraph of G by GLIB_000:40; take GG ; ::_thesis: GG is weight-inheriting the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) ; hence GG is weight-inheriting by Def10; ::_thesis: verum end; end; registration let G be EGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] elabel-inheriting for Subgraph of G; existence ex b1 being [ELabeled] Subgraph of G st b1 is elabel-inheriting proof reconsider GG = G as [ELabeled] Subgraph of G by GLIB_000:40; take GG ; ::_thesis: GG is elabel-inheriting dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then the_ELabel_of GG = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:68; hence GG is elabel-inheriting by Def11; ::_thesis: verum end; end; registration let G be VGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [VLabeled] vlabel-inheriting for Subgraph of G; existence ex b1 being [VLabeled] Subgraph of G st b1 is vlabel-inheriting proof reconsider GG = G as [VLabeled] Subgraph of G by GLIB_000:40; take GG ; ::_thesis: GG is vlabel-inheriting dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then the_VLabel_of GG = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; end; registration let G be WEGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] weight-inheriting elabel-inheriting for Subgraph of G; existence ex b1 being [Weighted] [ELabeled] Subgraph of G st ( b1 is weight-inheriting & b1 is elabel-inheriting ) proof reconsider GG = G as [Weighted] [ELabeled] Subgraph of G by GLIB_000:40; take GG ; ::_thesis: ( GG is weight-inheriting & GG is elabel-inheriting ) the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) ; hence GG is weight-inheriting by Def10; ::_thesis: GG is elabel-inheriting dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then the_ELabel_of GG = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:68; hence GG is elabel-inheriting by Def11; ::_thesis: verum end; end; registration let G be WVGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [VLabeled] weight-inheriting vlabel-inheriting for Subgraph of G; existence ex b1 being [Weighted] [VLabeled] Subgraph of G st ( b1 is weight-inheriting & b1 is vlabel-inheriting ) proof reconsider GG = G as [Weighted] [VLabeled] Subgraph of G by GLIB_000:40; take GG ; ::_thesis: ( GG is weight-inheriting & GG is vlabel-inheriting ) the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) ; hence GG is weight-inheriting by Def10; ::_thesis: GG is vlabel-inheriting dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then the_VLabel_of GG = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; end; registration let G be EVGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting for Subgraph of G; existence ex b1 being [ELabeled] [VLabeled] Subgraph of G st ( b1 is elabel-inheriting & b1 is vlabel-inheriting ) proof reconsider GG = G as [ELabeled] [VLabeled] Subgraph of G by GLIB_000:40; take GG ; ::_thesis: ( GG is elabel-inheriting & GG is vlabel-inheriting ) dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then the_ELabel_of GG = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:68; hence GG is elabel-inheriting by Def11; ::_thesis: GG is vlabel-inheriting dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then the_VLabel_of GG = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; end; registration let G be WEVGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting for Subgraph of G; existence ex b1 being [Weighted] [ELabeled] [VLabeled] Subgraph of G st ( b1 is weight-inheriting & b1 is elabel-inheriting & b1 is vlabel-inheriting ) proof reconsider GG = G as [Weighted] [ELabeled] [VLabeled] Subgraph of G by GLIB_000:40; take GG ; ::_thesis: ( GG is weight-inheriting & GG is elabel-inheriting & GG is vlabel-inheriting ) the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) ; hence GG is weight-inheriting by Def10; ::_thesis: ( GG is elabel-inheriting & GG is vlabel-inheriting ) dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then the_ELabel_of GG = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:68; hence GG is elabel-inheriting by Def11; ::_thesis: GG is vlabel-inheriting dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then the_VLabel_of GG = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; end; definition let G be WGraph; mode WSubgraph of G is [Weighted] weight-inheriting Subgraph of G; end; definition let G be EGraph; mode ESubgraph of G is [ELabeled] elabel-inheriting Subgraph of G; end; definition let G be VGraph; mode VSubgraph of G is [VLabeled] vlabel-inheriting Subgraph of G; end; definition let G be WEGraph; mode WESubgraph of G is [Weighted] [ELabeled] weight-inheriting elabel-inheriting Subgraph of G; end; definition let G be WVGraph; mode WVSubgraph of G is [Weighted] [VLabeled] weight-inheriting vlabel-inheriting Subgraph of G; end; definition let G be EVGraph; mode EVSubgraph of G is [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting Subgraph of G; end; definition let G be WEVGraph; mode WEVSubgraph of G is [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting Subgraph of G; end; registration let G be _Graph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] for inducedSubgraph of G,V,E; existence ex b1 being inducedSubgraph of G,V,E st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) proof now__::_thesis:_ex_b1_being_inducedSubgraph_of_G,V,E_st_ (_b1_is_[Weighted]_&_b1_is_[ELabeled]_&_b1_is_[VLabeled]_) percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: ex b1 being inducedSubgraph of G,V,E st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) set X = the inducedSubgraph of G,V,E; set W = the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E; set G2 = the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E); set EL = the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL; set G3 = ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL); set VL = the PartFunc of (the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),REAL; set G4 = (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),REAL); ( the inducedSubgraph of G,V,E == the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E) & the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E) == ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL) ) by Lm3; then A2: the inducedSubgraph of G,V,E == ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL) by GLIB_000:85; ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL) == (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),REAL) by Lm3; then A3: the inducedSubgraph of G,V,E == (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),REAL) by A2, GLIB_000:85; then (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),REAL) is Subgraph of the inducedSubgraph of G,V,E by GLIB_000:87; then reconsider G4 = (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),REAL) as Subgraph of G by GLIB_000:43; the_Edges_of the inducedSubgraph of G,V,E = E by A1, GLIB_000:def_37; then A4: the_Edges_of G4 = E by A3, GLIB_000:def_34; the_Vertices_of the inducedSubgraph of G,V,E = V by A1, GLIB_000:def_37; then the_Vertices_of G4 = V by A3, GLIB_000:def_34; then G4 is inducedSubgraph of G,V,E by A1, A4, GLIB_000:def_37; hence ex b1 being inducedSubgraph of G,V,E st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) ; ::_thesis: verum end; supposeA5: ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: ex b1 being inducedSubgraph of G,V,E st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) set W = the ManySortedSet of the_Edges_of G; set G2 = G .set (WeightSelector, the ManySortedSet of the_Edges_of G); set EL = the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL; set G3 = (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL); set VL = the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL; set G4 = ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL); ( G == G .set (WeightSelector, the ManySortedSet of the_Edges_of G) & G .set (WeightSelector, the ManySortedSet of the_Edges_of G) == (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL) ) by Lm3; then A6: G == (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL) by GLIB_000:85; (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL) == ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL) by Lm3; then A7: G == ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL) by A6, GLIB_000:85; then reconsider G4 = ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),REAL) as Subgraph of G by GLIB_000:87; G4 is inducedSubgraph of G,V,E by A5, A7, GLIB_000:def_37; hence ex b1 being inducedSubgraph of G,V,E st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) ; ::_thesis: verum end; end; end; hence ex b1 being inducedSubgraph of G,V,E st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) ; ::_thesis: verum end; end; registration let G be WGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] weight-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [Weighted] inducedSubgraph of G,V,E st b1 is weight-inheriting proof now__::_thesis:_ex_GG_being_[Weighted]_inducedSubgraph_of_G,V,E_st_GG_is_weight-inheriting percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: ex GG being [Weighted] inducedSubgraph of G,V,E st GG is weight-inheriting set X = the [Weighted] inducedSubgraph of G,V,E; set W = (the_Weight_of G) | (the_Edges_of the [Weighted] inducedSubgraph of G,V,E); dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def_2; then dom ((the_Weight_of G) | (the_Edges_of the [Weighted] inducedSubgraph of G,V,E)) = the_Edges_of the [Weighted] inducedSubgraph of G,V,E by RELAT_1:62; then reconsider W = (the_Weight_of G) | (the_Edges_of the [Weighted] inducedSubgraph of G,V,E) as ManySortedSet of the_Edges_of the [Weighted] inducedSubgraph of G,V,E by PARTFUN1:def_2; set GG = the [Weighted] inducedSubgraph of G,V,E .set (WeightSelector,W); A2: the [Weighted] inducedSubgraph of G,V,E .set (WeightSelector,W) == the [Weighted] inducedSubgraph of G,V,E by Lm3; then the [Weighted] inducedSubgraph of G,V,E .set (WeightSelector,W) is Subgraph of the [Weighted] inducedSubgraph of G,V,E by GLIB_000:87; then reconsider GG = the [Weighted] inducedSubgraph of G,V,E .set (WeightSelector,W) as Subgraph of G by GLIB_000:43; A3: the_Vertices_of GG = the_Vertices_of the [Weighted] inducedSubgraph of G,V,E by A2, GLIB_000:def_34 .= V by A1, GLIB_000:def_37 ; the_Edges_of GG = the_Edges_of the [Weighted] inducedSubgraph of G,V,E by A2, GLIB_000:def_34 .= E by A1, GLIB_000:def_37 ; then reconsider GG = GG as [Weighted] inducedSubgraph of G,V,E by A1, A3, GLIB_000:def_37; take GG = GG; ::_thesis: GG is weight-inheriting the_Weight_of GG = W by GLIB_000:8 .= (the_Weight_of G) | (the_Edges_of GG) by A2, GLIB_000:def_34 ; hence GG is weight-inheriting by Def10; ::_thesis: verum end; supposeA4: ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: ex GG being [Weighted] inducedSubgraph of G,V,E st GG is weight-inheriting reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG = GG as [Weighted] inducedSubgraph of G,V,E by A4, GLIB_000:def_37; take GG = GG; ::_thesis: GG is weight-inheriting the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) ; hence GG is weight-inheriting by Def10; ::_thesis: verum end; end; end; hence ex b1 being [Weighted] inducedSubgraph of G,V,E st b1 is weight-inheriting ; ::_thesis: verum end; end; registration let G be EGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] elabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [ELabeled] inducedSubgraph of G,V,E st b1 is elabel-inheriting proof now__::_thesis:_ex_GG_being_[ELabeled]_inducedSubgraph_of_G,V,E_st_GG_is_elabel-inheriting percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: ex GG being [ELabeled] inducedSubgraph of G,V,E st GG is elabel-inheriting set X = the [ELabeled] inducedSubgraph of G,V,E; set EL = (the_ELabel_of G) | (the_Edges_of the [ELabeled] inducedSubgraph of G,V,E); reconsider EL9 = (the_ELabel_of G) | (the_Edges_of the [ELabeled] inducedSubgraph of G,V,E) as PartFunc of (dom ((the_ELabel_of G) | (the_Edges_of the [ELabeled] inducedSubgraph of G,V,E))),(rng ((the_ELabel_of G) | (the_Edges_of the [ELabeled] inducedSubgraph of G,V,E))) by RELSET_1:4; reconsider EL9 = EL9 as PartFunc of (the_Edges_of the [ELabeled] inducedSubgraph of G,V,E),(rng ((the_ELabel_of G) | (the_Edges_of the [ELabeled] inducedSubgraph of G,V,E))) by RELAT_1:58, RELSET_1:5; set GG = the [ELabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9); A2: the [ELabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9) == the [ELabeled] inducedSubgraph of G,V,E by Lm3; then the [ELabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9) is Subgraph of the [ELabeled] inducedSubgraph of G,V,E by GLIB_000:87; then reconsider GG = the [ELabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9) as Subgraph of G by GLIB_000:43; A3: the_Vertices_of GG = the_Vertices_of the [ELabeled] inducedSubgraph of G,V,E by A2, GLIB_000:def_34 .= V by A1, GLIB_000:def_37 ; the_Edges_of GG = the_Edges_of the [ELabeled] inducedSubgraph of G,V,E by A2, GLIB_000:def_34 .= E by A1, GLIB_000:def_37 ; then reconsider GG = GG as [ELabeled] inducedSubgraph of G,V,E by A1, A3, GLIB_000:def_37; take GG = GG; ::_thesis: GG is elabel-inheriting the_ELabel_of GG = (the_ELabel_of G) | (the_Edges_of the [ELabeled] inducedSubgraph of G,V,E) by GLIB_000:8 .= (the_ELabel_of G) | (the_Edges_of GG) by A2, GLIB_000:def_34 ; hence GG is elabel-inheriting by Def11; ::_thesis: verum end; supposeA4: ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: ex GG being [ELabeled] inducedSubgraph of G,V,E st GG is elabel-inheriting reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG = GG as [ELabeled] inducedSubgraph of G,V,E by A4, GLIB_000:def_37; take GG = GG; ::_thesis: GG is elabel-inheriting dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then the_ELabel_of G = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:68; hence GG is elabel-inheriting by Def11; ::_thesis: verum end; end; end; hence ex b1 being [ELabeled] inducedSubgraph of G,V,E st b1 is elabel-inheriting ; ::_thesis: verum end; end; registration let G be VGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [VLabeled] vlabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [VLabeled] inducedSubgraph of G,V,E st b1 is vlabel-inheriting proof now__::_thesis:_ex_GG_being_[VLabeled]_inducedSubgraph_of_G,V,E_st_GG_is_vlabel-inheriting percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: ex GG being [VLabeled] inducedSubgraph of G,V,E st GG is vlabel-inheriting set X = the [VLabeled] inducedSubgraph of G,V,E; set VL = (the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E); reconsider VL9 = (the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E) as PartFunc of (dom ((the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E))),(rng ((the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E))) by RELSET_1:4; reconsider VL9 = VL9 as PartFunc of (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E),(rng ((the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E))) by RELAT_1:58, RELSET_1:5; set GG = the [VLabeled] inducedSubgraph of G,V,E .set (VLabelSelector,VL9); A2: the [VLabeled] inducedSubgraph of G,V,E .set (VLabelSelector,VL9) == the [VLabeled] inducedSubgraph of G,V,E by Lm3; then the [VLabeled] inducedSubgraph of G,V,E .set (VLabelSelector,VL9) is Subgraph of the [VLabeled] inducedSubgraph of G,V,E by GLIB_000:87; then reconsider GG = the [VLabeled] inducedSubgraph of G,V,E .set (VLabelSelector,VL9) as Subgraph of G by GLIB_000:43; A3: the_Vertices_of GG = the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E by A2, GLIB_000:def_34 .= V by A1, GLIB_000:def_37 ; the_Edges_of GG = the_Edges_of the [VLabeled] inducedSubgraph of G,V,E by A2, GLIB_000:def_34 .= E by A1, GLIB_000:def_37 ; then reconsider GG = GG as [VLabeled] inducedSubgraph of G,V,E by A1, A3, GLIB_000:def_37; take GG = GG; ::_thesis: GG is vlabel-inheriting the_VLabel_of GG = (the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E) by GLIB_000:8 .= (the_VLabel_of G) | (the_Vertices_of GG) by A2, GLIB_000:def_34 ; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; supposeA4: ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: ex GG being [VLabeled] inducedSubgraph of G,V,E st GG is vlabel-inheriting reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG = GG as [VLabeled] inducedSubgraph of G,V,E by A4, GLIB_000:def_37; take GG = GG; ::_thesis: GG is vlabel-inheriting dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then the_VLabel_of G = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; end; end; hence ex b1 being [VLabeled] inducedSubgraph of G,V,E st b1 is vlabel-inheriting ; ::_thesis: verum end; end; registration let G be WEGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] weight-inheriting elabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [Weighted] [ELabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is elabel-inheriting ) proof now__::_thesis:_ex_G2_being_[Weighted]_[ELabeled]_inducedSubgraph_of_G,V,E_st_ (_G2_is_weight-inheriting_&_G2_is_elabel-inheriting_) percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: ex G2 being [Weighted] [ELabeled] inducedSubgraph of G,V,E st ( G2 is weight-inheriting & G2 is elabel-inheriting ) set X = the [Weighted] [ELabeled] inducedSubgraph of G,V,E; set W = (the_Weight_of G) | (the_Edges_of the [Weighted] [ELabeled] inducedSubgraph of G,V,E); dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def_2; then dom ((the_Weight_of G) | (the_Edges_of the [Weighted] [ELabeled] inducedSubgraph of G,V,E)) = the_Edges_of the [Weighted] [ELabeled] inducedSubgraph of G,V,E by RELAT_1:62; then reconsider W = (the_Weight_of G) | (the_Edges_of the [Weighted] [ELabeled] inducedSubgraph of G,V,E) as ManySortedSet of the_Edges_of the [Weighted] [ELabeled] inducedSubgraph of G,V,E by PARTFUN1:def_2; set G1 = the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W); set EL = (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))); reconsider EL9 = (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))) as PartFunc of (dom ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))),(rng ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))) by RELSET_1:4; reconsider EL9 = EL9 as PartFunc of (the_Edges_of ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))),(rng ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))) by RELAT_1:58, RELSET_1:5; set G2 = ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9); A2: ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) == the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by Lm3; the [Weighted] [ELabeled] inducedSubgraph of G,V,E == the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by Lm3; then A3: ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) == the [Weighted] [ELabeled] inducedSubgraph of G,V,E by A2, GLIB_000:85; then ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) is Subgraph of the [Weighted] [ELabeled] inducedSubgraph of G,V,E by GLIB_000:87; then reconsider G2 = ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) as Subgraph of G by GLIB_000:43; A4: the_Vertices_of G2 = the_Vertices_of the [Weighted] [ELabeled] inducedSubgraph of G,V,E by A3, GLIB_000:def_34 .= V by A1, GLIB_000:def_37 ; the_Edges_of G2 = the_Edges_of the [Weighted] [ELabeled] inducedSubgraph of G,V,E by A3, GLIB_000:def_34 .= E by A1, GLIB_000:def_37 ; then reconsider G2 = G2 as [Weighted] [ELabeled] inducedSubgraph of G,V,E by A1, A4, GLIB_000:def_37; take G2 = G2; ::_thesis: ( G2 is weight-inheriting & G2 is elabel-inheriting ) the_Weight_of G2 = ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) . WeightSelector by GLIB_000:9 .= W by GLIB_000:8 .= (the_Weight_of G) | (the_Edges_of G2) by A3, GLIB_000:def_34 ; hence G2 is weight-inheriting by Def10; ::_thesis: G2 is elabel-inheriting the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))) by GLIB_000:8 .= (the_ELabel_of G) | (the_Edges_of G2) by A2, GLIB_000:def_34 ; hence G2 is elabel-inheriting by Def11; ::_thesis: verum end; supposeA5: ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: ex GG being [Weighted] [ELabeled] inducedSubgraph of G,V,E st ( GG is weight-inheriting & GG is elabel-inheriting ) reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG = GG as [Weighted] [ELabeled] inducedSubgraph of G,V,E by A5, GLIB_000:def_37; take GG = GG; ::_thesis: ( GG is weight-inheriting & GG is elabel-inheriting ) the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) ; hence GG is weight-inheriting by Def10; ::_thesis: GG is elabel-inheriting dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then the_ELabel_of G = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:68; hence GG is elabel-inheriting by Def11; ::_thesis: verum end; end; end; hence ex b1 being [Weighted] [ELabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is elabel-inheriting ) ; ::_thesis: verum end; end; registration let G be WVGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [VLabeled] weight-inheriting vlabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [Weighted] [VLabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is vlabel-inheriting ) proof now__::_thesis:_ex_G2_being_[Weighted]_[VLabeled]_inducedSubgraph_of_G,V,E_st_ (_G2_is_weight-inheriting_&_G2_is_vlabel-inheriting_) percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: ex G2 being [Weighted] [VLabeled] inducedSubgraph of G,V,E st ( G2 is weight-inheriting & G2 is vlabel-inheriting ) set X = the [Weighted] [VLabeled] inducedSubgraph of G,V,E; set W = (the_Weight_of G) | (the_Edges_of the [Weighted] [VLabeled] inducedSubgraph of G,V,E); dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def_2; then dom ((the_Weight_of G) | (the_Edges_of the [Weighted] [VLabeled] inducedSubgraph of G,V,E)) = the_Edges_of the [Weighted] [VLabeled] inducedSubgraph of G,V,E by RELAT_1:62; then reconsider W = (the_Weight_of G) | (the_Edges_of the [Weighted] [VLabeled] inducedSubgraph of G,V,E) as ManySortedSet of the_Edges_of the [Weighted] [VLabeled] inducedSubgraph of G,V,E by PARTFUN1:def_2; set G1 = the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W); set VL = (the_VLabel_of G) | (the_Vertices_of ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))); reconsider VL9 = (the_VLabel_of G) | (the_Vertices_of ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))) as PartFunc of (dom ((the_VLabel_of G) | (the_Vertices_of ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))),(rng ((the_VLabel_of G) | (the_Vertices_of ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))) by RELSET_1:4; reconsider VL9 = VL9 as PartFunc of (the_Vertices_of ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))),(rng ((the_VLabel_of G) | (the_Vertices_of ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))) by RELAT_1:58, RELSET_1:5; set G2 = ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (VLabelSelector,VL9); A2: ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (VLabelSelector,VL9) == the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by Lm3; the [Weighted] [VLabeled] inducedSubgraph of G,V,E == the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by Lm3; then A3: ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (VLabelSelector,VL9) == the [Weighted] [VLabeled] inducedSubgraph of G,V,E by A2, GLIB_000:85; then ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (VLabelSelector,VL9) is Subgraph of the [Weighted] [VLabeled] inducedSubgraph of G,V,E by GLIB_000:87; then reconsider G2 = ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (VLabelSelector,VL9) as Subgraph of G by GLIB_000:43; A4: the_Vertices_of G2 = the_Vertices_of the [Weighted] [VLabeled] inducedSubgraph of G,V,E by A3, GLIB_000:def_34 .= V by A1, GLIB_000:def_37 ; the_Edges_of G2 = the_Edges_of the [Weighted] [VLabeled] inducedSubgraph of G,V,E by A3, GLIB_000:def_34 .= E by A1, GLIB_000:def_37 ; then reconsider G2 = G2 as [Weighted] [VLabeled] inducedSubgraph of G,V,E by A1, A4, GLIB_000:def_37; take G2 = G2; ::_thesis: ( G2 is weight-inheriting & G2 is vlabel-inheriting ) the_Weight_of G2 = ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) . WeightSelector by GLIB_000:9 .= W by GLIB_000:8 .= (the_Weight_of G) | (the_Edges_of G2) by A3, GLIB_000:def_34 ; hence G2 is weight-inheriting by Def10; ::_thesis: G2 is vlabel-inheriting the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of ( the [Weighted] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))) by GLIB_000:8 .= (the_VLabel_of G) | (the_Vertices_of G2) by A2, GLIB_000:def_34 ; hence G2 is vlabel-inheriting by Def12; ::_thesis: verum end; supposeA5: ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: ex GG being [Weighted] [VLabeled] inducedSubgraph of G,V,E st ( GG is weight-inheriting & GG is vlabel-inheriting ) reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG = GG as [Weighted] [VLabeled] inducedSubgraph of G,V,E by A5, GLIB_000:def_37; take GG = GG; ::_thesis: ( GG is weight-inheriting & GG is vlabel-inheriting ) the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) ; hence GG is weight-inheriting by Def10; ::_thesis: GG is vlabel-inheriting dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then the_VLabel_of G = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; end; end; hence ex b1 being [Weighted] [VLabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is vlabel-inheriting ) ; ::_thesis: verum end; end; registration let G be EVGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( b1 is elabel-inheriting & b1 is vlabel-inheriting ) proof now__::_thesis:_ex_G2_being_[ELabeled]_[VLabeled]_inducedSubgraph_of_G,V,E_st_ (_G2_is_elabel-inheriting_&_G2_is_vlabel-inheriting_) percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: ex G2 being [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( G2 is elabel-inheriting & G2 is vlabel-inheriting ) set X = the [ELabeled] [VLabeled] inducedSubgraph of G,V,E; set EL = (the_ELabel_of G) | (the_Edges_of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E); reconsider EL9 = (the_ELabel_of G) | (the_Edges_of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E) as PartFunc of (dom ((the_ELabel_of G) | (the_Edges_of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E))),(rng ((the_ELabel_of G) | (the_Edges_of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E))) by RELSET_1:4; reconsider EL9 = EL9 as PartFunc of (the_Edges_of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E),(rng ((the_ELabel_of G) | (the_Edges_of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E))) by RELAT_1:58, RELSET_1:5; set G1 = the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9); set VL = (the_VLabel_of G) | (the_Vertices_of ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9))); reconsider VL9 = (the_VLabel_of G) | (the_Vertices_of ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9))) as PartFunc of (dom ((the_VLabel_of G) | (the_Vertices_of ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9))))),(rng ((the_VLabel_of G) | (the_Vertices_of ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9))))) by RELSET_1:4; reconsider VL9 = VL9 as PartFunc of (the_Vertices_of ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9))),(rng ((the_VLabel_of G) | (the_Vertices_of ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9))))) by RELAT_1:58, RELSET_1:5; set G2 = ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9); A2: ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) == the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9) by Lm3; the [ELabeled] [VLabeled] inducedSubgraph of G,V,E == the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9) by Lm3; then A3: ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) == the [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A2, GLIB_000:85; then ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) is Subgraph of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E by GLIB_000:87; then reconsider G2 = ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) as Subgraph of G by GLIB_000:43; A4: the_Vertices_of G2 = the_Vertices_of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A3, GLIB_000:def_34 .= V by A1, GLIB_000:def_37 ; the_Edges_of G2 = the_Edges_of the [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A3, GLIB_000:def_34 .= E by A1, GLIB_000:def_37 ; then reconsider G2 = G2 as [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A1, A4, GLIB_000:def_37; take G2 = G2; ::_thesis: ( G2 is elabel-inheriting & G2 is vlabel-inheriting ) the_ELabel_of G2 = ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9)) . ELabelSelector by GLIB_000:9 .= EL9 by GLIB_000:8 .= (the_ELabel_of G) | (the_Edges_of G2) by A3, GLIB_000:def_34 ; hence G2 is elabel-inheriting by Def11; ::_thesis: G2 is vlabel-inheriting the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of ( the [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (ELabelSelector,EL9))) by GLIB_000:8 .= (the_VLabel_of G) | (the_Vertices_of G2) by A2, GLIB_000:def_34 ; hence G2 is vlabel-inheriting by Def12; ::_thesis: verum end; supposeA5: ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: ex GG being [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( GG is elabel-inheriting & GG is vlabel-inheriting ) reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG = GG as [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A5, GLIB_000:def_37; take GG = GG; ::_thesis: ( GG is elabel-inheriting & GG is vlabel-inheriting ) dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then the_ELabel_of G = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:68; hence GG is elabel-inheriting by Def11; ::_thesis: GG is vlabel-inheriting dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then the_VLabel_of G = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; end; end; hence ex b1 being [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( b1 is elabel-inheriting & b1 is vlabel-inheriting ) ; ::_thesis: verum end; end; registration let G be WEVGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is elabel-inheriting & b1 is vlabel-inheriting ) proof now__::_thesis:_ex_G3_being_[Weighted]_[ELabeled]_[VLabeled]_inducedSubgraph_of_G,V,E_st_ (_G3_is_weight-inheriting_&_G3_is_elabel-inheriting_&_G3_is_vlabel-inheriting_) percases ( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) or not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; supposeA1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; ::_thesis: ex G3 being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( G3 is weight-inheriting & G3 is elabel-inheriting & G3 is vlabel-inheriting ) set X = the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E; set W = (the_Weight_of G) | (the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E); dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def_2; then dom ((the_Weight_of G) | (the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E)) = the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by RELAT_1:62; then reconsider W = (the_Weight_of G) | (the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E) as ManySortedSet of the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by PARTFUN1:def_2; set G1 = the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W); set EL = (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))); reconsider EL9 = (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))) as PartFunc of (dom ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))),(rng ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))) by RELSET_1:4; reconsider EL9 = EL9 as PartFunc of (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))),(rng ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))) by RELAT_1:58, RELSET_1:5; set G2 = ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9); set VL = (the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))); reconsider VL9 = (the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))) as PartFunc of (dom ((the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))))),(rng ((the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))))) by RELSET_1:4; reconsider VL9 = VL9 as PartFunc of (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))),(rng ((the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))))) by RELAT_1:58, RELSET_1:5; set G3 = (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9); A2: ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by Lm3; A3: (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) == ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) by Lm3; the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by Lm3; then ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A2, GLIB_000:85; then A4: (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A3, GLIB_000:85; then (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) is Subgraph of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by GLIB_000:87; then reconsider G3 = (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) as Subgraph of G by GLIB_000:43; A5: the_Vertices_of G3 = the_Vertices_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A4, GLIB_000:def_34 .= V by A1, GLIB_000:def_37 ; the_Edges_of G3 = the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A4, GLIB_000:def_34 .= E by A1, GLIB_000:def_37 ; then reconsider G3 = G3 as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A1, A5, GLIB_000:def_37; A6: G3 == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by A2, A3, GLIB_000:85; take G3 = G3; ::_thesis: ( G3 is weight-inheriting & G3 is elabel-inheriting & G3 is vlabel-inheriting ) the_Weight_of G3 = (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) . WeightSelector by GLIB_000:9 .= ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) . WeightSelector by GLIB_000:9 .= W by GLIB_000:8 .= (the_Weight_of G) | (the_Edges_of G3) by A4, GLIB_000:def_34 ; hence G3 is weight-inheriting by Def10; ::_thesis: ( G3 is elabel-inheriting & G3 is vlabel-inheriting ) the_ELabel_of G3 = (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) . ELabelSelector by GLIB_000:9 .= (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))) by GLIB_000:8 .= (the_ELabel_of G) | (the_Edges_of G3) by A6, GLIB_000:def_34 ; hence G3 is elabel-inheriting by Def11; ::_thesis: G3 is vlabel-inheriting the_VLabel_of G3 = (the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))) by GLIB_000:8 .= (the_VLabel_of G) | (the_Vertices_of G3) by A3, GLIB_000:def_34 ; hence G3 is vlabel-inheriting by Def12; ::_thesis: verum end; supposeA7: ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) ; ::_thesis: ex GG being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( GG is weight-inheriting & GG is elabel-inheriting & GG is vlabel-inheriting ) reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG = GG as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A7, GLIB_000:def_37; take GG = GG; ::_thesis: ( GG is weight-inheriting & GG is elabel-inheriting & GG is vlabel-inheriting ) the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) ; hence GG is weight-inheriting by Def10; ::_thesis: ( GG is elabel-inheriting & GG is vlabel-inheriting ) dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then the_ELabel_of G = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:68; hence GG is elabel-inheriting by Def11; ::_thesis: GG is vlabel-inheriting dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then the_VLabel_of G = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68; hence GG is vlabel-inheriting by Def12; ::_thesis: verum end; end; end; hence ex b1 being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is elabel-inheriting & b1 is vlabel-inheriting ) ; ::_thesis: verum end; end; definition let G be WGraph; let V, E be set ; mode inducedWSubgraph of G,V,E is [Weighted] weight-inheriting inducedSubgraph of G,V,E; end; definition let G be EGraph; let V, E be set ; mode inducedESubgraph of G,V,E is [ELabeled] elabel-inheriting inducedSubgraph of G,V,E; end; definition let G be VGraph; let V, E be set ; mode inducedVSubgraph of G,V,E is [VLabeled] vlabel-inheriting inducedSubgraph of G,V,E; end; definition let G be WEGraph; let V, E be set ; mode inducedWESubgraph of G,V,E is [Weighted] [ELabeled] weight-inheriting elabel-inheriting inducedSubgraph of G,V,E; end; definition let G be WVGraph; let V, E be set ; mode inducedWVSubgraph of G,V,E is [Weighted] [VLabeled] weight-inheriting vlabel-inheriting inducedSubgraph of G,V,E; end; definition let G be EVGraph; let V, E be set ; mode inducedEVSubgraph of G,V,E is [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting inducedSubgraph of G,V,E; end; definition let G be WEVGraph; let V, E be set ; mode inducedWEVSubgraph of G,V,E is [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting inducedSubgraph of G,V,E; end; definition let G be WGraph; let V be set ; mode inducedWSubgraph of G,V is inducedWSubgraph of G,V,G .edgesBetween V; end; definition let G be EGraph; let V be set ; mode inducedESubgraph of G,V is inducedESubgraph of G,V,G .edgesBetween V; end; definition let G be VGraph; let V be set ; mode inducedVSubgraph of G,V is inducedVSubgraph of G,V,G .edgesBetween V; end; definition let G be WEGraph; let V be set ; mode inducedWESubgraph of G,V is inducedWESubgraph of G,V,G .edgesBetween V; end; definition let G be WVGraph; let V be set ; mode inducedWVSubgraph of G,V is inducedWVSubgraph of G,V,G .edgesBetween V; end; definition let G be EVGraph; let V be set ; mode inducedEVSubgraph of G,V is inducedEVSubgraph of G,V,G .edgesBetween V; end; definition let G be WEVGraph; let V be set ; mode inducedWEVSubgraph of G,V is inducedWEVSubgraph of G,V,G .edgesBetween V; end; definition let G be WGraph; attrG is real-weighted means :Def13: :: GLIB_003:def 13 the_Weight_of G is real-valued ; end; :: deftheorem Def13 defines real-weighted GLIB_003:def_13_:_ for G being WGraph holds ( G is real-weighted iff the_Weight_of G is real-valued ); definition let G be WGraph; attrG is nonnegative-weighted means :Def14: :: GLIB_003:def 14 rng (the_Weight_of G) c= Real>=0 ; end; :: deftheorem Def14 defines nonnegative-weighted GLIB_003:def_14_:_ for G being WGraph holds ( G is nonnegative-weighted iff rng (the_Weight_of G) c= Real>=0 ); registration cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] nonnegative-weighted -> real-weighted for set ; coherence for b1 being WGraph st b1 is nonnegative-weighted holds b1 is real-weighted proof let G be WGraph; ::_thesis: ( G is nonnegative-weighted implies G is real-weighted ) assume G is nonnegative-weighted ; ::_thesis: G is real-weighted then rng (the_Weight_of G) c= Real>=0 by Def14; then rng (the_Weight_of G) c= REAL by XBOOLE_1:1; then the_Weight_of G is real-valued by VALUED_0:def_3; hence G is real-weighted by Def13; ::_thesis: verum end; end; definition let G be EGraph; attrG is real-elabeled means :Def15: :: GLIB_003:def 15 the_ELabel_of G is real-valued ; end; :: deftheorem Def15 defines real-elabeled GLIB_003:def_15_:_ for G being EGraph holds ( G is real-elabeled iff the_ELabel_of G is real-valued ); definition let G be VGraph; attrG is real-vlabeled means :Def16: :: GLIB_003:def 16 the_VLabel_of G is real-valued ; end; :: deftheorem Def16 defines real-vlabeled GLIB_003:def_16_:_ for G being VGraph holds ( G is real-vlabeled iff the_VLabel_of G is real-valued ); definition let G be WEVGraph; attrG is real-WEV means :Def17: :: GLIB_003:def 17 ( G is real-weighted & G is real-elabeled & G is real-vlabeled ); end; :: deftheorem Def17 defines real-WEV GLIB_003:def_17_:_ for G being WEVGraph holds ( G is real-WEV iff ( G is real-weighted & G is real-elabeled & G is real-vlabeled ) ); registration cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] real-WEV -> real-weighted real-elabeled real-vlabeled for set ; coherence for b1 being WEVGraph st b1 is real-WEV holds ( b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled ) by Def17; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] real-weighted real-elabeled real-vlabeled -> real-WEV for set ; coherence for b1 being WEVGraph st b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled holds b1 is real-WEV by Def17; end; registration let G be _Graph; let X be Function of (the_Edges_of G),REAL; clusterG .set (WeightSelector,X) -> real-weighted ; coherence G .set (WeightSelector,X) is real-weighted proof set G2 = G .set (WeightSelector,X); the_Weight_of (G .set (WeightSelector,X)) = X by GLIB_000:8; hence G .set (WeightSelector,X) is real-weighted by Def13; ::_thesis: verum end; end; registration let G be _Graph; let X be PartFunc of (the_Edges_of G),REAL; clusterG .set (ELabelSelector,X) -> real-elabeled ; coherence G .set (ELabelSelector,X) is real-elabeled proof set G2 = G .set (ELabelSelector,X); the_ELabel_of (G .set (ELabelSelector,X)) = X by GLIB_000:8; hence G .set (ELabelSelector,X) is real-elabeled by Def15; ::_thesis: verum end; end; registration let G be _Graph; let X be real-valued ManySortedSet of the_Edges_of G; clusterG .set (ELabelSelector,X) -> real-elabeled ; coherence G .set (ELabelSelector,X) is real-elabeled proof set G2 = G .set (ELabelSelector,X); the_ELabel_of (G .set (ELabelSelector,X)) = X by GLIB_000:8; hence G .set (ELabelSelector,X) is real-elabeled by Def15; ::_thesis: verum end; end; registration let G be _Graph; let X be PartFunc of (the_Vertices_of G),REAL; clusterG .set (VLabelSelector,X) -> real-vlabeled ; coherence G .set (VLabelSelector,X) is real-vlabeled proof set G2 = G .set (VLabelSelector,X); the_VLabel_of (G .set (VLabelSelector,X)) = X by GLIB_000:8; hence G .set (VLabelSelector,X) is real-vlabeled by Def16; ::_thesis: verum end; end; registration let G be _Graph; let X be real-valued ManySortedSet of the_Vertices_of G; clusterG .set (VLabelSelector,X) -> real-vlabeled ; coherence G .set (VLabelSelector,X) is real-vlabeled proof set G2 = G .set (VLabelSelector,X); the_VLabel_of (G .set (VLabelSelector,X)) = X by GLIB_000:8; hence G .set (VLabelSelector,X) is real-vlabeled by Def16; ::_thesis: verum end; end; registration let G be _Graph; clusterG .set (ELabelSelector,{}) -> real-elabeled ; coherence G .set (ELabelSelector,{}) is real-elabeled proof reconsider X = {} as PartFunc of (the_Edges_of G),REAL by RELSET_1:12; G .set (ELabelSelector,X) is real-elabeled ; hence G .set (ELabelSelector,{}) is real-elabeled ; ::_thesis: verum end; clusterG .set (VLabelSelector,{}) -> real-vlabeled ; coherence G .set (VLabelSelector,{}) is real-vlabeled proof reconsider X = {} as PartFunc of (the_Vertices_of G),REAL by RELSET_1:12; G .set (VLabelSelector,X) is real-vlabeled ; hence G .set (VLabelSelector,{}) is real-vlabeled ; ::_thesis: verum end; end; registration let G be _Graph; let v be Vertex of G; let val be real number ; clusterG .set (VLabelSelector,(v .--> val)) -> [VLabeled] ; coherence G .set (VLabelSelector,(v .--> val)) is [VLabeled] proof reconsider X = v .--> val as PartFunc of {v},{val} ; dom (v .--> val) = {v} by FUNCOP_1:13; then reconsider X = X as PartFunc of (the_Vertices_of G),{val} by RELSET_1:5; rng (v .--> val) = {val} by FUNCOP_1:8; then reconsider X = X as PartFunc of (the_Vertices_of G),REAL by RELSET_1:6; G .set (VLabelSelector,X) is real-vlabeled ; hence G .set (VLabelSelector,(v .--> val)) is [VLabeled] ; ::_thesis: verum end; end; registration let G be _Graph; let v be Vertex of G; let val be real number ; clusterG .set (VLabelSelector,(v .--> val)) -> real-vlabeled ; coherence G .set (VLabelSelector,(v .--> val)) is real-vlabeled proof reconsider X = v .--> val as PartFunc of {v},{val} ; dom (v .--> val) = {v} by FUNCOP_1:13; then reconsider X = X as PartFunc of (the_Vertices_of G),{val} by RELSET_1:5; for x being set st x in {val} holds x in REAL by XREAL_0:def_1; then {val} c= REAL by TARSKI:def_3; then reconsider X = X as PartFunc of (the_Vertices_of G),REAL by RELSET_1:7; G .set (VLabelSelector,X) is real-vlabeled ; hence G .set (VLabelSelector,(v .--> val)) is real-vlabeled ; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like finite [Graph-like] finite trivial Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ; existence ex b1 being WEVGraph st ( b1 is finite & b1 is trivial & b1 is Tree-like & b1 is nonnegative-weighted & b1 is real-WEV ) proof set E = {} ; set V = {1}; reconsider S = {} as Function of {},{1} by RELSET_1:12; set G1 = createGraph ({1},{},S,S); set WL = the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL; set G2 = (createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL); set EL = the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL; set G3 = ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL); set VL = the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL; set G4 = (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL); take (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) ; ::_thesis: ( (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is finite & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is trivial & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is Tree-like & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is nonnegative-weighted & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-WEV ) thus ( (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is finite & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is trivial & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is Tree-like ) ; ::_thesis: ( (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is nonnegative-weighted & (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-WEV ) A1: the_Weight_of ((((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL)) = (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) . WeightSelector by GLIB_000:9 .= ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) . WeightSelector by GLIB_000:9 .= the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL by GLIB_000:8 ; the_Edges_of (createGraph ({1},{},S,S)) = {} by GLIB_000:6; then rng (the_Weight_of ((((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL))) = {} by A1; then rng (the_Weight_of ((((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL))) c= Real>=0 by XBOOLE_1:2; hence (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is nonnegative-weighted by Def14; ::_thesis: (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-WEV the_ELabel_of ((((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL)) = (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) . ELabelSelector by GLIB_000:9 .= the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL by GLIB_000:8 ; then A2: (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-elabeled by Def15; (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-weighted by A1, Def13; hence (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL)) .set (VLabelSelector, the PartFunc of (the_Vertices_of (((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL)) .set (ELabelSelector, the PartFunc of (the_Edges_of ((createGraph ({1},{},S,S)) .set (WeightSelector, the Function of (the_Edges_of (createGraph ({1},{},S,S))),REAL))),REAL))),REAL) is real-WEV by A2; ::_thesis: verum end; cluster Relation-like NAT -defined Function-like finite [Graph-like] finite non trivial Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ; existence ex b1 being WEVGraph st ( b1 is finite & not b1 is trivial & b1 is Tree-like & b1 is nonnegative-weighted & b1 is real-WEV ) proof set G1 = the finite non trivial Tree-like _Graph; set W = (the_Edges_of the finite non trivial Tree-like _Graph) --> 0; A3: dom ((the_Edges_of the finite non trivial Tree-like _Graph) --> 0) = the_Edges_of the finite non trivial Tree-like _Graph by FUNCOP_1:13; A4: rng ((the_Edges_of the finite non trivial Tree-like _Graph) --> 0) c= {0} by FUNCOP_1:13; then reconsider W = (the_Edges_of the finite non trivial Tree-like _Graph) --> 0 as Function of (the_Edges_of the finite non trivial Tree-like _Graph),REAL by A3, FUNCT_2:2; set G2 = the finite non trivial Tree-like _Graph .set (WeightSelector,W); reconsider EL = {} as PartFunc of (the_Edges_of ( the finite non trivial Tree-like _Graph .set (WeightSelector,W))),REAL by RELSET_1:12; set G3 = ( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL); reconsider VL = {} as PartFunc of (the_Vertices_of (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL))),REAL by RELSET_1:12; set G4 = (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL); take (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) ; ::_thesis: ( (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is finite & not (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is trivial & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is Tree-like & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is nonnegative-weighted & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV ) thus ( (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is finite & not (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is trivial & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is Tree-like ) ; ::_thesis: ( (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is nonnegative-weighted & (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV ) A5: the_Weight_of ((( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL)) = (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) . WeightSelector by GLIB_000:9 .= ( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) . WeightSelector by GLIB_000:9 .= W by GLIB_000:8 ; now__::_thesis:_for_x_being_set_st_x_in_{0}_holds_ x_in_Real>=0 let x be set ; ::_thesis: ( x in {0} implies x in Real>=0 ) assume x in {0} ; ::_thesis: x in Real>=0 then x = 0 by TARSKI:def_1; hence x in Real>=0 by GRAPH_5:def_12; ::_thesis: verum end; then {0} c= Real>=0 by TARSKI:def_3; then rng W c= Real>=0 by A4, XBOOLE_1:1; hence (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is nonnegative-weighted by A5, Def14; ::_thesis: (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV the_ELabel_of ((( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL)) = (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) . ELabelSelector by GLIB_000:9 .= EL by GLIB_000:8 ; then A6: (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-elabeled by Def15; (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-weighted by A5, Def13; hence (( the finite non trivial Tree-like _Graph .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (VLabelSelector,VL) is real-WEV by A6; ::_thesis: verum end; end; registration let G be finite WGraph; cluster the_Weight_of G -> finite ; coherence the_Weight_of G is finite proof A1: dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def_2; then rng (the_Weight_of G) is finite by FINSET_1:8; hence the_Weight_of G is finite by A1, ORDERS_1:87; ::_thesis: verum end; end; registration let G be finite EGraph; cluster the_ELabel_of G -> finite ; coherence the_ELabel_of G is finite proof A1: dom (the_ELabel_of G) c= the_Edges_of G by Lm1; then rng (the_ELabel_of G) is finite by FINSET_1:8; hence the_ELabel_of G is finite by A1, ORDERS_1:87; ::_thesis: verum end; end; registration let G be finite VGraph; cluster the_VLabel_of G -> finite ; coherence the_VLabel_of G is finite proof A1: dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; then rng (the_VLabel_of G) is finite by FINSET_1:8; hence the_VLabel_of G is finite by A1, ORDERS_1:87; ::_thesis: verum end; end; registration let G be real-weighted WGraph; cluster the_Weight_of G -> real-valued ; coherence the_Weight_of G is real-valued by Def13; end; registration let G be real-elabeled EGraph; cluster the_ELabel_of G -> real-valued ; coherence the_ELabel_of G is real-valued by Def15; end; registration let G be real-vlabeled VGraph; cluster the_VLabel_of G -> real-valued ; coherence the_VLabel_of G is real-valued by Def16; end; registration let G be real-weighted WGraph; let X be set ; clusterG .set (ELabelSelector,X) -> real-weighted ; coherence G .set (ELabelSelector,X) is real-weighted proof set G2 = G .set (ELabelSelector,X); the_Weight_of (G .set (ELabelSelector,X)) = the_Weight_of G by GLIB_000:9; hence G .set (ELabelSelector,X) is real-weighted by Def13; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> real-weighted ; coherence G .set (VLabelSelector,X) is real-weighted proof set G2 = G .set (VLabelSelector,X); the_Weight_of (G .set (VLabelSelector,X)) = the_Weight_of G by GLIB_000:9; hence G .set (VLabelSelector,X) is real-weighted by Def13; ::_thesis: verum end; end; registration let G be nonnegative-weighted WGraph; let X be set ; clusterG .set (ELabelSelector,X) -> nonnegative-weighted ; coherence G .set (ELabelSelector,X) is nonnegative-weighted proof set G2 = G .set (ELabelSelector,X); ( the_Weight_of (G .set (ELabelSelector,X)) = the_Weight_of G & rng (the_Weight_of G) c= Real>=0 ) by Def14, GLIB_000:9; hence G .set (ELabelSelector,X) is nonnegative-weighted by Def14; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> nonnegative-weighted ; coherence G .set (VLabelSelector,X) is nonnegative-weighted proof set G2 = G .set (VLabelSelector,X); ( the_Weight_of (G .set (VLabelSelector,X)) = the_Weight_of G & rng (the_Weight_of G) c= Real>=0 ) by Def14, GLIB_000:9; hence G .set (VLabelSelector,X) is nonnegative-weighted by Def14; ::_thesis: verum end; end; registration let G be real-elabeled EGraph; let X be set ; clusterG .set (WeightSelector,X) -> real-elabeled ; coherence G .set (WeightSelector,X) is real-elabeled proof set G2 = G .set (WeightSelector,X); the_ELabel_of (G .set (WeightSelector,X)) = the_ELabel_of G by GLIB_000:9; hence G .set (WeightSelector,X) is real-elabeled by Def15; ::_thesis: verum end; clusterG .set (VLabelSelector,X) -> real-elabeled ; coherence G .set (VLabelSelector,X) is real-elabeled proof set G2 = G .set (VLabelSelector,X); the_ELabel_of (G .set (VLabelSelector,X)) = the_ELabel_of G by GLIB_000:9; hence G .set (VLabelSelector,X) is real-elabeled by Def15; ::_thesis: verum end; end; registration let G be real-vlabeled VGraph; let X be set ; clusterG .set (WeightSelector,X) -> real-vlabeled ; coherence G .set (WeightSelector,X) is real-vlabeled proof set G2 = G .set (WeightSelector,X); the_VLabel_of (G .set (WeightSelector,X)) = the_VLabel_of G by GLIB_000:9; hence G .set (WeightSelector,X) is real-vlabeled by Def16; ::_thesis: verum end; clusterG .set (ELabelSelector,X) -> real-vlabeled ; coherence G .set (ELabelSelector,X) is real-vlabeled proof set G2 = G .set (ELabelSelector,X); the_VLabel_of (G .set (ELabelSelector,X)) = the_VLabel_of G by GLIB_000:9; hence G .set (ELabelSelector,X) is real-vlabeled by Def16; ::_thesis: verum end; end; definition let G be WGraph; let W be Walk of G; funcW .weightSeq() -> FinSequence means :Def18: :: GLIB_003:def 18 ( len it = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len it holds it . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ); existence ex b1 being FinSequence st ( len b1 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b1 holds b1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ) proof deffunc H1( Nat) -> set = (the_Weight_of G) . ((W .edgeSeq()) . $1); consider IT being FinSequence such that A1: ( len IT = len (W .edgeSeq()) & ( for k being Nat st k in dom IT holds IT . k = H1(k) ) ) from FINSEQ_1:sch_2(); take IT ; ::_thesis: ( len IT = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len IT holds IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ) thus len IT = len (W .edgeSeq()) by A1; ::_thesis: for n being Nat st 1 <= n & n <= len IT holds IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n) let n be Nat; ::_thesis: ( 1 <= n & n <= len IT implies IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) assume ( 1 <= n & n <= len IT ) ; ::_thesis: IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n) then n in dom IT by FINSEQ_3:25; hence IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n) by A1; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence st len b1 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b1 holds b1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) & len b2 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b2 holds b2 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) holds b1 = b2 proof let IT1, IT2 be FinSequence; ::_thesis: ( len IT1 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len IT1 holds IT1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) & len IT2 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len IT2 holds IT2 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) implies IT1 = IT2 ) assume that A2: len IT1 = len (W .edgeSeq()) and A3: for n being Nat st 1 <= n & n <= len IT1 holds IT1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) and A4: len IT2 = len (W .edgeSeq()) and A5: for n being Nat st 1 <= n & n <= len IT2 holds IT2 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ; ::_thesis: IT1 = IT2 now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_len_IT1_holds_ IT1_._n_=_IT2_._n let n be Nat; ::_thesis: ( 1 <= n & n <= len IT1 implies IT1 . n = IT2 . n ) assume A6: ( 1 <= n & n <= len IT1 ) ; ::_thesis: IT1 . n = IT2 . n hence IT1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) by A3 .= IT2 . n by A2, A4, A5, A6 ; ::_thesis: verum end; hence IT1 = IT2 by A2, A4, FINSEQ_1:14; ::_thesis: verum end; end; :: deftheorem Def18 defines .weightSeq() GLIB_003:def_18_:_ for G being WGraph for W being Walk of G for b3 being FinSequence holds ( b3 = W .weightSeq() iff ( len b3 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b3 holds b3 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ) ); definition let G be real-weighted WGraph; let W be Walk of G; :: original: .weightSeq() redefine funcW .weightSeq() -> FinSequence of REAL ; coherence W .weightSeq() is FinSequence of REAL proof now__::_thesis:_for_y_being_set_st_y_in_rng_(W_.weightSeq())_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng (W .weightSeq()) implies y in REAL ) assume y in rng (W .weightSeq()) ; ::_thesis: y in REAL then consider x being Nat such that A1: x in dom (W .weightSeq()) and A2: y = (W .weightSeq()) . x by FINSEQ_2:10; ( 1 <= x & x <= len (W .weightSeq()) ) by A1, FINSEQ_3:25; then y = (the_Weight_of G) . ((W .edgeSeq()) . x) by A2, Def18; hence y in REAL ; ::_thesis: verum end; then rng (W .weightSeq()) c= REAL by TARSKI:def_3; hence W .weightSeq() is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum end; end; definition let G be real-weighted WGraph; let W be Walk of G; funcW .cost() -> Real equals :: GLIB_003:def 19 Sum (W .weightSeq()); coherence Sum (W .weightSeq()) is Real ; end; :: deftheorem defines .cost() GLIB_003:def_19_:_ for G being real-weighted WGraph for W being Walk of G holds W .cost() = Sum (W .weightSeq()); Lm4: for x, y, X, Y being set for f being PartFunc of X,Y st x in X & y in Y holds f +* (x .--> y) is PartFunc of X,Y proof let x, y, X, Y be set ; ::_thesis: for f being PartFunc of X,Y st x in X & y in Y holds f +* (x .--> y) is PartFunc of X,Y let f be PartFunc of X,Y; ::_thesis: ( x in X & y in Y implies f +* (x .--> y) is PartFunc of X,Y ) assume that A1: x in X and A2: y in Y ; ::_thesis: f +* (x .--> y) is PartFunc of X,Y set F = f +* (x .--> y); A3: rng (f +* (x .--> y)) c= (rng f) \/ (rng (x .--> y)) by FUNCT_4:17; now__::_thesis:_for_z_being_set_st_z_in_rng_(f_+*_(x_.-->_y))_holds_ z_in_Y let z be set ; ::_thesis: ( z in rng (f +* (x .--> y)) implies z in Y ) assume A4: z in rng (f +* (x .--> y)) ; ::_thesis: z in Y now__::_thesis:_z_in_Y percases ( z in rng f or z in rng (x .--> y) ) by A3, A4, XBOOLE_0:def_3; suppose z in rng f ; ::_thesis: z in Y hence z in Y ; ::_thesis: verum end; suppose z in rng (x .--> y) ; ::_thesis: z in Y then z in {y} by FUNCOP_1:8; hence z in Y by A2, TARSKI:def_1; ::_thesis: verum end; end; end; hence z in Y ; ::_thesis: verum end; then rng (f +* (x .--> y)) c= Y by TARSKI:def_3; then reconsider F1 = f +* (x .--> y) as PartFunc of (dom (f +* (x .--> y))),Y by RELSET_1:4; now__::_thesis:_for_z_being_set_st_z_in_dom_F1_holds_ z_in_X let z be set ; ::_thesis: ( z in dom F1 implies z in X ) assume z in dom F1 ; ::_thesis: z in X then A5: z in (dom f) \/ (dom (x .--> y)) by FUNCT_4:def_1; now__::_thesis:_z_in_X percases ( z in dom f or z in dom (x .--> y) ) by A5, XBOOLE_0:def_3; suppose z in dom f ; ::_thesis: z in X hence z in X ; ::_thesis: verum end; suppose z in dom (x .--> y) ; ::_thesis: z in X then z in {x} ; hence z in X by A1, TARSKI:def_1; ::_thesis: verum end; end; end; hence z in X ; ::_thesis: verum end; then dom F1 c= X by TARSKI:def_3; hence f +* (x .--> y) is PartFunc of X,Y by RELSET_1:7; ::_thesis: verum end; definition let G be EGraph; funcG .labeledE() -> Subset of (the_Edges_of G) equals :: GLIB_003:def 20 dom (the_ELabel_of G); coherence dom (the_ELabel_of G) is Subset of (the_Edges_of G) by Lm1; end; :: deftheorem defines .labeledE() GLIB_003:def_20_:_ for G being EGraph holds G .labeledE() = dom (the_ELabel_of G); definition let G be EGraph; let e, x be set ; funcG .labelEdge (e,x) -> EGraph equals :Def21: :: GLIB_003:def 21 G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) if e in the_Edges_of G otherwise G; coherence ( ( e in the_Edges_of G implies G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) is EGraph ) & ( not e in the_Edges_of G implies G is EGraph ) ) proof set EL = (the_ELabel_of G) +* (e .--> x); set G2 = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))); G == G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Lm3; then A1: the_Edges_of G = the_Edges_of (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) by GLIB_000:def_34; hereby ::_thesis: ( not e in the_Edges_of G implies G is EGraph ) A2: dom ((the_ELabel_of G) +* (e .--> x)) = (dom (the_ELabel_of G)) \/ (dom (e .--> x)) by FUNCT_4:def_1 .= (dom (the_ELabel_of G)) \/ {e} by FUNCOP_1:13 ; assume A3: e in the_Edges_of G ; ::_thesis: G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) is EGraph now__::_thesis:_for_z_being_set_st_z_in_dom_((the_ELabel_of_G)_+*_(e_.-->_x))_holds_ z_in_the_Edges_of_G let z be set ; ::_thesis: ( z in dom ((the_ELabel_of G) +* (e .--> x)) implies z in the_Edges_of G ) assume A4: z in dom ((the_ELabel_of G) +* (e .--> x)) ; ::_thesis: z in the_Edges_of G now__::_thesis:_z_in_the_Edges_of_G percases ( z in dom (the_ELabel_of G) or z in {e} ) by A2, A4, XBOOLE_0:def_3; supposeA5: z in dom (the_ELabel_of G) ; ::_thesis: z in the_Edges_of G dom (the_ELabel_of G) c= the_Edges_of G by Lm1; hence z in the_Edges_of G by A5; ::_thesis: verum end; suppose z in {e} ; ::_thesis: z in the_Edges_of G hence z in the_Edges_of G by A3, TARSKI:def_1; ::_thesis: verum end; end; end; hence z in the_Edges_of G ; ::_thesis: verum end; then A6: dom ((the_ELabel_of G) +* (e .--> x)) c= the_Edges_of (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) by A1, TARSKI:def_3; A7: (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) . ELabelSelector = (the_ELabel_of G) +* (e .--> x) by GLIB_000:8; ( ELabelSelector in dom G & dom G c= dom (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) ) by Def5, FUNCT_4:10; hence G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) is EGraph by A6, A7, Def5; ::_thesis: verum end; thus ( not e in the_Edges_of G implies G is EGraph ) ; ::_thesis: verum end; consistency for b1 being EGraph holds verum ; end; :: deftheorem Def21 defines .labelEdge GLIB_003:def_21_:_ for G being EGraph for e, x being set holds ( ( e in the_Edges_of G implies G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) ) & ( not e in the_Edges_of G implies G .labelEdge (e,x) = G ) ); registration let G be finite EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> finite ; coherence G .labelEdge (e,x) is finite proof now__::_thesis:_G_.labelEdge_(e,x)_is_finite percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is finite then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is finite ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is finite hence G .labelEdge (e,x) is finite by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is finite ; ::_thesis: verum end; end; registration let G be loopless EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> loopless ; coherence G .labelEdge (e,x) is loopless proof now__::_thesis:_G_.labelEdge_(e,x)_is_loopless percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is loopless then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is loopless ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is loopless hence G .labelEdge (e,x) is loopless by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is loopless ; ::_thesis: verum end; end; registration let G be trivial EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> trivial ; coherence G .labelEdge (e,x) is trivial proof now__::_thesis:_G_.labelEdge_(e,x)_is_trivial percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is trivial then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is trivial ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is trivial hence G .labelEdge (e,x) is trivial by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is trivial ; ::_thesis: verum end; end; registration let G be non trivial EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> non trivial ; coherence not G .labelEdge (e,x) is trivial proof now__::_thesis:_not_G_.labelEdge_(e,x)_is_trivial percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: not G .labelEdge (e,x) is trivial then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence not G .labelEdge (e,x) is trivial ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: not G .labelEdge (e,x) is trivial hence not G .labelEdge (e,x) is trivial by Def21; ::_thesis: verum end; end; end; hence not G .labelEdge (e,x) is trivial ; ::_thesis: verum end; end; registration let G be non-multi EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> non-multi ; coherence G .labelEdge (e,x) is non-multi proof now__::_thesis:_G_.labelEdge_(e,x)_is_non-multi percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is non-multi then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is non-multi ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is non-multi hence G .labelEdge (e,x) is non-multi by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is non-multi ; ::_thesis: verum end; end; registration let G be non-Dmulti EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> non-Dmulti ; coherence G .labelEdge (e,x) is non-Dmulti proof now__::_thesis:_G_.labelEdge_(e,x)_is_non-Dmulti percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is non-Dmulti then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is non-Dmulti ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is non-Dmulti hence G .labelEdge (e,x) is non-Dmulti by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is non-Dmulti ; ::_thesis: verum end; end; registration let G be connected EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> connected ; coherence G .labelEdge (e,x) is connected proof now__::_thesis:_G_.labelEdge_(e,x)_is_connected percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is connected then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is connected ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is connected hence G .labelEdge (e,x) is connected by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is connected ; ::_thesis: verum end; end; registration let G be acyclic EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> acyclic ; coherence G .labelEdge (e,x) is acyclic proof now__::_thesis:_G_.labelEdge_(e,x)_is_acyclic percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is acyclic then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is acyclic ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is acyclic hence G .labelEdge (e,x) is acyclic by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is acyclic ; ::_thesis: verum end; end; registration let G be WEGraph; let e, x be set ; clusterG .labelEdge (e,x) -> [Weighted] ; coherence G .labelEdge (e,x) is [Weighted] proof now__::_thesis:_G_.labelEdge_(e,x)_is_[Weighted] percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is [Weighted] then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is [Weighted] ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is [Weighted] hence G .labelEdge (e,x) is [Weighted] by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is [Weighted] ; ::_thesis: verum end; end; registration let G be EVGraph; let e, x be set ; clusterG .labelEdge (e,x) -> [VLabeled] ; coherence G .labelEdge (e,x) is [VLabeled] proof now__::_thesis:_G_.labelEdge_(e,x)_is_[VLabeled] percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is [VLabeled] then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is [VLabeled] ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is [VLabeled] hence G .labelEdge (e,x) is [VLabeled] by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is [VLabeled] ; ::_thesis: verum end; end; registration let G be real-weighted WEGraph; let e, x be set ; clusterG .labelEdge (e,x) -> real-weighted ; coherence G .labelEdge (e,x) is real-weighted proof now__::_thesis:_G_.labelEdge_(e,x)_is_real-weighted percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is real-weighted then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is real-weighted ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is real-weighted hence G .labelEdge (e,x) is real-weighted by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is real-weighted ; ::_thesis: verum end; end; registration let G be nonnegative-weighted WEGraph; let e, x be set ; clusterG .labelEdge (e,x) -> nonnegative-weighted ; coherence G .labelEdge (e,x) is nonnegative-weighted proof now__::_thesis:_G_.labelEdge_(e,x)_is_nonnegative-weighted percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is nonnegative-weighted then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is nonnegative-weighted ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is nonnegative-weighted hence G .labelEdge (e,x) is nonnegative-weighted by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is nonnegative-weighted ; ::_thesis: verum end; end; registration let G be real-elabeled EGraph; let e be set ; let x be Real; clusterG .labelEdge (e,x) -> real-elabeled ; coherence G .labelEdge (e,x) is real-elabeled proof now__::_thesis:_G_.labelEdge_(e,x)_is_real-elabeled percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; supposeA1: e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is real-elabeled set EL = (the_ELabel_of G) +* (e .--> x); rng (the_ELabel_of G) c= REAL ; then the_ELabel_of G is PartFunc of (dom (the_ELabel_of G)),REAL by RELSET_1:4; then the_ELabel_of G is PartFunc of (the_Edges_of G),REAL by Lm1, RELSET_1:5; then reconsider EL = (the_ELabel_of G) +* (e .--> x) as PartFunc of (the_Edges_of G),REAL by A1, Lm4; G .labelEdge (e,x) = G .set (ELabelSelector,EL) by A1, Def21; hence G .labelEdge (e,x) is real-elabeled ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is real-elabeled hence G .labelEdge (e,x) is real-elabeled by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is real-elabeled ; ::_thesis: verum end; end; registration let G be real-vlabeled EVGraph; let e, x be set ; clusterG .labelEdge (e,x) -> real-vlabeled ; coherence G .labelEdge (e,x) is real-vlabeled proof now__::_thesis:_G_.labelEdge_(e,x)_is_real-vlabeled percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is real-vlabeled then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence G .labelEdge (e,x) is real-vlabeled ; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G .labelEdge (e,x) is real-vlabeled hence G .labelEdge (e,x) is real-vlabeled by Def21; ::_thesis: verum end; end; end; hence G .labelEdge (e,x) is real-vlabeled ; ::_thesis: verum end; end; definition let G be VGraph; let v, x be set ; funcG .labelVertex (v,x) -> VGraph equals :Def22: :: GLIB_003:def 22 G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) if v in the_Vertices_of G otherwise G; coherence ( ( v in the_Vertices_of G implies G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) is VGraph ) & ( not v in the_Vertices_of G implies G is VGraph ) ) proof set VL = (the_VLabel_of G) +* (v .--> x); set G2 = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))); hereby ::_thesis: ( not v in the_Vertices_of G implies G is VGraph ) A1: dom ((the_VLabel_of G) +* (v .--> x)) = (dom (the_VLabel_of G)) \/ (dom (v .--> x)) by FUNCT_4:def_1; assume A2: v in the_Vertices_of G ; ::_thesis: G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) is VGraph now__::_thesis:_for_y_being_set_st_y_in_dom_((the_VLabel_of_G)_+*_(v_.-->_x))_holds_ y_in_the_Vertices_of_G let y be set ; ::_thesis: ( y in dom ((the_VLabel_of G) +* (v .--> x)) implies y in the_Vertices_of G ) assume A3: y in dom ((the_VLabel_of G) +* (v .--> x)) ; ::_thesis: y in the_Vertices_of G now__::_thesis:_y_in_the_Vertices_of_G percases ( y in dom (the_VLabel_of G) or y in dom (v .--> x) ) by A1, A3, XBOOLE_0:def_3; supposeA4: y in dom (the_VLabel_of G) ; ::_thesis: y in the_Vertices_of G dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; hence y in the_Vertices_of G by A4; ::_thesis: verum end; suppose y in dom (v .--> x) ; ::_thesis: y in the_Vertices_of G then y in {v} ; hence y in the_Vertices_of G by A2, TARSKI:def_1; ::_thesis: verum end; end; end; hence y in the_Vertices_of G ; ::_thesis: verum end; then dom ((the_VLabel_of G) +* (v .--> x)) c= the_Vertices_of G by TARSKI:def_3; then reconsider V1 = (the_VLabel_of G) +* (v .--> x) as PartFunc of (the_Vertices_of G),(rng ((the_VLabel_of G) +* (v .--> x))) by RELSET_1:4; G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) = G .set (VLabelSelector,V1) ; hence G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) is VGraph ; ::_thesis: verum end; thus ( not v in the_Vertices_of G implies G is VGraph ) ; ::_thesis: verum end; consistency for b1 being VGraph holds verum ; end; :: deftheorem Def22 defines .labelVertex GLIB_003:def_22_:_ for G being VGraph for v, x being set holds ( ( v in the_Vertices_of G implies G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) ) & ( not v in the_Vertices_of G implies G .labelVertex (v,x) = G ) ); definition let G be VGraph; funcG .labeledV() -> Subset of (the_Vertices_of G) equals :: GLIB_003:def 23 dom (the_VLabel_of G); coherence dom (the_VLabel_of G) is Subset of (the_Vertices_of G) by Lm2; end; :: deftheorem defines .labeledV() GLIB_003:def_23_:_ for G being VGraph holds G .labeledV() = dom (the_VLabel_of G); registration let G be finite VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> finite ; coherence G .labelVertex (v,x) is finite proof now__::_thesis:_G_.labelVertex_(v,x)_is_finite percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is finite then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is finite ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is finite hence G .labelVertex (v,x) is finite by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is finite ; ::_thesis: verum end; end; registration let G be loopless VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> loopless ; coherence G .labelVertex (v,x) is loopless proof now__::_thesis:_G_.labelVertex_(v,x)_is_loopless percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is loopless then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is loopless ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is loopless hence G .labelVertex (v,x) is loopless by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is loopless ; ::_thesis: verum end; end; registration let G be trivial VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> trivial ; coherence G .labelVertex (v,x) is trivial proof now__::_thesis:_G_.labelVertex_(v,x)_is_trivial percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is trivial then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is trivial ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is trivial hence G .labelVertex (v,x) is trivial by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is trivial ; ::_thesis: verum end; end; registration let G be non trivial VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> non trivial ; coherence not G .labelVertex (v,x) is trivial proof now__::_thesis:_not_G_.labelVertex_(v,x)_is_trivial percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: not G .labelVertex (v,x) is trivial then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence not G .labelVertex (v,x) is trivial ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: not G .labelVertex (v,x) is trivial hence not G .labelVertex (v,x) is trivial by Def22; ::_thesis: verum end; end; end; hence not G .labelVertex (v,x) is trivial ; ::_thesis: verum end; end; registration let G be non-multi VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> non-multi ; coherence G .labelVertex (v,x) is non-multi proof now__::_thesis:_G_.labelVertex_(v,x)_is_non-multi percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is non-multi then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is non-multi ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is non-multi hence G .labelVertex (v,x) is non-multi by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is non-multi ; ::_thesis: verum end; end; registration let G be non-Dmulti VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> non-Dmulti ; coherence G .labelVertex (v,x) is non-Dmulti proof now__::_thesis:_G_.labelVertex_(v,x)_is_non-Dmulti percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is non-Dmulti then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is non-Dmulti ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is non-Dmulti hence G .labelVertex (v,x) is non-Dmulti by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is non-Dmulti ; ::_thesis: verum end; end; registration let G be connected VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> connected ; coherence G .labelVertex (v,x) is connected proof now__::_thesis:_G_.labelVertex_(v,x)_is_connected percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is connected then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is connected ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is connected hence G .labelVertex (v,x) is connected by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is connected ; ::_thesis: verum end; end; registration let G be acyclic VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> acyclic ; coherence G .labelVertex (v,x) is acyclic proof now__::_thesis:_G_.labelVertex_(v,x)_is_acyclic percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is acyclic then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is acyclic ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is acyclic hence G .labelVertex (v,x) is acyclic by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is acyclic ; ::_thesis: verum end; end; registration let G be WVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> [Weighted] ; coherence G .labelVertex (v,x) is [Weighted] proof now__::_thesis:_G_.labelVertex_(v,x)_is_[Weighted] percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is [Weighted] then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is [Weighted] ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is [Weighted] hence G .labelVertex (v,x) is [Weighted] by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is [Weighted] ; ::_thesis: verum end; end; registration let G be EVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> [ELabeled] ; coherence G .labelVertex (v,x) is [ELabeled] proof now__::_thesis:_G_.labelVertex_(v,x)_is_[ELabeled] percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is [ELabeled] then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is [ELabeled] ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is [ELabeled] hence G .labelVertex (v,x) is [ELabeled] by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is [ELabeled] ; ::_thesis: verum end; end; registration let G be real-weighted WVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> real-weighted ; coherence G .labelVertex (v,x) is real-weighted proof now__::_thesis:_G_.labelVertex_(v,x)_is_real-weighted percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is real-weighted then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is real-weighted ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is real-weighted hence G .labelVertex (v,x) is real-weighted by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is real-weighted ; ::_thesis: verum end; end; registration let G be nonnegative-weighted WVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> nonnegative-weighted ; coherence G .labelVertex (v,x) is nonnegative-weighted proof now__::_thesis:_G_.labelVertex_(v,x)_is_nonnegative-weighted percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is nonnegative-weighted then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is nonnegative-weighted ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is nonnegative-weighted hence G .labelVertex (v,x) is nonnegative-weighted by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is nonnegative-weighted ; ::_thesis: verum end; end; registration let G be real-elabeled EVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> real-elabeled ; coherence G .labelVertex (v,x) is real-elabeled proof now__::_thesis:_G_.labelVertex_(v,x)_is_real-elabeled percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; suppose v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is real-elabeled then G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) by Def22; hence G .labelVertex (v,x) is real-elabeled ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is real-elabeled hence G .labelVertex (v,x) is real-elabeled by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is real-elabeled ; ::_thesis: verum end; end; registration let G be real-vlabeled VGraph; let v be set ; let x be Real; clusterG .labelVertex (v,x) -> real-vlabeled ; coherence G .labelVertex (v,x) is real-vlabeled proof now__::_thesis:_G_.labelVertex_(v,x)_is_real-vlabeled percases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ; supposeA1: v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is real-vlabeled set EL = (the_VLabel_of G) +* (v .--> x); rng (the_VLabel_of G) c= REAL ; then the_VLabel_of G is PartFunc of (dom (the_VLabel_of G)),REAL by RELSET_1:4; then the_VLabel_of G is PartFunc of (the_Vertices_of G),REAL by Lm2, RELSET_1:5; then reconsider EL = (the_VLabel_of G) +* (v .--> x) as PartFunc of (the_Vertices_of G),REAL by A1, Lm4; G .labelVertex (v,x) = G .set (VLabelSelector,EL) by A1, Def22; hence G .labelVertex (v,x) is real-vlabeled ; ::_thesis: verum end; suppose not v in the_Vertices_of G ; ::_thesis: G .labelVertex (v,x) is real-vlabeled hence G .labelVertex (v,x) is real-vlabeled by Def22; ::_thesis: verum end; end; end; hence G .labelVertex (v,x) is real-vlabeled ; ::_thesis: verum end; end; registration let G be real-weighted WGraph; cluster [Weighted] weight-inheriting -> real-weighted for Subgraph of G; coherence for b1 being WSubgraph of G holds b1 is real-weighted proof let G2 be WSubgraph of G; ::_thesis: G2 is real-weighted set W2 = (the_Weight_of G) | (the_Edges_of G2); the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2) by Def10; hence G2 is real-weighted by Def13; ::_thesis: verum end; end; registration let G be nonnegative-weighted WGraph; cluster [Weighted] weight-inheriting -> nonnegative-weighted for Subgraph of G; coherence for b1 being WSubgraph of G holds b1 is nonnegative-weighted proof let G2 be WSubgraph of G; ::_thesis: G2 is nonnegative-weighted now__::_thesis:_for_x_being_set_st_x_in_rng_(the_Weight_of_G2)_holds_ x_in_Real>=0 let x be set ; ::_thesis: ( x in rng (the_Weight_of G2) implies x in Real>=0 ) A1: rng (the_Weight_of G) c= Real>=0 by Def14; assume x in rng (the_Weight_of G2) ; ::_thesis: x in Real>=0 then A2: x in rng ((the_Weight_of G) | (the_Edges_of G2)) by Def10; rng ((the_Weight_of G) | (the_Edges_of G2)) c= rng (the_Weight_of G) by RELAT_1:70; then x in rng (the_Weight_of G) by A2; hence x in Real>=0 by A1; ::_thesis: verum end; hence rng (the_Weight_of G2) c= Real>=0 by TARSKI:def_3; :: according to GLIB_003:def_14 ::_thesis: verum end; end; registration let G be real-elabeled EGraph; cluster [ELabeled] elabel-inheriting -> real-elabeled for Subgraph of G; coherence for b1 being ESubgraph of G holds b1 is real-elabeled proof let G2 be ESubgraph of G; ::_thesis: G2 is real-elabeled the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2) by Def11; hence G2 is real-elabeled by Def15; ::_thesis: verum end; end; registration let G be real-vlabeled VGraph; cluster [VLabeled] vlabel-inheriting -> real-vlabeled for Subgraph of G; coherence for b1 being VSubgraph of G holds b1 is real-vlabeled proof let G2 be VSubgraph of G; ::_thesis: G2 is real-vlabeled the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2) by Def12; hence G2 is real-vlabeled by Def16; ::_thesis: verum end; end; definition let GSq be GraphSeq; attrGSq is [Weighted] means :Def24: :: GLIB_003:def 24 for x being Nat holds GSq . x is [Weighted] ; attrGSq is [ELabeled] means :Def25: :: GLIB_003:def 25 for x being Nat holds GSq . x is [ELabeled] ; attrGSq is [VLabeled] means :Def26: :: GLIB_003:def 26 for x being Nat holds GSq . x is [VLabeled] ; end; :: deftheorem Def24 defines [Weighted] GLIB_003:def_24_:_ for GSq being GraphSeq holds ( GSq is [Weighted] iff for x being Nat holds GSq . x is [Weighted] ); :: deftheorem Def25 defines [ELabeled] GLIB_003:def_25_:_ for GSq being GraphSeq holds ( GSq is [ELabeled] iff for x being Nat holds GSq . x is [ELabeled] ); :: deftheorem Def26 defines [VLabeled] GLIB_003:def_26_:_ for GSq being GraphSeq holds ( GSq is [VLabeled] iff for x being Nat holds GSq . x is [VLabeled] ); registration cluster Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] for set ; existence ex b1 being GraphSeq st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) proof set G = the finite loopless trivial non-multi simple nonnegative-weighted real-WEV WEVGraph; set F = NAT --> the finite loopless trivial non-multi simple nonnegative-weighted real-WEV WEVGraph; A1: dom (NAT --> the finite loopless trivial non-multi simple nonnegative-weighted real-WEV WEVGraph) = NAT by FUNCOP_1:13; reconsider F = NAT --> the finite loopless trivial non-multi simple nonnegative-weighted real-WEV WEVGraph as ManySortedSet of NAT ; now__::_thesis:_for_x_being_Nat_holds_F_._x_is__Graph let x be Nat; ::_thesis: F . x is _Graph x in NAT by ORDINAL1:def_12; then F . x in rng F by A1, FUNCT_1:3; then F . x in { the finite loopless trivial non-multi simple nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8; hence F . x is _Graph by TARSKI:def_1; ::_thesis: verum end; then reconsider F = F as GraphSeq by GLIB_000:def_53; take F ; ::_thesis: ( F is [Weighted] & F is [ELabeled] & F is [VLabeled] ) now__::_thesis:_for_x_being_Nat_holds_ (_F_._x_is_[Weighted]_&_F_._x_is_[ELabeled]_&_F_._x_is_[VLabeled]_) let x be Nat; ::_thesis: ( F . x is [Weighted] & F . x is [ELabeled] & F . x is [VLabeled] ) x in NAT by ORDINAL1:def_12; then F . x in rng F by A1, FUNCT_1:3; then F . x in { the finite loopless trivial non-multi simple nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8; hence ( F . x is [Weighted] & F . x is [ELabeled] & F . x is [VLabeled] ) by TARSKI:def_1; ::_thesis: verum end; hence ( F is [Weighted] & F is [ELabeled] & F is [VLabeled] ) by Def24, Def25, Def26; ::_thesis: verum end; end; definition mode WGraphSeq is [Weighted] GraphSeq; mode EGraphSeq is [ELabeled] GraphSeq; mode VGraphSeq is [VLabeled] GraphSeq; mode WEGraphSeq is [Weighted] [ELabeled] GraphSeq; mode WVGraphSeq is [Weighted] [VLabeled] GraphSeq; mode EVGraphSeq is [ELabeled] [VLabeled] GraphSeq; mode WEVGraphSeq is [Weighted] [ELabeled] [VLabeled] GraphSeq; end; registration let GSq be WGraphSeq; let x be Nat; clusterGSq . x -> [Weighted] for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is [Weighted] by Def24; end; registration let GSq be EGraphSeq; let x be Nat; clusterGSq . x -> [ELabeled] for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is [ELabeled] by Def25; end; registration let GSq be VGraphSeq; let x be Nat; clusterGSq . x -> [VLabeled] for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is [VLabeled] by Def26; end; definition let GSq be WGraphSeq; attrGSq is real-weighted means :Def27: :: GLIB_003:def 27 for x being Nat holds GSq . x is real-weighted ; attrGSq is nonnegative-weighted means :Def28: :: GLIB_003:def 28 for x being Nat holds GSq . x is nonnegative-weighted ; end; :: deftheorem Def27 defines real-weighted GLIB_003:def_27_:_ for GSq being WGraphSeq holds ( GSq is real-weighted iff for x being Nat holds GSq . x is real-weighted ); :: deftheorem Def28 defines nonnegative-weighted GLIB_003:def_28_:_ for GSq being WGraphSeq holds ( GSq is nonnegative-weighted iff for x being Nat holds GSq . x is nonnegative-weighted ); definition let GSq be EGraphSeq; attrGSq is real-elabeled means :Def29: :: GLIB_003:def 29 for x being Nat holds GSq . x is real-elabeled ; end; :: deftheorem Def29 defines real-elabeled GLIB_003:def_29_:_ for GSq being EGraphSeq holds ( GSq is real-elabeled iff for x being Nat holds GSq . x is real-elabeled ); definition let GSq be VGraphSeq; attrGSq is real-vlabeled means :Def30: :: GLIB_003:def 30 for x being Nat holds GSq . x is real-vlabeled ; end; :: deftheorem Def30 defines real-vlabeled GLIB_003:def_30_:_ for GSq being VGraphSeq holds ( GSq is real-vlabeled iff for x being Nat holds GSq . x is real-vlabeled ); definition let GSq be WEVGraphSeq; attrGSq is real-WEV means :Def31: :: GLIB_003:def 31 for x being Nat holds GSq . x is real-WEV ; end; :: deftheorem Def31 defines real-WEV GLIB_003:def_31_:_ for GSq being WEVGraphSeq holds ( GSq is real-WEV iff for x being Nat holds GSq . x is real-WEV ); registration cluster Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] real-WEV -> real-weighted real-elabeled real-vlabeled for set ; coherence for b1 being WEVGraphSeq st b1 is real-WEV holds ( b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled ) proof let GSq be [Weighted] [ELabeled] [VLabeled] GraphSeq; ::_thesis: ( GSq is real-WEV implies ( GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled ) ) assume A1: for x being Nat holds GSq . x is real-WEV ; :: according to GLIB_003:def_31 ::_thesis: ( GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled ) now__::_thesis:_for_x_being_Nat_holds_GSq_._x_is_real-weighted let x be Nat; ::_thesis: GSq . x is real-weighted reconsider G = GSq . x as real-WEV WEVGraph by A1; G is real-WEV ; hence GSq . x is real-weighted ; ::_thesis: verum end; hence GSq is real-weighted by Def27; ::_thesis: ( GSq is real-elabeled & GSq is real-vlabeled ) now__::_thesis:_for_x_being_Nat_holds_GSq_._x_is_real-elabeled let x be Nat; ::_thesis: GSq . x is real-elabeled reconsider G = GSq . x as real-WEV WEVGraph by A1; G is real-WEV ; hence GSq . x is real-elabeled ; ::_thesis: verum end; hence GSq is real-elabeled by Def29; ::_thesis: GSq is real-vlabeled now__::_thesis:_for_x_being_Nat_holds_GSq_._x_is_real-vlabeled let x be Nat; ::_thesis: GSq . x is real-vlabeled reconsider G = GSq . x as real-WEV WEVGraph by A1; G is real-WEV ; hence GSq . x is real-vlabeled ; ::_thesis: verum end; hence GSq is real-vlabeled by Def30; ::_thesis: verum end; cluster Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] real-weighted real-elabeled real-vlabeled -> real-WEV for set ; coherence for b1 being WEVGraphSeq st b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled holds b1 is real-WEV proof let GSq be [Weighted] [ELabeled] [VLabeled] GraphSeq; ::_thesis: ( GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled implies GSq is real-WEV ) assume A2: ( GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled ) ; ::_thesis: GSq is real-WEV let x be Nat; :: according to GLIB_003:def_31 ::_thesis: GSq . x is real-WEV reconsider G = GSq . x as real-weighted real-elabeled real-vlabeled WEVGraph by A2, Def27, Def29, Def30; G is real-WEV ; hence GSq . x is real-WEV ; ::_thesis: verum end; end; registration cluster Relation-like NAT -defined Function-like total Graph-yielding halting finite loopless trivial non-multi simple Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ; existence ex b1 being WEVGraphSeq st ( b1 is halting & b1 is finite & b1 is loopless & b1 is trivial & b1 is non-multi & b1 is simple & b1 is real-WEV & b1 is nonnegative-weighted & b1 is Tree-like ) proof set G = the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph; set F = NAT --> the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph; A1: dom (NAT --> the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph) = NAT by FUNCOP_1:13; reconsider F = NAT --> the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph as ManySortedSet of NAT ; now__::_thesis:_for_x_being_Nat_holds_F_._x_is__Graph let x be Nat; ::_thesis: F . x is _Graph x in NAT by ORDINAL1:def_12; then F . x in rng F by A1, FUNCT_1:3; then F . x in { the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8; hence F . x is _Graph by TARSKI:def_1; ::_thesis: verum end; then reconsider F = F as GraphSeq by GLIB_000:def_53; now__::_thesis:_for_x_being_Nat_holds_ (_F_._x_is_[Weighted]_&_F_._x_is_[ELabeled]_&_F_._x_is_[VLabeled]_) let x be Nat; ::_thesis: ( F . x is [Weighted] & F . x is [ELabeled] & F . x is [VLabeled] ) x in NAT by ORDINAL1:def_12; then F . x in rng F by A1, FUNCT_1:3; then F . x in { the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8; hence ( F . x is [Weighted] & F . x is [ELabeled] & F . x is [VLabeled] ) by TARSKI:def_1; ::_thesis: verum end; then reconsider F = F as [Weighted] [ELabeled] [VLabeled] GraphSeq by Def24, Def25, Def26; F . (1 + 1) in rng F by A1, FUNCT_1:3; then F . (1 + 1) in { the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8; then A2: F . (1 + 1) = the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph by TARSKI:def_1; take F ; ::_thesis: ( F is halting & F is finite & F is loopless & F is trivial & F is non-multi & F is simple & F is real-WEV & F is nonnegative-weighted & F is Tree-like ) F . 1 in rng F by A1, FUNCT_1:3; then F . 1 in { the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8; then F . 1 = the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph by TARSKI:def_1; hence F is halting by A2, GLIB_000:def_54; ::_thesis: ( F is finite & F is loopless & F is trivial & F is non-multi & F is simple & F is real-WEV & F is nonnegative-weighted & F is Tree-like ) now__::_thesis:_for_x_being_Nat_holds_ (_F_._x_is_finite_&_F_._x_is_loopless_&_F_._x_is_trivial_&_F_._x_is_non-multi_&_F_._x_is_simple_&_F_._x_is_real-WEV_&_F_._x_is_nonnegative-weighted_&_F_._x_is_Tree-like_) let x be Nat; ::_thesis: ( F . x is finite & F . x is loopless & F . x is trivial & F . x is non-multi & F . x is simple & F . x is real-WEV & F . x is nonnegative-weighted & F . x is Tree-like ) x in NAT by ORDINAL1:def_12; then F . x in rng F by A1, FUNCT_1:3; then F . x in { the finite loopless trivial non-multi simple connected acyclic Tree-like nonnegative-weighted real-WEV WEVGraph} by FUNCOP_1:8; hence ( F . x is finite & F . x is loopless & F . x is trivial & F . x is non-multi & F . x is simple & F . x is real-WEV & F . x is nonnegative-weighted & F . x is Tree-like ) by TARSKI:def_1; ::_thesis: verum end; hence ( F is finite & F is loopless & F is trivial & F is non-multi & F is simple & F is real-WEV & F is nonnegative-weighted & F is Tree-like ) by Def28, Def31, GLIB_000:def_57, GLIB_000:def_58, GLIB_000:def_59, GLIB_000:def_61, GLIB_000:def_63, GLIB_002:def_14; ::_thesis: verum end; end; registration let GSq be real-weighted WGraphSeq; let x be Nat; clusterGSq . x -> real-weighted for WGraph; coherence for b1 being WGraph st b1 = GSq . x holds b1 is real-weighted by Def27; end; registration let GSq be nonnegative-weighted WGraphSeq; let x be Nat; clusterGSq . x -> nonnegative-weighted for WGraph; coherence for b1 being WGraph st b1 = GSq . x holds b1 is nonnegative-weighted by Def28; end; registration let GSq be real-elabeled EGraphSeq; let x be Nat; clusterGSq . x -> real-elabeled for EGraph; coherence for b1 being EGraph st b1 = GSq . x holds b1 is real-elabeled by Def29; end; registration let GSq be real-vlabeled VGraphSeq; let x be Nat; clusterGSq . x -> real-vlabeled for VGraph; coherence for b1 being VGraph st b1 = GSq . x holds b1 is real-vlabeled by Def30; end; begin theorem :: GLIB_003:3 ( WeightSelector = 5 & ELabelSelector = 6 & VLabelSelector = 7 ) ; theorem :: GLIB_003:4 ( ( for G being WGraph holds the_Weight_of G = G . WeightSelector ) & ( for G being EGraph holds the_ELabel_of G = G . ELabelSelector ) & ( for G being VGraph holds the_VLabel_of G = G . VLabelSelector ) ) ; theorem :: GLIB_003:5 for G being EGraph holds dom (the_ELabel_of G) c= the_Edges_of G by Lm1; theorem :: GLIB_003:6 for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; theorem :: GLIB_003:7 for G being _Graph for X being set holds ( G == G .set (WeightSelector,X) & G == G .set (ELabelSelector,X) & G == G .set (VLabelSelector,X) ) by Lm3; theorem :: GLIB_003:8 for G1, G2, G3 being WGraph st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 & G1 is WSubgraph of G3 holds G2 is WSubgraph of G3 proof let G1, G2 be WGraph; ::_thesis: for G3 being WGraph st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 & G1 is WSubgraph of G3 holds G2 is WSubgraph of G3 let G3 be WGraph; ::_thesis: ( G1 == G2 & the_Weight_of G1 = the_Weight_of G2 & G1 is WSubgraph of G3 implies G2 is WSubgraph of G3 ) assume that A1: G1 == G2 and A2: the_Weight_of G1 = the_Weight_of G2 and A3: G1 is WSubgraph of G3 ; ::_thesis: G2 is WSubgraph of G3 reconsider G29 = G2 as [Weighted] Subgraph of G3 by A1, A3, GLIB_000:92; the_Edges_of G1 = the_Edges_of G2 by A1, GLIB_000:def_34; then the_Weight_of G2 = (the_Weight_of G3) | (the_Edges_of G2) by A2, A3, Def10; then G29 is weight-inheriting by Def10; hence G2 is WSubgraph of G3 ; ::_thesis: verum end; theorem :: GLIB_003:9 for G1 being WGraph for G2 being WSubgraph of G1 for G3 being WSubgraph of G2 holds G3 is WSubgraph of G1 proof let G1 be WGraph; ::_thesis: for G2 being WSubgraph of G1 for G3 being WSubgraph of G2 holds G3 is WSubgraph of G1 let G2 be WSubgraph of G1; ::_thesis: for G3 being WSubgraph of G2 holds G3 is WSubgraph of G1 let G3 be WSubgraph of G2; ::_thesis: G3 is WSubgraph of G1 reconsider G39 = G3 as [Weighted] Subgraph of G1 by GLIB_000:43; the_Weight_of G3 = (the_Weight_of G2) | (the_Edges_of G3) by Def10 .= ((the_Weight_of G1) | (the_Edges_of G2)) | (the_Edges_of G3) by Def10 .= (the_Weight_of G1) | (the_Edges_of G3) by RELAT_1:74 ; then G39 is weight-inheriting by Def10; hence G3 is WSubgraph of G1 ; ::_thesis: verum end; theorem :: GLIB_003:10 for G1, G2 being WGraph for G3 being WSubgraph of G1 st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds G3 is WSubgraph of G2 proof let G1, G2 be WGraph; ::_thesis: for G3 being WSubgraph of G1 st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds G3 is WSubgraph of G2 let G3 be WSubgraph of G1; ::_thesis: ( G1 == G2 & the_Weight_of G1 = the_Weight_of G2 implies G3 is WSubgraph of G2 ) assume that A1: G1 == G2 and A2: the_Weight_of G1 = the_Weight_of G2 ; ::_thesis: G3 is WSubgraph of G2 reconsider G39 = G3 as [Weighted] Subgraph of G2 by A1, GLIB_000:91; the_Weight_of G3 = (the_Weight_of G2) | (the_Edges_of G3) by A2, Def10; then G39 is WSubgraph of G2 by Def10; hence G3 is WSubgraph of G2 ; ::_thesis: verum end; theorem :: GLIB_003:11 for G1 being WGraph for G2 being WSubgraph of G1 for x being set st x in the_Edges_of G2 holds (the_Weight_of G2) . x = (the_Weight_of G1) . x proof let G1 be WGraph; ::_thesis: for G2 being WSubgraph of G1 for x being set st x in the_Edges_of G2 holds (the_Weight_of G2) . x = (the_Weight_of G1) . x let G2 be WSubgraph of G1; ::_thesis: for x being set st x in the_Edges_of G2 holds (the_Weight_of G2) . x = (the_Weight_of G1) . x let x be set ; ::_thesis: ( x in the_Edges_of G2 implies (the_Weight_of G2) . x = (the_Weight_of G1) . x ) assume x in the_Edges_of G2 ; ::_thesis: (the_Weight_of G2) . x = (the_Weight_of G1) . x then A1: x in dom (the_Weight_of G2) by PARTFUN1:def_2; the_Weight_of G2 = (the_Weight_of G1) | (the_Edges_of G2) by Def10; hence (the_Weight_of G2) . x = (the_Weight_of G1) . x by A1, FUNCT_1:47; ::_thesis: verum end; theorem Th12: :: GLIB_003:12 for G being WGraph for W being Walk of G st W is trivial holds W .weightSeq() = {} proof let G be WGraph; ::_thesis: for W being Walk of G st W is trivial holds W .weightSeq() = {} let W be Walk of G; ::_thesis: ( W is trivial implies W .weightSeq() = {} ) assume W is trivial ; ::_thesis: W .weightSeq() = {} then W .length() = 0 by GLIB_001:def_26; then len (W .edgeSeq()) = 0 by GLIB_001:def_18; then len (W .weightSeq()) = 0 by Def18; hence W .weightSeq() = {} ; ::_thesis: verum end; theorem :: GLIB_003:13 for G being WGraph for W being Walk of G holds len (W .weightSeq()) = W .length() proof let G be WGraph; ::_thesis: for W being Walk of G holds len (W .weightSeq()) = W .length() let W be Walk of G; ::_thesis: len (W .weightSeq()) = W .length() thus len (W .weightSeq()) = len (W .edgeSeq()) by Def18 .= W .length() by GLIB_001:def_18 ; ::_thesis: verum end; theorem Th14: :: GLIB_003:14 for G being WGraph for x, y, e being set st e Joins x,y,G holds (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*> proof let G be WGraph; ::_thesis: for x, y, e being set st e Joins x,y,G holds (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*> let x, y, e be set ; ::_thesis: ( e Joins x,y,G implies (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*> ) set W = G .walkOf (x,e,y); assume e Joins x,y,G ; ::_thesis: (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*> then A1: (G .walkOf (x,e,y)) .edgeSeq() = <*e*> by GLIB_001:83; then len ((G .walkOf (x,e,y)) .edgeSeq()) = 1 by FINSEQ_1:39; then A2: len ((G .walkOf (x,e,y)) .weightSeq()) = 1 by Def18; A3: now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_len_((G_.walkOf_(x,e,y))_.weightSeq())_holds_ ((G_.walkOf_(x,e,y))_.weightSeq())_._n_=_<*((the_Weight_of_G)_._e)*>_._n let n be Nat; ::_thesis: ( 1 <= n & n <= len ((G .walkOf (x,e,y)) .weightSeq()) implies ((G .walkOf (x,e,y)) .weightSeq()) . n = <*((the_Weight_of G) . e)*> . n ) assume that A4: 1 <= n and A5: n <= len ((G .walkOf (x,e,y)) .weightSeq()) ; ::_thesis: ((G .walkOf (x,e,y)) .weightSeq()) . n = <*((the_Weight_of G) . e)*> . n A6: n = 1 by A2, A4, A5, XXREAL_0:1; hence ((G .walkOf (x,e,y)) .weightSeq()) . n = (the_Weight_of G) . (<*e*> . 1) by A1, A5, Def18 .= (the_Weight_of G) . e by FINSEQ_1:40 .= <*((the_Weight_of G) . e)*> . n by A6, FINSEQ_1:40 ; ::_thesis: verum end; len ((G .walkOf (x,e,y)) .weightSeq()) = len <*((the_Weight_of G) . e)*> by A2, FINSEQ_1:39; hence (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*> by A3, FINSEQ_1:14; ::_thesis: verum end; theorem Th15: :: GLIB_003:15 for G being WGraph for W being Walk of G holds (W .reverse()) .weightSeq() = Rev (W .weightSeq()) proof let G be WGraph; ::_thesis: for W being Walk of G holds (W .reverse()) .weightSeq() = Rev (W .weightSeq()) let W be Walk of G; ::_thesis: (W .reverse()) .weightSeq() = Rev (W .weightSeq()) set W1 = (W .reverse()) .weightSeq() ; set W2 = Rev (W .weightSeq()); len (W .reverse()) = len W by GLIB_001:21; then (W .reverse()) .length() = W .length() by GLIB_001:113; then len ((W .reverse()) .edgeSeq()) = W .length() by GLIB_001:def_18 .= len (W .edgeSeq()) by GLIB_001:def_18 ; then A1: len ((W .reverse()) .weightSeq()) = len (W .edgeSeq()) by Def18; A2: len (W .weightSeq()) = len (W .edgeSeq()) by Def18; A3: now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_len_((W_.reverse())_.weightSeq())_holds_ ((W_.reverse())_.weightSeq())_._n_=_(Rev_(W_.weightSeq()))_._n let n be Nat; ::_thesis: ( 1 <= n & n <= len ((W .reverse()) .weightSeq()) implies ((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . n ) assume that A4: 1 <= n and A5: n <= len ((W .reverse()) .weightSeq()) ; ::_thesis: ((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . n A6: n in dom (W .edgeSeq()) by A1, A4, A5, FINSEQ_3:25; set rn = ((len (W .weightSeq())) - n) + 1; reconsider rn = ((len (W .weightSeq())) - n) + 1 as Element of NAT by A1, A2, A5, FINSEQ_5:1; n in Seg (len (W .weightSeq())) by A1, A2, A4, A5, FINSEQ_1:1; then rn in Seg (len (W .weightSeq())) by FINSEQ_5:2; then A7: ( 1 <= rn & rn <= len (W .weightSeq()) ) by FINSEQ_1:1; ((W .reverse()) .weightSeq()) . n = (the_Weight_of G) . (((W .reverse()) .edgeSeq()) . n) by A4, A5, Def18 .= (the_Weight_of G) . ((Rev (W .edgeSeq())) . n) by GLIB_001:84 ; then A8: ((W .reverse()) .weightSeq()) . n = (the_Weight_of G) . ((W .edgeSeq()) . (((len (W .edgeSeq())) - n) + 1)) by A6, FINSEQ_5:58; n in dom (W .weightSeq()) by A1, A2, A4, A5, FINSEQ_3:25; then (Rev (W .weightSeq())) . n = (W .weightSeq()) . rn by FINSEQ_5:58 .= (the_Weight_of G) . ((W .edgeSeq()) . rn) by A7, Def18 ; hence ((W .reverse()) .weightSeq()) . n = (Rev (W .weightSeq())) . n by A8, Def18; ::_thesis: verum end; len ((W .reverse()) .weightSeq()) = len (Rev (W .weightSeq())) by A1, A2, FINSEQ_5:def_3; hence (W .reverse()) .weightSeq() = Rev (W .weightSeq()) by A3, FINSEQ_1:14; ::_thesis: verum end; theorem Th16: :: GLIB_003:16 for G being WGraph for W1, W2 being Walk of G st W1 .last() = W2 .first() holds (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) proof let G be WGraph; ::_thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) let W1, W2 be Walk of G; ::_thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) ) set W3 = W1 .append W2; set W4 = (W1 .weightSeq()) ^ (W2 .weightSeq()); assume A1: W1 .last() = W2 .first() ; ::_thesis: (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) then (W1 .append W2) .edgeSeq() = (W1 .edgeSeq()) ^ (W2 .edgeSeq()) by GLIB_001:85; then len ((W1 .append W2) .edgeSeq()) = (len (W1 .edgeSeq())) + (len (W2 .edgeSeq())) by FINSEQ_1:22; then A2: len ((W1 .append W2) .weightSeq()) = (len (W1 .edgeSeq())) + (len (W2 .edgeSeq())) by Def18 .= (len (W1 .weightSeq())) + (len (W2 .edgeSeq())) by Def18 .= (len (W1 .weightSeq())) + (len (W2 .weightSeq())) by Def18 .= len ((W1 .weightSeq()) ^ (W2 .weightSeq())) by FINSEQ_1:22 ; now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_len_((W1_.append_W2)_.weightSeq())_holds_ ((W1_.append_W2)_.weightSeq())_._n_=_((W1_.weightSeq())_^_(W2_.weightSeq()))_._n let n be Nat; ::_thesis: ( 1 <= n & n <= len ((W1 .append W2) .weightSeq()) implies ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n ) assume A3: ( 1 <= n & n <= len ((W1 .append W2) .weightSeq()) ) ; ::_thesis: ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n then A4: ((W1 .append W2) .weightSeq()) . n = (the_Weight_of G) . (((W1 .append W2) .edgeSeq()) . n) by Def18 .= (the_Weight_of G) . (((W1 .edgeSeq()) ^ (W2 .edgeSeq())) . n) by A1, GLIB_001:85 ; A5: n in dom ((W1 .weightSeq()) ^ (W2 .weightSeq())) by A2, A3, FINSEQ_3:25; now__::_thesis:_((W1_.append_W2)_.weightSeq())_._n_=_((W1_.weightSeq())_^_(W2_.weightSeq()))_._n percases ( n in dom (W1 .weightSeq()) or ex k being Nat st ( k in dom (W2 .weightSeq()) & n = (len (W1 .weightSeq())) + k ) ) by A5, FINSEQ_1:25; supposeA6: n in dom (W1 .weightSeq()) ; ::_thesis: ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n then A7: 1 <= n by FINSEQ_3:25; A8: n <= len (W1 .weightSeq()) by A6, FINSEQ_3:25; then n <= len (W1 .edgeSeq()) by Def18; then A9: n in dom (W1 .edgeSeq()) by A7, FINSEQ_3:25; ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n = (W1 .weightSeq()) . n by A6, FINSEQ_1:def_7 .= (the_Weight_of G) . ((W1 .edgeSeq()) . n) by A7, A8, Def18 ; hence ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n by A4, A9, FINSEQ_1:def_7; ::_thesis: verum end; suppose ex k being Nat st ( k in dom (W2 .weightSeq()) & n = (len (W1 .weightSeq())) + k ) ; ::_thesis: ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n then consider k being Nat such that A10: k in dom (W2 .weightSeq()) and A11: n = (len (W1 .weightSeq())) + k ; A12: 1 <= k by A10, FINSEQ_3:25; A13: k <= len (W2 .weightSeq()) by A10, FINSEQ_3:25; then k <= len (W2 .edgeSeq()) by Def18; then A14: k in dom (W2 .edgeSeq()) by A12, FINSEQ_3:25; A15: n = (len (W1 .edgeSeq())) + k by A11, Def18; ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n = (W2 .weightSeq()) . k by A10, A11, FINSEQ_1:def_7 .= (the_Weight_of G) . ((W2 .edgeSeq()) . k) by A12, A13, Def18 ; hence ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n by A4, A14, A15, FINSEQ_1:def_7; ::_thesis: verum end; end; end; hence ((W1 .append W2) .weightSeq()) . n = ((W1 .weightSeq()) ^ (W2 .weightSeq())) . n ; ::_thesis: verum end; hence (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) by A2, FINSEQ_1:14; ::_thesis: verum end; theorem Th17: :: GLIB_003:17 for G being WGraph for W being Walk of G for e being set st e in (W .last()) .edgesInOut() holds (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> proof let G be WGraph; ::_thesis: for W being Walk of G for e being set st e in (W .last()) .edgesInOut() holds (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> let W be Walk of G; ::_thesis: for e being set st e in (W .last()) .edgesInOut() holds (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> let e be set ; ::_thesis: ( e in (W .last()) .edgesInOut() implies (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> ) set W2 = W .addEdge e; set WA = G .walkOf ((W .last()),e,((W .last()) .adj e)); assume e in (W .last()) .edgesInOut() ; ::_thesis: (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> then A1: e Joins W .last() ,(W .last()) .adj e,G by GLIB_000:67; then ( W .addEdge e = W .append (G .walkOf ((W .last()),e,((W .last()) .adj e))) & W .last() = (G .walkOf ((W .last()),e,((W .last()) .adj e))) .first() ) by GLIB_001:15, GLIB_001:def_13; hence (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ ((G .walkOf ((W .last()),e,((W .last()) .adj e))) .weightSeq()) by Th16 .= (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> by A1, Th14 ; ::_thesis: verum end; theorem Th18: :: GLIB_003:18 for G being real-weighted WGraph for W1 being Walk of G for W2 being Subwalk of W1 ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws proof let G be real-weighted WGraph; ::_thesis: for W1 being Walk of G for W2 being Subwalk of W1 ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws let W1 be Walk of G; ::_thesis: for W2 being Subwalk of W1 ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws let W2 be Subwalk of W1; ::_thesis: ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws consider es being Subset of (W1 .edgeSeq()) such that A1: W2 .edgeSeq() = Seq es by GLIB_001:def_32; deffunc H1( set ) -> Element of REAL = (the_Weight_of G) . (es . $1); consider ws being Function such that A2: ( dom ws = dom es & ( for x being set st x in dom es holds ws . x = H1(x) ) ) from FUNCT_1:sch_3(); A3: ex k being Nat st dom ws c= Seg k by A2, FINSEQ_1:def_12; then reconsider ws = ws as FinSubsequence by FINSEQ_1:def_12; now__::_thesis:_for_z_being_set_st_z_in_ws_holds_ z_in_W1_.weightSeq() let z be set ; ::_thesis: ( z in ws implies z in W1 .weightSeq() ) assume A4: z in ws ; ::_thesis: z in W1 .weightSeq() then consider x, y being set such that A5: z = [x,y] by RELAT_1:def_1; A6: x in dom es by A2, A4, A5, FUNCT_1:1; then A7: [x,(es . x)] in es by FUNCT_1:1; then A8: x in dom (W1 .edgeSeq()) by FUNCT_1:1; A9: ws . x = y by A4, A5, FUNCT_1:1; reconsider x = x as Element of NAT by A8; x <= len (W1 .edgeSeq()) by A8, FINSEQ_3:25; then A10: x <= len (W1 .weightSeq()) by Def18; A11: 1 <= x by A8, FINSEQ_3:25; then A12: (W1 .weightSeq()) . x = (the_Weight_of G) . ((W1 .edgeSeq()) . x) by A10, Def18; x in dom (W1 .weightSeq()) by A11, A10, FINSEQ_3:25; then A13: [x,((W1 .weightSeq()) . x)] in W1 .weightSeq() by FUNCT_1:1; y = (the_Weight_of G) . (es . x) by A2, A6, A9; hence z in W1 .weightSeq() by A5, A7, A13, A12, FUNCT_1:1; ::_thesis: verum end; then reconsider ws = ws as Subset of (W1 .weightSeq()) by TARSKI:def_3; take ws ; ::_thesis: W2 .weightSeq() = Seq ws A14: len (Seq es) = card es by GLIB_001:5 .= card (dom ws) by A2, CARD_1:62 .= card ws by CARD_1:62 .= len (Seq ws) by GLIB_001:5 ; then A15: len (W2 .weightSeq()) = len (Seq ws) by A1, Def18; now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_len_(W2_.weightSeq())_holds_ (W2_.weightSeq())_._n_=_(Seq_ws)_._n A16: rng (Sgm (dom es)) = dom es by A2, A3, FINSEQ_1:def_13; let n be Nat; ::_thesis: ( 1 <= n & n <= len (W2 .weightSeq()) implies (W2 .weightSeq()) . n = (Seq ws) . n ) A17: Seq ws = ws * (Sgm (dom es)) by A2, FINSEQ_1:def_14; assume A18: ( 1 <= n & n <= len (W2 .weightSeq()) ) ; ::_thesis: (W2 .weightSeq()) . n = (Seq ws) . n then A19: ( Seq es = es * (Sgm (dom es)) & n in dom (Seq es) ) by A14, A15, FINSEQ_1:def_14, FINSEQ_3:25; A20: n in dom (Seq ws) by A15, A18, FINSEQ_3:25; then n in dom (Sgm (dom es)) by A17, FUNCT_1:11; then A21: (Sgm (dom es)) . n in dom es by A16, FUNCT_1:def_3; (Seq ws) . n = ws . ((Sgm (dom es)) . n) by A17, A20, FUNCT_1:12 .= (the_Weight_of G) . (es . ((Sgm (dom es)) . n)) by A2, A21 .= (the_Weight_of G) . ((Seq es) . n) by A19, FUNCT_1:12 ; hence (W2 .weightSeq()) . n = (Seq ws) . n by A1, A18, Def18; ::_thesis: verum end; hence W2 .weightSeq() = Seq ws by A15, FINSEQ_1:14; ::_thesis: verum end; theorem Th19: :: GLIB_003:19 for G1, G2 being WGraph for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds W1 .weightSeq() = W2 .weightSeq() proof let G1, G2 be WGraph; ::_thesis: for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds W1 .weightSeq() = W2 .weightSeq() let W1 be Walk of G1; ::_thesis: for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds W1 .weightSeq() = W2 .weightSeq() let W2 be Walk of G2; ::_thesis: ( W1 = W2 & the_Weight_of G1 = the_Weight_of G2 implies W1 .weightSeq() = W2 .weightSeq() ) assume that A1: W1 = W2 and A2: the_Weight_of G1 = the_Weight_of G2 ; ::_thesis: W1 .weightSeq() = W2 .weightSeq() set WS1 = W1 .weightSeq() ; set WS2 = W2 .weightSeq() ; A3: W1 .edgeSeq() = W2 .edgeSeq() by A1, GLIB_001:86; now__::_thesis:_(_len_(W1_.weightSeq())_=_len_(W1_.weightSeq())_&_len_(W2_.weightSeq())_=_len_(W1_.weightSeq())_&_(_for_x_being_Nat_st_x_in_dom_(W1_.weightSeq())_holds_ (W2_.weightSeq())_._x_=_(W1_.weightSeq())_._x_)_) thus len (W1 .weightSeq()) = len (W1 .weightSeq()) ; ::_thesis: ( len (W2 .weightSeq()) = len (W1 .weightSeq()) & ( for x being Nat st x in dom (W1 .weightSeq()) holds (W2 .weightSeq()) . x = (W1 .weightSeq()) . x ) ) thus A4: len (W2 .weightSeq()) = len (W1 .edgeSeq()) by A3, Def18 .= len (W1 .weightSeq()) by Def18 ; ::_thesis: for x being Nat st x in dom (W1 .weightSeq()) holds (W2 .weightSeq()) . x = (W1 .weightSeq()) . x let x be Nat; ::_thesis: ( x in dom (W1 .weightSeq()) implies (W2 .weightSeq()) . x = (W1 .weightSeq()) . x ) assume A5: x in dom (W1 .weightSeq()) ; ::_thesis: (W2 .weightSeq()) . x = (W1 .weightSeq()) . x then A6: 1 <= x by FINSEQ_3:25; A7: x <= len (W1 .weightSeq()) by A5, FINSEQ_3:25; x <= len (W2 .weightSeq()) by A4, A5, FINSEQ_3:25; hence (W2 .weightSeq()) . x = (the_Weight_of G2) . ((W2 .edgeSeq()) . x) by A6, Def18 .= (the_Weight_of G1) . ((W1 .edgeSeq()) . x) by A1, A2, GLIB_001:86 .= (W1 .weightSeq()) . x by A6, A7, Def18 ; ::_thesis: verum end; hence W1 .weightSeq() = W2 .weightSeq() by FINSEQ_2:9; ::_thesis: verum end; theorem Th20: :: GLIB_003:20 for G1 being WGraph for G2 being WSubgraph of G1 for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds W1 .weightSeq() = W2 .weightSeq() proof let G1 be WGraph; ::_thesis: for G2 being WSubgraph of G1 for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds W1 .weightSeq() = W2 .weightSeq() let G2 be WSubgraph of G1; ::_thesis: for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds W1 .weightSeq() = W2 .weightSeq() let W1 be Walk of G1; ::_thesis: for W2 being Walk of G2 st W1 = W2 holds W1 .weightSeq() = W2 .weightSeq() let W2 be Walk of G2; ::_thesis: ( W1 = W2 implies W1 .weightSeq() = W2 .weightSeq() ) set WS1 = W1 .weightSeq() ; set WS2 = W2 .weightSeq() ; assume W1 = W2 ; ::_thesis: W1 .weightSeq() = W2 .weightSeq() then A1: W1 .edgeSeq() = W2 .edgeSeq() by GLIB_001:86; now__::_thesis:_(_len_(W1_.weightSeq())_=_len_(W1_.weightSeq())_&_len_(W2_.weightSeq())_=_len_(W1_.weightSeq())_&_(_for_x_being_Nat_st_x_in_dom_(W1_.weightSeq())_holds_ (W2_.weightSeq())_._x_=_(W1_.weightSeq())_._x_)_) thus len (W1 .weightSeq()) = len (W1 .weightSeq()) ; ::_thesis: ( len (W2 .weightSeq()) = len (W1 .weightSeq()) & ( for x being Nat st x in dom (W1 .weightSeq()) holds (W2 .weightSeq()) . x = (W1 .weightSeq()) . x ) ) thus A2: len (W2 .weightSeq()) = len (W1 .edgeSeq()) by A1, Def18 .= len (W1 .weightSeq()) by Def18 ; ::_thesis: for x being Nat st x in dom (W1 .weightSeq()) holds (W2 .weightSeq()) . x = (W1 .weightSeq()) . x let x be Nat; ::_thesis: ( x in dom (W1 .weightSeq()) implies (W2 .weightSeq()) . x = (W1 .weightSeq()) . x ) assume A3: x in dom (W1 .weightSeq()) ; ::_thesis: (W2 .weightSeq()) . x = (W1 .weightSeq()) . x then A4: 1 <= x by FINSEQ_3:25; A5: x <= len (W2 .weightSeq()) by A2, A3, FINSEQ_3:25; then x <= len (W2 .edgeSeq()) by Def18; then A6: x in dom (W2 .edgeSeq()) by A4, FINSEQ_3:25; A7: x <= len (W1 .weightSeq()) by A3, FINSEQ_3:25; thus (W2 .weightSeq()) . x = (the_Weight_of G2) . ((W2 .edgeSeq()) . x) by A4, A5, Def18 .= ((the_Weight_of G1) | (the_Edges_of G2)) . ((W2 .edgeSeq()) . x) by Def10 .= (the_Weight_of G1) . ((W1 .edgeSeq()) . x) by A1, A6, FUNCT_1:49, GLIB_001:79 .= (W1 .weightSeq()) . x by A4, A7, Def18 ; ::_thesis: verum end; hence W1 .weightSeq() = W2 .weightSeq() by FINSEQ_2:9; ::_thesis: verum end; theorem :: GLIB_003:21 for G being real-weighted WGraph for W being Walk of G st W is trivial holds W .cost() = 0 by Th12, RVSUM_1:72; theorem :: GLIB_003:22 for G being real-weighted WGraph for v1, v2 being Vertex of G for e being set st e Joins v1,v2,G holds (G .walkOf (v1,e,v2)) .cost() = (the_Weight_of G) . e proof let G be real-weighted WGraph; ::_thesis: for v1, v2 being Vertex of G for e being set st e Joins v1,v2,G holds (G .walkOf (v1,e,v2)) .cost() = (the_Weight_of G) . e let v1, v2 be Vertex of G; ::_thesis: for e being set st e Joins v1,v2,G holds (G .walkOf (v1,e,v2)) .cost() = (the_Weight_of G) . e let e be set ; ::_thesis: ( e Joins v1,v2,G implies (G .walkOf (v1,e,v2)) .cost() = (the_Weight_of G) . e ) set W = G .walkOf (v1,e,v2); assume e Joins v1,v2,G ; ::_thesis: (G .walkOf (v1,e,v2)) .cost() = (the_Weight_of G) . e then (G .walkOf (v1,e,v2)) .weightSeq() = <*((the_Weight_of G) . e)*> by Th14; hence (G .walkOf (v1,e,v2)) .cost() = (the_Weight_of G) . e by FINSOP_1:11; ::_thesis: verum end; theorem :: GLIB_003:23 for G being real-weighted WGraph for W being Walk of G holds W .cost() = (W .reverse()) .cost() proof let G be real-weighted WGraph; ::_thesis: for W being Walk of G holds W .cost() = (W .reverse()) .cost() let W be Walk of G; ::_thesis: W .cost() = (W .reverse()) .cost() thus W .cost() = Sum (Rev (W .weightSeq())) by POLYNOM3:3 .= (W .reverse()) .cost() by Th15 ; ::_thesis: verum end; theorem :: GLIB_003:24 for G being real-weighted WGraph for W1, W2 being Walk of G st W1 .last() = W2 .first() holds (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost()) proof let G be real-weighted WGraph; ::_thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost()) let W1, W2 be Walk of G; ::_thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost()) ) set W3 = W1 .append W2; assume W1 .last() = W2 .first() ; ::_thesis: (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost()) then (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) by Th16; hence (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost()) by RVSUM_1:75; ::_thesis: verum end; theorem :: GLIB_003:25 for G being real-weighted WGraph for W being Walk of G for e being set st e in (W .last()) .edgesInOut() holds (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) proof let G be real-weighted WGraph; ::_thesis: for W being Walk of G for e being set st e in (W .last()) .edgesInOut() holds (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) let W be Walk of G; ::_thesis: for e being set st e in (W .last()) .edgesInOut() holds (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) let e be set ; ::_thesis: ( e in (W .last()) .edgesInOut() implies (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) ) set W2 = W .addEdge e; assume e in (W .last()) .edgesInOut() ; ::_thesis: (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) then (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> by Th17; then Sum ((W .addEdge e) .weightSeq()) = (Sum (W .weightSeq())) + (Sum <*((the_Weight_of G) . e)*>) by RVSUM_1:75; hence (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) by FINSOP_1:11; ::_thesis: verum end; theorem :: GLIB_003:26 for G1, G2 being real-weighted WGraph for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds W1 .cost() = W2 .cost() by Th19; theorem :: GLIB_003:27 for G1 being real-weighted WGraph for G2 being WSubgraph of G1 for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds W1 .cost() = W2 .cost() by Th20; theorem Th28: :: GLIB_003:28 for G being nonnegative-weighted WGraph for W being Walk of G for n being Element of NAT st n in dom (W .weightSeq()) holds 0 <= (W .weightSeq()) . n proof let G be nonnegative-weighted WGraph; ::_thesis: for W being Walk of G for n being Element of NAT st n in dom (W .weightSeq()) holds 0 <= (W .weightSeq()) . n let W be Walk of G; ::_thesis: for n being Element of NAT st n in dom (W .weightSeq()) holds 0 <= (W .weightSeq()) . n let n be Element of NAT ; ::_thesis: ( n in dom (W .weightSeq()) implies 0 <= (W .weightSeq()) . n ) set WS = W .weightSeq() ; assume A1: n in dom (W .weightSeq()) ; ::_thesis: 0 <= (W .weightSeq()) . n then A2: 1 <= n by FINSEQ_3:25; A3: n <= len (W .weightSeq()) by A1, FINSEQ_3:25; then n <= len (W .edgeSeq()) by Def18; then ( dom (the_Weight_of G) = the_Edges_of G & n in dom (W .edgeSeq()) ) by A2, FINSEQ_3:25, PARTFUN1:def_2; then A4: (W .edgeSeq()) . n in dom (the_Weight_of G) by GLIB_001:79; (W .weightSeq()) . n = (the_Weight_of G) . ((W .edgeSeq()) . n) by A2, A3, Def18; then A5: (W .weightSeq()) . n in rng (the_Weight_of G) by A4, FUNCT_1:def_3; rng (the_Weight_of G) c= Real>=0 by Def14; then (W .weightSeq()) . n in Real>=0 by A5; then ex r being Real st ( r = (W .weightSeq()) . n & r >= 0 ) by GRAPH_5:def_12; hence 0 <= (W .weightSeq()) . n ; ::_thesis: verum end; theorem :: GLIB_003:29 for G being nonnegative-weighted WGraph for W being Walk of G holds 0 <= W .cost() proof let G be nonnegative-weighted WGraph; ::_thesis: for W being Walk of G holds 0 <= W .cost() let W be Walk of G; ::_thesis: 0 <= W .cost() for i being Nat st i in dom (W .weightSeq()) holds 0 <= (W .weightSeq()) . i by Th28; hence 0 <= W .cost() by RVSUM_1:84; ::_thesis: verum end; theorem :: GLIB_003:30 for G being nonnegative-weighted WGraph for W1 being Walk of G for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost() proof let G be nonnegative-weighted WGraph; ::_thesis: for W1 being Walk of G for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost() let W1 be Walk of G; ::_thesis: for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost() let W2 be Subwalk of W1; ::_thesis: W2 .cost() <= W1 .cost() ( ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws & ( for i being Element of NAT st i in dom (W1 .weightSeq()) holds 0 <= (W1 .weightSeq()) . i ) ) by Th18, Th28; hence W2 .cost() <= W1 .cost() by Th2; ::_thesis: verum end; theorem :: GLIB_003:31 for G being nonnegative-weighted WGraph for e being set st e in the_Edges_of G holds 0 <= (the_Weight_of G) . e proof let G be nonnegative-weighted WGraph; ::_thesis: for e being set st e in the_Edges_of G holds 0 <= (the_Weight_of G) . e let e be set ; ::_thesis: ( e in the_Edges_of G implies 0 <= (the_Weight_of G) . e ) assume e in the_Edges_of G ; ::_thesis: 0 <= (the_Weight_of G) . e then e in dom (the_Weight_of G) by PARTFUN1:def_2; then A1: (the_Weight_of G) . e in rng (the_Weight_of G) by FUNCT_1:3; rng (the_Weight_of G) c= Real>=0 by Def14; then (the_Weight_of G) . e in Real>=0 by A1; then ex r being Real st ( (the_Weight_of G) . e = r & r >= 0 ) by GRAPH_5:def_12; hence 0 <= (the_Weight_of G) . e ; ::_thesis: verum end; theorem Th32: :: GLIB_003:32 for G being EGraph for e, x being set st e in the_Edges_of G holds the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) proof let G be EGraph; ::_thesis: for e, x being set st e in the_Edges_of G holds the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) let e, x be set ; ::_thesis: ( e in the_Edges_of G implies the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) ) assume e in the_Edges_of G ; ::_thesis: the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) then the_ELabel_of (G .labelEdge (e,x)) = (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) . ELabelSelector by Def21; hence the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) by GLIB_000:8; ::_thesis: verum end; theorem :: GLIB_003:33 for G being EGraph for e, x being set st e in the_Edges_of G holds (the_ELabel_of (G .labelEdge (e,x))) . e = x proof let G be EGraph; ::_thesis: for e, x being set st e in the_Edges_of G holds (the_ELabel_of (G .labelEdge (e,x))) . e = x let e, x be set ; ::_thesis: ( e in the_Edges_of G implies (the_ELabel_of (G .labelEdge (e,x))) . e = x ) e in {e} by TARSKI:def_1; then A1: e in dom (e .--> x) by FUNCOP_1:13; assume e in the_Edges_of G ; ::_thesis: (the_ELabel_of (G .labelEdge (e,x))) . e = x then the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) by Th32; then (the_ELabel_of (G .labelEdge (e,x))) . e = (e .--> x) . e by A1, FUNCT_4:13 .= x by FUNCOP_1:72 ; hence (the_ELabel_of (G .labelEdge (e,x))) . e = x ; ::_thesis: verum end; theorem :: GLIB_003:34 for G being EGraph for e, x being set holds G == G .labelEdge (e,x) proof let G be EGraph; ::_thesis: for e, x being set holds G == G .labelEdge (e,x) let e, x be set ; ::_thesis: G == G .labelEdge (e,x) now__::_thesis:_G_==_G_.labelEdge_(e,x) percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; supposeA1: e in the_Edges_of G ; ::_thesis: G == G .labelEdge (e,x) A2: not ELabelSelector in _GraphSelectors by ENUMSET1:def_2; A3: G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by A1, Def21; then A4: ( the_Source_of G = the_Source_of (G .labelEdge (e,x)) & the_Target_of G = the_Target_of (G .labelEdge (e,x)) ) by A2, GLIB_000:10; ( the_Vertices_of G = the_Vertices_of (G .labelEdge (e,x)) & the_Edges_of G = the_Edges_of (G .labelEdge (e,x)) ) by A3, A2, GLIB_000:10; hence G == G .labelEdge (e,x) by A4, GLIB_000:def_34; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: G == G .labelEdge (e,x) hence G == G .labelEdge (e,x) by Def21; ::_thesis: verum end; end; end; hence G == G .labelEdge (e,x) ; ::_thesis: verum end; theorem :: GLIB_003:35 for G being WEGraph for e, x being set holds the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) proof let G be WEGraph; ::_thesis: for e, x being set holds the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) let e, x be set ; ::_thesis: the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) set G2 = G .labelEdge (e,x); now__::_thesis:_the_Weight_of_G_=_the_Weight_of_(G_.labelEdge_(e,x)) percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) by GLIB_000:9; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) hence the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) by Def21; ::_thesis: verum end; end; end; hence the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) ; ::_thesis: verum end; theorem Th36: :: GLIB_003:36 for G being EVGraph for e, x being set holds the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) proof let G be EVGraph; ::_thesis: for e, x being set holds the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) let e, x be set ; ::_thesis: the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) set G2 = G .labelEdge (e,x); now__::_thesis:_the_VLabel_of_G_=_the_VLabel_of_(G_.labelEdge_(e,x)) percases ( e in the_Edges_of G or not e in the_Edges_of G ) ; suppose e in the_Edges_of G ; ::_thesis: the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21; hence the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) by GLIB_000:9; ::_thesis: verum end; suppose not e in the_Edges_of G ; ::_thesis: the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) hence the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) by Def21; ::_thesis: verum end; end; end; hence the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) ; ::_thesis: verum end; theorem :: GLIB_003:37 for G being EGraph for e1, e2, x being set st e1 <> e2 holds (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 proof let G be EGraph; ::_thesis: for e1, e2, x being set st e1 <> e2 holds (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 let e1, e2, x be set ; ::_thesis: ( e1 <> e2 implies (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 ) set G2 = G .labelEdge (e1,x); assume A1: e1 <> e2 ; ::_thesis: (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 now__::_thesis:_(the_ELabel_of_(G_.labelEdge_(e1,x)))_._e2_=_(the_ELabel_of_G)_._e2 percases ( e1 in the_Edges_of G or not e1 in the_Edges_of G ) ; supposeA2: e1 in the_Edges_of G ; ::_thesis: (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 not e2 in {e1} by A1, TARSKI:def_1; then A3: not e2 in dom (e1 .--> x) ; the_ELabel_of (G .labelEdge (e1,x)) = (the_ELabel_of G) +* (e1 .--> x) by A2, Th32; hence (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 by A3, FUNCT_4:11; ::_thesis: verum end; suppose not e1 in the_Edges_of G ; ::_thesis: (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 hence (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 by Def21; ::_thesis: verum end; end; end; hence (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 ; ::_thesis: verum end; theorem Th38: :: GLIB_003:38 for G being VGraph for v, x being set st v in the_Vertices_of G holds the_VLabel_of (G .labelVertex (v,x)) = (the_VLabel_of G) +* (v .--> x) proof let G be VGraph; ::_thesis: for v, x being set st v in the_Vertices_of G holds the_VLabel_of (G .labelVertex (v,x)) = (the_VLabel_of G) +* (v .--> x) let e, x be set ; ::_thesis: ( e in the_Vertices_of G implies the_VLabel_of (G .labelVertex (e,x)) = (the_VLabel_of G) +* (e .--> x) ) assume e in the_Vertices_of G ; ::_thesis: the_VLabel_of (G .labelVertex (e,x)) = (the_VLabel_of G) +* (e .--> x) then the_VLabel_of (G .labelVertex (e,x)) = (G .set (VLabelSelector,((the_VLabel_of G) +* (e .--> x)))) . VLabelSelector by Def22; hence the_VLabel_of (G .labelVertex (e,x)) = (the_VLabel_of G) +* (e .--> x) by GLIB_000:8; ::_thesis: verum end; theorem :: GLIB_003:39 for G being VGraph for v, x being set st v in the_Vertices_of G holds (the_VLabel_of (G .labelVertex (v,x))) . v = x proof let G be VGraph; ::_thesis: for v, x being set st v in the_Vertices_of G holds (the_VLabel_of (G .labelVertex (v,x))) . v = x let e, x be set ; ::_thesis: ( e in the_Vertices_of G implies (the_VLabel_of (G .labelVertex (e,x))) . e = x ) e in {e} by TARSKI:def_1; then A1: e in dom (e .--> x) by FUNCOP_1:13; assume e in the_Vertices_of G ; ::_thesis: (the_VLabel_of (G .labelVertex (e,x))) . e = x then the_VLabel_of (G .labelVertex (e,x)) = (the_VLabel_of G) +* (e .--> x) by Th38; then (the_VLabel_of (G .labelVertex (e,x))) . e = (e .--> x) . e by A1, FUNCT_4:13 .= x by FUNCOP_1:72 ; hence (the_VLabel_of (G .labelVertex (e,x))) . e = x ; ::_thesis: verum end; theorem :: GLIB_003:40 for G being VGraph for v, x being set holds G == G .labelVertex (v,x) proof let G be VGraph; ::_thesis: for v, x being set holds G == G .labelVertex (v,x) let e, x be set ; ::_thesis: G == G .labelVertex (e,x) now__::_thesis:_G_==_G_.labelVertex_(e,x) percases ( e in the_Vertices_of G or not e in the_Vertices_of G ) ; supposeA1: e in the_Vertices_of G ; ::_thesis: G == G .labelVertex (e,x) A2: not VLabelSelector in _GraphSelectors by ENUMSET1:def_2; A3: G .labelVertex (e,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (e .--> x))) by A1, Def22; then A4: ( the_Source_of G = the_Source_of (G .labelVertex (e,x)) & the_Target_of G = the_Target_of (G .labelVertex (e,x)) ) by A2, GLIB_000:10; ( the_Vertices_of G = the_Vertices_of (G .labelVertex (e,x)) & the_Edges_of G = the_Edges_of (G .labelVertex (e,x)) ) by A3, A2, GLIB_000:10; hence G == G .labelVertex (e,x) by A4, GLIB_000:def_34; ::_thesis: verum end; suppose not e in the_Vertices_of G ; ::_thesis: G == G .labelVertex (e,x) hence G == G .labelVertex (e,x) by Def22; ::_thesis: verum end; end; end; hence G == G .labelVertex (e,x) ; ::_thesis: verum end; theorem :: GLIB_003:41 for G being WVGraph for v, x being set holds the_Weight_of G = the_Weight_of (G .labelVertex (v,x)) proof let G be WVGraph; ::_thesis: for v, x being set holds the_Weight_of G = the_Weight_of (G .labelVertex (v,x)) let e, x be set ; ::_thesis: the_Weight_of G = the_Weight_of (G .labelVertex (e,x)) set G2 = G .labelVertex (e,x); now__::_thesis:_the_Weight_of_G_=_the_Weight_of_(G_.labelVertex_(e,x)) percases ( e in the_Vertices_of G or not e in the_Vertices_of G ) ; suppose e in the_Vertices_of G ; ::_thesis: the_Weight_of G = the_Weight_of (G .labelVertex (e,x)) then G .labelVertex (e,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (e .--> x))) by Def22; hence the_Weight_of G = the_Weight_of (G .labelVertex (e,x)) by GLIB_000:9; ::_thesis: verum end; suppose not e in the_Vertices_of G ; ::_thesis: the_Weight_of G = the_Weight_of (G .labelVertex (e,x)) hence the_Weight_of G = the_Weight_of (G .labelVertex (e,x)) by Def22; ::_thesis: verum end; end; end; hence the_Weight_of G = the_Weight_of (G .labelVertex (e,x)) ; ::_thesis: verum end; theorem Th42: :: GLIB_003:42 for G being EVGraph for v, x being set holds the_ELabel_of G = the_ELabel_of (G .labelVertex (v,x)) proof let G be EVGraph; ::_thesis: for v, x being set holds the_ELabel_of G = the_ELabel_of (G .labelVertex (v,x)) let e, x be set ; ::_thesis: the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x)) set G2 = G .labelVertex (e,x); now__::_thesis:_the_ELabel_of_G_=_the_ELabel_of_(G_.labelVertex_(e,x)) percases ( e in the_Vertices_of G or not e in the_Vertices_of G ) ; suppose e in the_Vertices_of G ; ::_thesis: the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x)) then G .labelVertex (e,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (e .--> x))) by Def22; hence the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x)) by GLIB_000:9; ::_thesis: verum end; suppose not e in the_Vertices_of G ; ::_thesis: the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x)) hence the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x)) by Def22; ::_thesis: verum end; end; end; hence the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x)) ; ::_thesis: verum end; theorem :: GLIB_003:43 for G being VGraph for v1, v2, x being set st v1 <> v2 holds (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 proof let G be VGraph; ::_thesis: for v1, v2, x being set st v1 <> v2 holds (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 let v1, v2, x be set ; ::_thesis: ( v1 <> v2 implies (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 ) set G2 = G .labelVertex (v1,x); assume A1: v1 <> v2 ; ::_thesis: (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 now__::_thesis:_(the_VLabel_of_(G_.labelVertex_(v1,x)))_._v2_=_(the_VLabel_of_G)_._v2 percases ( v1 in the_Vertices_of G or not v1 in the_Vertices_of G ) ; supposeA2: v1 in the_Vertices_of G ; ::_thesis: (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 not v2 in {v1} by A1, TARSKI:def_1; then A3: not v2 in dom (v1 .--> x) ; the_VLabel_of (G .labelVertex (v1,x)) = (the_VLabel_of G) +* (v1 .--> x) by A2, Th38; hence (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 by A3, FUNCT_4:11; ::_thesis: verum end; suppose not v1 in the_Vertices_of G ; ::_thesis: (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 hence (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 by Def22; ::_thesis: verum end; end; end; hence (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 ; ::_thesis: verum end; theorem :: GLIB_003:44 for G1, G2 being EGraph st the_ELabel_of G1 = the_ELabel_of G2 holds G1 .labeledE() = G2 .labeledE() ; theorem Th45: :: GLIB_003:45 for G being EGraph for e, x being set st e in the_Edges_of G holds (G .labelEdge (e,x)) .labeledE() = (G .labeledE()) \/ {e} proof let G be EGraph; ::_thesis: for e, x being set st e in the_Edges_of G holds (G .labelEdge (e,x)) .labeledE() = (G .labeledE()) \/ {e} let e, val be set ; ::_thesis: ( e in the_Edges_of G implies (G .labelEdge (e,val)) .labeledE() = (G .labeledE()) \/ {e} ) set G2 = G .labelEdge (e,val); set EG = the_ELabel_of G; set EG2 = the_ELabel_of (G .labelEdge (e,val)); assume e in the_Edges_of G ; ::_thesis: (G .labelEdge (e,val)) .labeledE() = (G .labeledE()) \/ {e} then the_ELabel_of (G .labelEdge (e,val)) = (the_ELabel_of G) +* (e .--> val) by Th32; then dom (the_ELabel_of (G .labelEdge (e,val))) = (dom (the_ELabel_of G)) \/ (dom (e .--> val)) by FUNCT_4:def_1; hence (G .labelEdge (e,val)) .labeledE() = (G .labeledE()) \/ {e} by FUNCOP_1:13; ::_thesis: verum end; theorem :: GLIB_003:46 for G being EGraph for e, x being set st e in the_Edges_of G holds G .labeledE() c= (G .labelEdge (e,x)) .labeledE() proof let G be EGraph; ::_thesis: for e, x being set st e in the_Edges_of G holds G .labeledE() c= (G .labelEdge (e,x)) .labeledE() let e, x be set ; ::_thesis: ( e in the_Edges_of G implies G .labeledE() c= (G .labelEdge (e,x)) .labeledE() ) assume e in the_Edges_of G ; ::_thesis: G .labeledE() c= (G .labelEdge (e,x)) .labeledE() then (G .labelEdge (e,x)) .labeledE() = (G .labeledE()) \/ {e} by Th45; hence G .labeledE() c= (G .labelEdge (e,x)) .labeledE() by XBOOLE_1:7; ::_thesis: verum end; theorem :: GLIB_003:47 for G being finite EGraph for e, x being set st e in the_Edges_of G & not e in G .labeledE() holds card ((G .labelEdge (e,x)) .labeledE()) = (card (G .labeledE())) + 1 proof let G be finite EGraph; ::_thesis: for e, x being set st e in the_Edges_of G & not e in G .labeledE() holds card ((G .labelEdge (e,x)) .labeledE()) = (card (G .labeledE())) + 1 let e, val be set ; ::_thesis: ( e in the_Edges_of G & not e in G .labeledE() implies card ((G .labelEdge (e,val)) .labeledE()) = (card (G .labeledE())) + 1 ) set G2 = G .labelEdge (e,val); set ECurr = the_ELabel_of G; set ENext = the_ELabel_of (G .labelEdge (e,val)); assume ( e in the_Edges_of G & not e in G .labeledE() ) ; ::_thesis: card ((G .labelEdge (e,val)) .labeledE()) = (card (G .labeledE())) + 1 then A1: ( card ((dom (the_ELabel_of G)) \/ {e}) = (card (dom (the_ELabel_of G))) + 1 & the_ELabel_of (G .labelEdge (e,val)) = (the_ELabel_of G) +* (e .--> val) ) by Th32, CARD_2:41; dom (e .--> val) = {e} by FUNCOP_1:13; hence card ((G .labelEdge (e,val)) .labeledE()) = (card (G .labeledE())) + 1 by A1, FUNCT_4:def_1; ::_thesis: verum end; theorem :: GLIB_003:48 for G being EGraph for e1, e2, x being set st not e2 in G .labeledE() & e2 in (G .labelEdge (e1,x)) .labeledE() holds ( e1 = e2 & e1 in the_Edges_of G ) proof let G be EGraph; ::_thesis: for e1, e2, x being set st not e2 in G .labeledE() & e2 in (G .labelEdge (e1,x)) .labeledE() holds ( e1 = e2 & e1 in the_Edges_of G ) let e1, e2, val be set ; ::_thesis: ( not e2 in G .labeledE() & e2 in (G .labelEdge (e1,val)) .labeledE() implies ( e1 = e2 & e1 in the_Edges_of G ) ) set Gn = G .labelEdge (e1,val); assume that A1: not e2 in G .labeledE() and A2: e2 in (G .labelEdge (e1,val)) .labeledE() ; ::_thesis: ( e1 = e2 & e1 in the_Edges_of G ) e1 in the_Edges_of G by A1, A2, Def21; then the_ELabel_of (G .labelEdge (e1,val)) = (the_ELabel_of G) +* (e1 .--> val) by Th32; then ( e2 in dom (the_ELabel_of G) or e2 in dom (e1 .--> val) ) by A2, FUNCT_4:12; then e2 in {e1} by A1; hence e1 = e2 by TARSKI:def_1; ::_thesis: e1 in the_Edges_of G thus e1 in the_Edges_of G by A1, A2, Def21; ::_thesis: verum end; theorem :: GLIB_003:49 for G being EVGraph for v, x being set holds G .labeledE() = (G .labelVertex (v,x)) .labeledE() by Th42; theorem :: GLIB_003:50 for G being EGraph for e, x being set st e in the_Edges_of G holds e in (G .labelEdge (e,x)) .labeledE() proof let G be EGraph; ::_thesis: for e, x being set st e in the_Edges_of G holds e in (G .labelEdge (e,x)) .labeledE() let e, x be set ; ::_thesis: ( e in the_Edges_of G implies e in (G .labelEdge (e,x)) .labeledE() ) assume e in the_Edges_of G ; ::_thesis: e in (G .labelEdge (e,x)) .labeledE() then A1: (G .labelEdge (e,x)) .labeledE() = (G .labeledE()) \/ {e} by Th45; e in {e} by TARSKI:def_1; hence e in (G .labelEdge (e,x)) .labeledE() by A1, XBOOLE_0:def_3; ::_thesis: verum end; theorem :: GLIB_003:51 for G1, G2 being VGraph st the_VLabel_of G1 = the_VLabel_of G2 holds G1 .labeledV() = G2 .labeledV() ; theorem Th52: :: GLIB_003:52 for G being VGraph for v, x being set st v in the_Vertices_of G holds (G .labelVertex (v,x)) .labeledV() = (G .labeledV()) \/ {v} proof let G be VGraph; ::_thesis: for v, x being set st v in the_Vertices_of G holds (G .labelVertex (v,x)) .labeledV() = (G .labeledV()) \/ {v} let e, val be set ; ::_thesis: ( e in the_Vertices_of G implies (G .labelVertex (e,val)) .labeledV() = (G .labeledV()) \/ {e} ) set G2 = G .labelVertex (e,val); set EG = the_VLabel_of G; set EG2 = the_VLabel_of (G .labelVertex (e,val)); assume e in the_Vertices_of G ; ::_thesis: (G .labelVertex (e,val)) .labeledV() = (G .labeledV()) \/ {e} then the_VLabel_of (G .labelVertex (e,val)) = (the_VLabel_of G) +* (e .--> val) by Th38; then dom (the_VLabel_of (G .labelVertex (e,val))) = (dom (the_VLabel_of G)) \/ (dom (e .--> val)) by FUNCT_4:def_1; hence (G .labelVertex (e,val)) .labeledV() = (G .labeledV()) \/ {e} by FUNCOP_1:13; ::_thesis: verum end; theorem :: GLIB_003:53 for G being VGraph for v, x being set st v in the_Vertices_of G holds G .labeledV() c= (G .labelVertex (v,x)) .labeledV() proof let G be VGraph; ::_thesis: for v, x being set st v in the_Vertices_of G holds G .labeledV() c= (G .labelVertex (v,x)) .labeledV() let e, x be set ; ::_thesis: ( e in the_Vertices_of G implies G .labeledV() c= (G .labelVertex (e,x)) .labeledV() ) assume e in the_Vertices_of G ; ::_thesis: G .labeledV() c= (G .labelVertex (e,x)) .labeledV() then (G .labelVertex (e,x)) .labeledV() = (G .labeledV()) \/ {e} by Th52; hence G .labeledV() c= (G .labelVertex (e,x)) .labeledV() by XBOOLE_1:7; ::_thesis: verum end; theorem :: GLIB_003:54 for G being finite VGraph for v, x being set st v in the_Vertices_of G & not v in G .labeledV() holds card ((G .labelVertex (v,x)) .labeledV()) = (card (G .labeledV())) + 1 proof let G be finite VGraph; ::_thesis: for v, x being set st v in the_Vertices_of G & not v in G .labeledV() holds card ((G .labelVertex (v,x)) .labeledV()) = (card (G .labeledV())) + 1 let e, val be set ; ::_thesis: ( e in the_Vertices_of G & not e in G .labeledV() implies card ((G .labelVertex (e,val)) .labeledV()) = (card (G .labeledV())) + 1 ) set G2 = G .labelVertex (e,val); set ECurr = the_VLabel_of G; set ENext = the_VLabel_of (G .labelVertex (e,val)); assume ( e in the_Vertices_of G & not e in G .labeledV() ) ; ::_thesis: card ((G .labelVertex (e,val)) .labeledV()) = (card (G .labeledV())) + 1 then A1: ( card ((dom (the_VLabel_of G)) \/ {e}) = (card (dom (the_VLabel_of G))) + 1 & the_VLabel_of (G .labelVertex (e,val)) = (the_VLabel_of G) +* (e .--> val) ) by Th38, CARD_2:41; dom (e .--> val) = {e} by FUNCOP_1:13; hence card ((G .labelVertex (e,val)) .labeledV()) = (card (G .labeledV())) + 1 by A1, FUNCT_4:def_1; ::_thesis: verum end; theorem :: GLIB_003:55 for G being VGraph for v1, v2, x being set st not v2 in G .labeledV() & v2 in (G .labelVertex (v1,x)) .labeledV() holds ( v1 = v2 & v1 in the_Vertices_of G ) proof let G be VGraph; ::_thesis: for v1, v2, x being set st not v2 in G .labeledV() & v2 in (G .labelVertex (v1,x)) .labeledV() holds ( v1 = v2 & v1 in the_Vertices_of G ) let e1, e2, val be set ; ::_thesis: ( not e2 in G .labeledV() & e2 in (G .labelVertex (e1,val)) .labeledV() implies ( e1 = e2 & e1 in the_Vertices_of G ) ) set Gn = G .labelVertex (e1,val); assume that A1: not e2 in G .labeledV() and A2: e2 in (G .labelVertex (e1,val)) .labeledV() ; ::_thesis: ( e1 = e2 & e1 in the_Vertices_of G ) e1 in the_Vertices_of G by A1, A2, Def22; then the_VLabel_of (G .labelVertex (e1,val)) = (the_VLabel_of G) +* (e1 .--> val) by Th38; then ( e2 in dom (the_VLabel_of G) or e2 in dom (e1 .--> val) ) by A2, FUNCT_4:12; then e2 in {e1} by A1; hence e1 = e2 by TARSKI:def_1; ::_thesis: e1 in the_Vertices_of G thus e1 in the_Vertices_of G by A1, A2, Def22; ::_thesis: verum end; theorem :: GLIB_003:56 for G being EVGraph for e, x being set holds G .labeledV() = (G .labelEdge (e,x)) .labeledV() by Th36; theorem :: GLIB_003:57 for G being VGraph for v being Vertex of G for x being set holds v in (G .labelVertex (v,x)) .labeledV() proof let G be VGraph; ::_thesis: for v being Vertex of G for x being set holds v in (G .labelVertex (v,x)) .labeledV() let v be Vertex of G; ::_thesis: for x being set holds v in (G .labelVertex (v,x)) .labeledV() let x be set ; ::_thesis: v in (G .labelVertex (v,x)) .labeledV() ( (G .labelVertex (v,x)) .labeledV() = (G .labeledV()) \/ {v} & v in {v} ) by Th52, TARSKI:def_1; hence v in (G .labelVertex (v,x)) .labeledV() by XBOOLE_0:def_3; ::_thesis: verum end;