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