let G be _finite VGraph; :: thesis: for v, x being set st v in the_Vertices_of G & not v in G .labeledV() holds
card ((G .labelVertex (v,x)) .labeledV()) = (card (G .labeledV())) + 1
let e, val be set ; :: thesis: ( e in the_Vertices_of G & not e in G .labeledV() implies card ((G .labelVertex (e,val)) .labeledV()) = (card (G .labeledV())) + 1 )
set G2 = G .labelVertex (e,val);
set ECurr = the_VLabel_of G;
set ENext = the_VLabel_of (G .labelVertex (e,val));
assume ( e in the_Vertices_of G & not e in G .labeledV() ) ; :: thesis: card ((G .labelVertex (e,val)) .labeledV()) = (card (G .labeledV())) + 1
then A1: ( card ((dom (the_VLabel_of G)) \/ {e}) = (card (dom (the_VLabel_of G))) + 1 & the_VLabel_of (G .labelVertex (e,val)) = (the_VLabel_of G) +* (e .--> val) ) by Th38, CARD_2:41;
dom (e .--> val) = {e} ;
hence card ((G .labelVertex (e,val)) .labeledV()) = (card (G .labeledV())) + 1 by A1, FUNCT_4:def 1; :: thesis: verum