set V2G = L `2 ;
set VLG = L `1 ;
set f = (L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1);

now

let x be set ; :: thesis: ( x in rng ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) implies x in NAT )
assume x in rng ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) ; :: thesis: x in NAT
then ex y being set st
( y in dom ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) & ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) . y = x ) by FUNCT_1:def 5;
hence x in NAT ; :: thesis: verum

end;

then A1: rng ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) c= NAT by TARSKI:def 3;
dom ((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1)) = dom (L `2) by Def4;
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:4;
then (L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1) in Funcs ((the_Vertices_of G),NAT) by FUNCT_2:11;
hence [(L `1),((L `2) .incSubset (((G .AdjacentSet {v}) \ (dom (L `1))),1))] is MCS:Labeling of G by ZFMISC_1:106; :: thesis: verum