set VLG = L `1 ;
set V2G = L `2 ;
set f = (L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1;
set H = [(L `1 ),((L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1)];
dom ((L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1) = dom (L `2 ) by Def4;
then A2a: dom ((L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1) = the_Vertices_of G by FUNCT_2:def 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 consider y being set such that
y in dom ((L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1) and
A15: ((L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1) . y = x by FUNCT_1:def 5;
thus x in NAT by A15; :: thesis: verum

end;

then rng ((L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1) c= NAT by TARSKI:def 3;
then (L `2 ) .incSubset ((G .AdjacentSet {v}) \ (dom (L `1 ))),1 is Function of (the_Vertices_of G),NAT by A2a, 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