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 A1: ( e in the_Vertices_of G & not e in G .labeledV() ) ; :: thesis: card ((G .labelVertex e,val) .labeledV() ) = (card (G .labeledV() )) + 1
then A2: card ((dom (the_VLabel_of G)) \/ {e}) = (card (dom (the_VLabel_of G))) + 1 by CARD_2:54;
A3: the_VLabel_of (G .labelVertex e,val) = (the_VLabel_of G) +* (e .--> val) by A1, Th45;
dom (e .--> val) = {e} by FUNCOP_1:19;
hence card ((G .labelVertex e,val) .labeledV() ) = (card (G .labeledV() )) + 1 by A2, A3, FUNCT_4:def 1; :: thesis: verum