set V2G = L `2 ;
set VLG = L `1 ;
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)];

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