let G be EGraph; :: thesis: for e, x being set st e in the_Edges_of G holds
the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x)
let e, x be set ; :: thesis: ( e in the_Edges_of G implies the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) )
assume e in the_Edges_of G ; :: thesis: the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x)
then the_ELabel_of (G .labelEdge (e,x)) = (G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x)))) . ELabelSelector by Def21;
hence the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) by GLIB_000:8; :: thesis: verum