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 Th32;
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} ; :: thesis: verum