let G be _finite EGraph; for e, x being set st e in the_Edges_of G & not e in G .labeledE() holds
card ((G .labelEdge (e,x)) .labeledE()) = (card (G .labeledE())) + 1
let e, val be set ; ( e in the_Edges_of G & not e in G .labeledE() implies card ((G .labelEdge (e,val)) .labeledE()) = (card (G .labeledE())) + 1 )
set G2 = G .labelEdge (e,val);
set ECurr = the_ELabel_of G;
set ENext = the_ELabel_of (G .labelEdge (e,val));
assume
( e in the_Edges_of G & not e in G .labeledE() )
; card ((G .labelEdge (e,val)) .labeledE()) = (card (G .labeledE())) + 1
then A1:
( card ((dom (the_ELabel_of G)) \/ {e}) = (card (dom (the_ELabel_of G))) + 1 & the_ELabel_of (G .labelEdge (e,val)) = (the_ELabel_of G) +* (e .--> val) )
by Th32, CARD_2:41;
dom (e .--> val) = {e}
;
hence
card ((G .labelEdge (e,val)) .labeledE()) = (card (G .labeledE())) + 1
by A1, FUNCT_4:def 1; verum