set f = v .--> ((G .order() ) -' n);
set L1 = (L `1 ) +* (v .--> ((G .order() ) -' n));
set L2 = (L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)});
Aa: dom ((L `1 ) +* (v .--> ((G .order() ) -' n))) = (dom (L `1 )) \/ (dom (v .--> ((G .order() ) -' n))) by FUNCT_4:def 1;
dom (v .--> ((G .order() ) -' n)) = {v} by FUNCOP_1:19;
then Ad: dom ((L `1 ) +* (v .--> ((G .order() ) -' n))) c= the_Vertices_of G by Aa, XBOOLE_1:8;
Ae: rng ((L `1 ) +* (v .--> ((G .order() ) -' n))) c= (rng (L `1 )) \/ (rng (v .--> ((G .order() ) -' n))) by FUNCT_4:18;
Ag: rng (v .--> ((G .order() ) -' n)) c= {((G .order() ) -' n)} by FUNCOP_1:19;
reconsider nn = (G .order() ) -' n as Element of NAT ;
rng (v .--> ((G .order() ) -' n)) c= NAT by Ag, XBOOLE_1:1;
then (rng (L `1 )) \/ (rng (v .--> ((G .order() ) -' n))) c= NAT by XBOOLE_1:8;
then rng ((L `1 ) +* (v .--> ((G .order() ) -' n))) c= NAT by Ae, XBOOLE_1:1;
then A: (L `1 ) +* (v .--> ((G .order() ) -' n)) in PFuncs (the_Vertices_of G),NAT by Ad, PARTFUN1:def 5;
set F = ((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)};
Ba: dom ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) = (dom (L `2 )) \/ (dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) by Def2;
consider f being Function such that
Ca: L `2 = f and
Cb: dom f = the_Vertices_of G and
Cc: rng f c= Fin NAT by FUNCT_2:def 2;
Bd: dom ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) = the_Vertices_of G by Ba, Ca, Cb, XBOOLE_1:12;
Bg: rng (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) c= {{nn}} by FUNCOP_1:19;
{nn} in Fin NAT by FINSUB_1:def 5;
then {{nn}} c= Fin NAT by ZFMISC_1:37;
then Bh: rng (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) c= Fin NAT by Bg, XBOOLE_1:1;
rng ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) c= Fin NAT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) or y in Fin NAT )
assume y in rng ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) ; :: thesis: y in Fin NAT
then consider x being set such that
A1: x in dom ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) and
B1: y = ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) . x by FUNCT_1:def 5;
C1: dom ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) = (dom f) \/ (dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) by Ca, Def2;
D1: y = (f . x) \/ ((((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) . x) by A1, B1, C1, Ca, Def2;

per cases ( ( x in dom f & not x in dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) ) or ( not x in dom f & x in dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) ) or ( x in dom f & x in dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) ) ) by A1, C1, XBOOLE_0:def 3;

suppose that S1a: x in dom f and
S1b: not x in dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) ; :: thesis: y in Fin NAT

A2: f . x in rng f by S1a, FUNCT_1:12;
(((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) . x = {} by S1b, FUNCT_1:def 4;
hence y in Fin NAT by Cc, A2, D1; :: thesis: verum

end;

suppose that S1a: not x in dom f and
S1b: x in dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) ; :: thesis: y in Fin NAT

A2: (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) . x in rng (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) by S1b, FUNCT_1:12;
f . x = {} by S1a, FUNCT_1:def 4;
hence y in Fin NAT by Bh, A2, D1; :: thesis: verum

end;

suppose that S1a: x in dom f and
S1b: x in dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) ; :: thesis: y in Fin NAT

A2: f . x in rng f by S1a, FUNCT_1:12;
(((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) . x in rng (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) by S1b, FUNCT_1:12;
hence y in Fin NAT by Cc, A2, Bh, D1, FINSUB_1:def 1; :: thesis: verum

end;

end;

end;

then (L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) in Funcs (the_Vertices_of G),(Fin NAT ) by Bd, FUNCT_2:def 2;
hence [((L `1 ) +* (v .--> ((G .order() ) -' n))),((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}))] is LexBFS:Labeling of G by A, ZFMISC_1:def 2; :: thesis: verum