let G be finite real-weighted WGraph; :: thesis: for V1 being non empty Subset of ()
for E1 being Subset of ()
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()) + (() . e) = G2 .cost()

let V1 be non empty Subset of (); :: thesis: for E1 being Subset of ()
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()) + (() . e) = G2 .cost()

let E1 be Subset of (); :: 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()) + (() . 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()) + (() . 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()) + (() . 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()) + (() . e) = G2 .cost() )
assume that
A1: not e in E1 and
A2: e in G .edgesBetween V1 ; :: thesis: (G1 .cost()) + (() . e) = G2 .cost()
{e} c= G .edgesBetween V1 by ;
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 () = E1 \/ {e} by PARTFUN1:def 2;
set W2 = e .--> (() . e);
A6: the_Edges_of G1 = E1 by GLIB_000:def 37;
then () \ () = {e} \ E1 by
.= {e} by ;
then reconsider W2 = e .--> (() . e) as ManySortedSet of () \ () ;
reconsider W2 = W2 as Rbag of () \ () ;
A7: the_Weight_of G1 = () | E1 by ;
A8: now :: thesis: for x being object st x in dom () holds
() . x = (() +* W2) . x
let x be object ; :: thesis: ( x in dom () implies () . x = (() +* W2) . x )
assume x in dom () ; :: thesis: () . x = (() +* W2) . x
then A9: x in E1 \/ {e} by A3;
the_Weight_of G2 = () | (E1 \/ {e}) by ;
then A10: (the_Weight_of G2) . x = () . x by ;
now :: thesis: (() +* W2) . x = () . x
per cases ( not x in dom W2 or x in dom W2 ) ;
suppose not x in dom W2 ; :: thesis: (() +* W2) . x = () . x
then ( ((the_Weight_of G1) +* W2) . x = () . x & x in E1 ) by ;
hence ((the_Weight_of G1) +* W2) . x = () . x by ; :: thesis: verum
end;
suppose A11: x in dom W2 ; :: thesis: (() +* W2) . x = () . x
then A12: x = e by TARSKI:def 1;
(() +* W2) . x = W2 . x by
.= () . e by ;
hence ((the_Weight_of G1) +* W2) . x = () . x by ; :: thesis: verum
end;
end;
end;
hence (the_Weight_of G2) . x = (() +* W2) . x ; :: thesis: verum
end;
dom W2 = {e} ;
then A13: Sum W2 = W2 . e by Th4
.= () . e by FUNCOP_1:72 ;
dom (() +* W2) = (dom ()) \/ (dom W2) by FUNCT_4:def 1
.= E1 \/ {e} by ;
hence (G1 .cost()) + (() . e) = G2 .cost() by ; :: thesis: verum