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;

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

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;

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

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

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;

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;

end;

end;

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

end;

dom W2 = {e} ;
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