let G be finite EGraph; :: thesis: 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 ; :: thesis: ( 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() ) ; :: thesis: 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 Th39, CARD_2:54;
dom (e .--> val) = {e} by FUNCOP_1:19;
hence card ((G .labelEdge e,val) .labeledE() ) = (card (G .labeledE() )) + 1 by A1, FUNCT_4:def 1; :: thesis: verum