set F = ((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)};
reconsider nn = (G .order()) -' n as Element of NAT ;
set L2 = (L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)});
set f = v .--> ((G .order()) -' n);
set L1 = (L `1) +* (v .--> ((G .order()) -' n));
A1: dom (v .--> ((G .order()) -' n)) = {v} ;
A2: rng ((L `1) +* (v .--> ((G .order()) -' n))) c= NAT ;
dom ((L `1) +* (v .--> ((G .order()) -' n))) = (dom (L `1)) \/ (dom (v .--> ((G .order()) -' n))) by FUNCT_4:def 1;
then dom ((L `1) +* (v .--> ((G .order()) -' n))) c= the_Vertices_of G by A1, XBOOLE_1:8;
then A3: (L `1) +* (v .--> ((G .order()) -' n)) in PFuncs ((the_Vertices_of G),NAT) by A2, PARTFUN1:def 3;
{nn} in Fin NAT by FINSUB_1:def 5;
then A4: {{nn}} c= Fin NAT by ZFMISC_1:31;
consider f being Function such that
A5: L `2 = f and
A6: dom f = the_Vertices_of G and
A7: rng f c= Fin NAT by FUNCT_2:def 2;
rng (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) c= {{nn}} by FUNCOP_1:13;
then A8: rng (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) c= Fin NAT by A4;
A9: 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 A5, Def1;
A10: rng ((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)})) c= Fin NAT

proof

let y be object ; :: 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 object such that
A11: x in dom ((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)})) and
A12: y = ((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)})) . x by FUNCT_1:def 3;
A13: y = (f . x) \/ ((((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) . x) by A5, A11, A12, Def1, A9;

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 A11, A9, XBOOLE_0:def 3;

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

A16: (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) . x = {} by A15, FUNCT_1:def 2;
f . x in rng f by A14, FUNCT_1:3;
hence y in Fin NAT by A7, A13, A16; :: thesis: verum

end;

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

A19: f . x = {} by A17, FUNCT_1:def 2;
(((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) . x in rng (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) by A18, FUNCT_1:3;
hence y in Fin NAT by A8, A13, A19; :: thesis: verum

end;

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

A22: (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) . x in rng (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) by A21, FUNCT_1:3;
f . x in rng f by A20, FUNCT_1:3;
hence y in Fin NAT by A7, A8, A13, A22, FINSUB_1:def 1; :: thesis: verum

end;

end;

end;

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 A9;
then dom ((L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)})) = the_Vertices_of G by A6, XBOOLE_1:12;
then (L `2) .\/ (((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' n)}) in Funcs ((the_Vertices_of G),(Fin NAT)) by A10, 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 A3, ZFMISC_1:def 2; :: thesis: verum