let G be _finite real-weighted WGraph; :: thesis: for V1 being non empty Subset of (the_Vertices_of G)

for E1 being Subset of (G .edgesBetween V1)

for G1 being inducedWSubgraph of G,V1,E1

for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let V1 be non empty Subset of (the_Vertices_of G); :: thesis: for E1 being Subset of (G .edgesBetween V1)

for G1 being inducedWSubgraph of G,V1,E1

for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let E1 be Subset of (G .edgesBetween V1); :: thesis: for G1 being inducedWSubgraph of G,V1,E1

for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let G1 be inducedWSubgraph of G,V1,E1; :: thesis: for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let e be set ; :: thesis: for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let G2 be inducedWSubgraph of G,V1,E1 \/ {e}; :: thesis: ( not e in E1 & e in G .edgesBetween V1 implies (G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost() )

assume that

A1: not e in E1 and

A2: e in G .edgesBetween V1 ; :: thesis: (G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

{e} c= G .edgesBetween V1 by A2, ZFMISC_1:31;

then E1 \/ {e} c= G .edgesBetween V1 by XBOOLE_1:8;

then A3: the_Edges_of G2 = E1 \/ {e} by GLIB_000:def 37;

then A4: dom (the_Weight_of G2) = E1 \/ {e} by PARTFUN1:def 2;

set W2 = e .--> ((the_Weight_of G) . e);

A6: the_Edges_of G1 = E1 by GLIB_000:def 37;

then (the_Edges_of G2) \ (the_Edges_of G1) = {e} \ E1 by A3, XBOOLE_1:40

.= {e} by A1, ZFMISC_1:59 ;

then reconsider W2 = e .--> ((the_Weight_of G) . e) as ManySortedSet of (the_Edges_of G2) \ (the_Edges_of G1) ;

reconsider W2 = W2 as Rbag of (the_Edges_of G2) \ (the_Edges_of G1) ;

A7: the_Weight_of G1 = (the_Weight_of G) | E1 by A6, GLIB_003:def 10;

then A13: Sum W2 = W2 . e by Th4

.= (the_Weight_of G) . e by FUNCOP_1:72 ;

dom ((the_Weight_of G1) +* W2) = (dom (the_Weight_of G1)) \/ (dom W2) by FUNCT_4:def 1

.= E1 \/ {e} by A6, PARTFUN1:def 2 ;

hence (G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost() by A4, A8, A13, Th3, FUNCT_1:2; :: thesis: verum

for E1 being Subset of (G .edgesBetween V1)

for G1 being inducedWSubgraph of G,V1,E1

for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let V1 be non empty Subset of (the_Vertices_of G); :: thesis: for E1 being Subset of (G .edgesBetween V1)

for G1 being inducedWSubgraph of G,V1,E1

for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let E1 be Subset of (G .edgesBetween V1); :: thesis: for G1 being inducedWSubgraph of G,V1,E1

for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let G1 be inducedWSubgraph of G,V1,E1; :: thesis: for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let e be set ; :: thesis: for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

let G2 be inducedWSubgraph of G,V1,E1 \/ {e}; :: thesis: ( not e in E1 & e in G .edgesBetween V1 implies (G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost() )

assume that

A1: not e in E1 and

A2: e in G .edgesBetween V1 ; :: thesis: (G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

{e} c= G .edgesBetween V1 by A2, ZFMISC_1:31;

then E1 \/ {e} c= G .edgesBetween V1 by XBOOLE_1:8;

then A3: the_Edges_of G2 = E1 \/ {e} by GLIB_000:def 37;

then A4: dom (the_Weight_of G2) = E1 \/ {e} by PARTFUN1:def 2;

set W2 = e .--> ((the_Weight_of G) . e);

A6: the_Edges_of G1 = E1 by GLIB_000:def 37;

then (the_Edges_of G2) \ (the_Edges_of G1) = {e} \ E1 by A3, XBOOLE_1:40

.= {e} by A1, ZFMISC_1:59 ;

then reconsider W2 = e .--> ((the_Weight_of G) . e) as ManySortedSet of (the_Edges_of G2) \ (the_Edges_of G1) ;

reconsider W2 = W2 as Rbag of (the_Edges_of G2) \ (the_Edges_of G1) ;

A7: the_Weight_of G1 = (the_Weight_of G) | E1 by A6, GLIB_003:def 10;

A8: now :: thesis: for x being object st x in dom (the_Weight_of G2) holds

(the_Weight_of G2) . x = ((the_Weight_of G1) +* W2) . x

dom W2 = {e}
;(the_Weight_of G2) . x = ((the_Weight_of G1) +* W2) . x

let x be object ; :: thesis: ( x in dom (the_Weight_of G2) implies (the_Weight_of G2) . x = ((the_Weight_of G1) +* W2) . x )

assume x in dom (the_Weight_of G2) ; :: thesis: (the_Weight_of G2) . x = ((the_Weight_of G1) +* W2) . x

then A9: x in E1 \/ {e} by A3;

the_Weight_of G2 = (the_Weight_of G) | (E1 \/ {e}) by A3, GLIB_003:def 10;

then A10: (the_Weight_of G2) . x = (the_Weight_of G) . x by A9, FUNCT_1:49;

end;assume x in dom (the_Weight_of G2) ; :: thesis: (the_Weight_of G2) . x = ((the_Weight_of G1) +* W2) . x

then A9: x in E1 \/ {e} by A3;

the_Weight_of G2 = (the_Weight_of G) | (E1 \/ {e}) by A3, GLIB_003:def 10;

then A10: (the_Weight_of G2) . x = (the_Weight_of G) . x by A9, FUNCT_1:49;

now :: thesis: ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . xend;

hence
(the_Weight_of G2) . x = ((the_Weight_of G1) +* W2) . x
; :: thesis: verumper cases
( not x in dom W2 or x in dom W2 )
;

end;

suppose
not x in dom W2
; :: thesis: ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . x

then
( ((the_Weight_of G1) +* W2) . x = (the_Weight_of G1) . x & x in E1 )
by A9, FUNCT_4:11, XBOOLE_0:def 3;

hence ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . x by A7, A10, FUNCT_1:49; :: thesis: verum

end;hence ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . x by A7, A10, FUNCT_1:49; :: thesis: verum

suppose A11:
x in dom W2
; :: thesis: ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . x

then A12:
x = e
by TARSKI:def 1;

((the_Weight_of G1) +* W2) . x = W2 . x by A11, FUNCT_4:13

.= (the_Weight_of G) . e by A12, FUNCOP_1:72 ;

hence ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . x by A10, A11, TARSKI:def 1; :: thesis: verum

end;((the_Weight_of G1) +* W2) . x = W2 . x by A11, FUNCT_4:13

.= (the_Weight_of G) . e by A12, FUNCOP_1:72 ;

hence ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . x by A10, A11, TARSKI:def 1; :: thesis: verum

then A13: Sum W2 = W2 . e by Th4

.= (the_Weight_of G) . e by FUNCOP_1:72 ;

dom ((the_Weight_of G1) +* W2) = (dom (the_Weight_of G1)) \/ (dom W2) by FUNCT_4:def 1

.= E1 \/ {e} by A6, PARTFUN1:def 2 ;

hence (G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost() by A4, A8, A13, Th3, FUNCT_1:2; :: thesis: verum