set V2G = L `2 ;
set VLG = L `1 ;
set f = (L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1);
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; :: thesis: verum