let G be EGraph; :: thesis: for e, x being set st e in the_Edges_of G holds
(G .labelEdge e,x) .labeledE() = (G .labeledE() ) \/ {e}
let e, val be set ; :: thesis: ( e in the_Edges_of G implies (G .labelEdge e,val) .labeledE() = (G .labeledE() ) \/ {e} )
set G2 = G .labelEdge e,val;
set EG = the_ELabel_of G;
set EG2 = the_ELabel_of (G .labelEdge e,val);
assume e in the_Edges_of G ; :: thesis: (G .labelEdge e,val) .labeledE() = (G .labeledE() ) \/ {e}
then the_ELabel_of (G .labelEdge e,val) = (the_ELabel_of G) +* (e .--> val) by Th39;
then dom (the_ELabel_of (G .labelEdge e,val)) = (dom (the_ELabel_of G)) \/ (dom (e .--> val)) by FUNCT_4:def 1;
hence (G .labelEdge e,val) .labeledE() = (G .labeledE() ) \/ {e} by FUNCOP_1:19; :: thesis: verum