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: the_Edges_of G2 = (the_Edges_of G1) \ {e} by GLIB_000:54;
A3: the_Weight_of G2 = (the_Weight_of G1) | (the_Edges_of G2) by GLIB_003:def 10;
set b2 = e .--> ((the_Weight_of G1) . e);
A4: ( dom (e .--> ((the_Weight_of G1) . e)) = {e} & rng (e .--> ((the_Weight_of G1) . e)) = {((the_Weight_of G1) . e)} ) by FUNCOP_1:14, FUNCOP_1:19;
(the_Edges_of G1) \ (the_Edges_of G2) = (the_Edges_of G1) /\ {e} by A2, XBOOLE_1:48
.= {e} by A1, ZFMISC_1:52 ;
then reconsider b2 = e .--> ((the_Weight_of G1) . e) as ManySortedSet of ;
reconsider b2 = b2 as Rbag of ;
A5: dom ((the_Weight_of G2) +* b2) = (dom (the_Weight_of G2)) \/ {e} by A4, FUNCT_4:def 1
.= ((the_Edges_of G1) \ {e}) \/ {e} by A2, PARTFUN1:def 4
.= (the_Edges_of G1) \/ {e} by XBOOLE_1:39
.= the_Edges_of G1 by A1, ZFMISC_1:46 ;
A6: dom (the_Weight_of G1) = the_Edges_of G1 by PARTFUN1:def 4;

now

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

now

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 A4, A8, FUNCT_4:14
.= (the_Weight_of G1) . x by A9, FUNCOP_1:87 ;
:: thesis: verum

end;

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

then A11: ((the_Weight_of G2) +* b2) . x = (the_Weight_of G2) . x by A4, FUNCT_4:12;
x in (the_Edges_of G1) \ {e} by A7, A10, XBOOLE_0:def 5;
hence ((the_Weight_of G2) +* b2) . x = (the_Weight_of G1) . x by A2, A3, A11, FUNCT_1:72; :: thesis: verum

end;

end;

end;

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

end;

hence G1 .cost() = (G2 .cost() ) + (Sum b2) by Th3, A5, A6, FUNCT_1:9
.= (G2 .cost() ) + (b2 . e) by A4, Th4
.= (G2 .cost() ) + ((the_Weight_of G1) . e) by FUNCOP_1:87 ;
:: thesis: verum