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 A1: ( not e in E1 & e in G .edgesBetween V1 ) ; :: thesis: (G1 .cost() ) + ((the_Weight_of G) . e) = G2 .cost()
A2: ( the_Vertices_of G1 = V1 & the_Edges_of G1 = E1 ) by GLIB_000:def 39;
{e} c= G .edgesBetween V1 by A1, ZFMISC_1:37;
then E1 \/ {e} c= G .edgesBetween V1 by XBOOLE_1:8;
then A3: ( the_Vertices_of G2 = V1 & the_Edges_of G2 = E1 \/ {e} ) by GLIB_000:def 39;
set W2 = e .--> ((the_Weight_of G) . e);
A4: (the_Edges_of G2) \ (the_Edges_of G1) = {e} \ E1 by A2, A3, XBOOLE_1:40
.= {e} by A1, ZFMISC_1:67 ;
A5: dom (e .--> ((the_Weight_of G) . e)) = {e} by FUNCOP_1:19;
reconsider W2 = e .--> ((the_Weight_of G) . e) as ManySortedSet of by A4;
reconsider W2 = W2 as Rbag of ;
A6: dom (the_Weight_of G2) = E1 \/ {e} by A3, PARTFUN1:def 4;
A7: dom ((the_Weight_of G1) +* W2) = (dom (the_Weight_of G1)) \/ (dom W2) by FUNCT_4:def 1
.= E1 \/ {e} by A2, A5, PARTFUN1:def 4 ;
A8: the_Weight_of G1 = (the_Weight_of G) | E1 by A2, GLIB_003:def 10;

A8a: now

let x be set ; :: 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, PARTFUN1:def 4;
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:72;

now

per cases ( not x in dom W2 or x in dom W2 ) ;

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

then A12: ((the_Weight_of G1) +* W2) . x = (the_Weight_of G1) . x by FUNCT_4:12;
x in E1 by A5, A9, A11, XBOOLE_0:def 3;
hence ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . x by A8, A10, A12, FUNCT_1:72; :: thesis: verum

end;

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

then A14: x = e by A5, TARSKI:def 1;
((the_Weight_of G1) +* W2) . x = W2 . x by A13, FUNCT_4:14
.= (the_Weight_of G) . e by A14, FUNCOP_1:87 ;
hence ((the_Weight_of G1) +* W2) . x = (the_Weight_of G2) . x by A5, A10, A13, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence (the_Weight_of G2) . x = ((the_Weight_of G1) +* W2) . x ; :: thesis: verum

end;

dom W2 = {e} by FUNCOP_1:19;
then Sum W2 = W2 . e by Th4
.= (the_Weight_of G) . e by FUNCOP_1:87 ;
hence (G1 .cost() ) + ((the_Weight_of G) . e) = G2 .cost() by Th3, A8a, A6, A7, FUNCT_1:9; :: thesis: verum