set V2G = L `2 ;
set VLG = L `1 ;
set f = (L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1);
for x being object st x in rng ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) holds
x in NAT
by ORDINAL1:def 12;
then A1:
rng ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) c= NAT
;
dom ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) = dom (L `2)
by Def3;
then
dom ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) = the_Vertices_of G
by FUNCT_2:def 1;
then
(L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1) is Function of (the_Vertices_of G),NAT
by A1, FUNCT_2:2;
then
(L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1) in Funcs ((the_Vertices_of G),NAT)
by FUNCT_2:8;
hence
[(L `1),((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1))] is MCS:Labeling of G
by ZFMISC_1:87; verum