let G1 be _finite real-weighted WGraph; :: thesis: for e being set
for G2 being [Weighted] weight-inheriting removeEdge of G1,e st e in the_Edges_of G1 holds
G1 .cost() = (G2 .cost()) + ((the_Weight_of G1) . e)
let e be set ; :: thesis: for G2 being [Weighted] weight-inheriting removeEdge of G1,e st e in the_Edges_of G1 holds
G1 .cost() = (G2 .cost()) + ((the_Weight_of G1) . e)
let G2 be [Weighted] weight-inheriting removeEdge of G1,e; :: thesis: ( e in the_Edges_of G1 implies G1 .cost() = (G2 .cost()) + ((the_Weight_of G1) . e) )
set EG1 = the_Edges_of G1;
set EG2 = the_Edges_of G2;
assume A1: e in the_Edges_of G1 ; :: thesis: G1 .cost() = (G2 .cost()) + ((the_Weight_of G1) . e)
A2: dom (the_Weight_of G1) = the_Edges_of G1 by PARTFUN1:def 2;
set b2 = e .--> ((the_Weight_of G1) . e);
A3: dom (e .--> ((the_Weight_of G1) . e)) = {e} ;
A4: the_Edges_of G2 = (the_Edges_of G1) \ {e} by GLIB_000:51;
then (the_Edges_of G1) \ (the_Edges_of G2) = (the_Edges_of G1) /\ {e} by XBOOLE_1:48
.= {e} by A1, ZFMISC_1:46 ;
then reconsider b2 = e .--> ((the_Weight_of G1) . e) as ManySortedSet of (the_Edges_of G1) \ (the_Edges_of G2) ;
reconsider b2 = b2 as Rbag of (the_Edges_of G1) \ (the_Edges_of G2) ;
A5: the_Weight_of G2 = (the_Weight_of G1) | (the_Edges_of G2) by GLIB_003:def 10;

A6: now :: thesis: for x being object st x in dom (the_Weight_of G1) holds
(the_Weight_of G1) . x = ((the_Weight_of G2) +* b2) . x

let x be object ; :: thesis: ( x in dom (the_Weight_of G1) implies (the_Weight_of G1) . x = ((the_Weight_of G2) +* b2) . x )
assume x in dom (the_Weight_of G1) ; :: thesis: (the_Weight_of G1) . x = ((the_Weight_of G2) +* b2) . x
then A7: x in the_Edges_of G1 ;

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

per cases ( x in {e} or not x in {e} ) ;

suppose A8: x in {e} ; :: thesis: ((the_Weight_of G2) +* b2) . x = (the_Weight_of G1) . x

then A9: x = e by TARSKI:def 1;
hence ((the_Weight_of G2) +* b2) . x = b2 . e by A3, A8, FUNCT_4:13
.= (the_Weight_of G1) . x by A9, FUNCOP_1:72 ;
:: thesis: verum

end;

suppose not x in {e} ; :: thesis: ((the_Weight_of G2) +* b2) . x = (the_Weight_of G1) . x

then ( ((the_Weight_of G2) +* b2) . x = (the_Weight_of G2) . x & x in (the_Edges_of G1) \ {e} ) by A3, A7, FUNCT_4:11, XBOOLE_0:def 5;
hence ((the_Weight_of G2) +* b2) . x = (the_Weight_of G1) . x by A4, A5, FUNCT_1:49; :: thesis: verum

end;

end;

end;

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

end;

dom ((the_Weight_of G2) +* b2) = (dom (the_Weight_of G2)) \/ {e} by A3, FUNCT_4:def 1
.= ((the_Edges_of G1) \ {e}) \/ {e} by A4, PARTFUN1:def 2
.= (the_Edges_of G1) \/ {e} by XBOOLE_1:39
.= the_Edges_of G1 by A1, ZFMISC_1:40 ;
hence G1 .cost() = (G2 .cost()) + (Sum b2) by A2, A6, Th3, FUNCT_1:2
.= (G2 .cost()) + (b2 . e) by A3, Th4
.= (G2 .cost()) + ((the_Weight_of G1) . e) by FUNCOP_1:72 ;
:: thesis: verum