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))) . e = x
let e, x be set ; :: thesis: ( e in the_Edges_of G implies (the_ELabel_of (G .labelEdge (e,x))) . e = x )
e in {e} by TARSKI:def 1;
then A1: e in dom (e .--> x) by FUNCOP_1:13;
assume e in the_Edges_of G ; :: thesis: (the_ELabel_of (G .labelEdge (e,x))) . e = x
then the_ELabel_of (G .labelEdge (e,x)) = (the_ELabel_of G) +* (e .--> x) by Th39;
then (the_ELabel_of (G .labelEdge (e,x))) . e = (e .--> x) . e by A1, FUNCT_4:13
.= x by FUNCOP_1:72 ;
hence (the_ELabel_of (G .labelEdge (e,x))) . e = x ; :: thesis: verum