let G be _finite VGraph; 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 ; ( 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() )
; 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; verum