set k = (G .order() ) -' n;
set L1 = (L `1 ) +* (v .--> ((G .order() ) -' n));
A1: dom ((L `1 ) +* (v .--> ((G .order() ) -' n))) = (dom (L `1 )) \/ {v} by Lm2;
rng (v .--> ((G .order() ) -' n)) c= {((G .order() ) -' n)} by FUNCOP_1:19;
then rng (v .--> ((G .order() ) -' n)) c= NAT by XBOOLE_1:1;
then A2: (rng (L `1 )) \/ (rng (v .--> ((G .order() ) -' n))) c= NAT by XBOOLE_1:8;
rng ((L `1 ) +* (v .--> ((G .order() ) -' n))) c= (rng (L `1 )) \/ (rng (v .--> ((G .order() ) -' n))) by FUNCT_4:18;
then rng ((L `1 ) +* (v .--> ((G .order() ) -' n))) c= NAT by A2, XBOOLE_1:1;
then (L `1 ) +* (v .--> ((G .order() ) -' n)) in PFuncs (the_Vertices_of G),NAT by A1, PARTFUN1:def 5;
then reconsider M = [((L `1 ) +* (v .--> ((G .order() ) -' n))),(L `2 )] as MCS:Labeling of G by ZFMISC_1:106;
MCS:LabelAdjacent M,v is MCS:Labeling of G ;
hence ex b₁, M being MCS:Labeling of G st
( M = [((L `1 ) +* (v .--> ((G .order() ) -' n))),(L `2 )] & b₁ = MCS:LabelAdjacent M,v ) ; :: thesis: verum