let G be EGraph; :: thesis: for e1, e2, x being set st e1 <> e2 holds
(the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2
let e1, e2, x be set ; :: thesis: ( e1 <> e2 implies (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 )
set G2 = G .labelEdge (e1,x);
assume A1: e1 <> e2 ; :: thesis: (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2

now :: thesis: (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2

per cases ( e1 in the_Edges_of G or not e1 in the_Edges_of G ) ;

suppose A2: e1 in the_Edges_of G ; :: thesis: (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2

not e2 in {e1} by A1, TARSKI:def 1;
then A3: not e2 in dom (e1 .--> x) ;
the_ELabel_of (G .labelEdge (e1,x)) = (the_ELabel_of G) +* (e1 .--> x) by A2, Th32;
hence (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 by A3, FUNCT_4:11; :: thesis: verum

end;

suppose not e1 in the_Edges_of G ; :: thesis: (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2

hence (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 by Def21; :: thesis: verum

end;

end;

end;

hence (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 ; :: thesis: verum