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} by FUNCOP_1:19;
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 A3: rng ((L `1 ) +* (v .--> ((G .order() ) -' n))) c= NAT by A2, XBOOLE_1:1;
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 A4: (L `1 ) +* (v .--> ((G .order() ) -' n)) in PFuncs (the_Vertices_of G),NAT by A3, PARTFUN1:def 5;
{nn} in Fin NAT by FINSUB_1:def 5;
then A5: {{nn}} c= Fin NAT by ZFMISC_1:37;
consider f being Function such that
A6: L `2 = f and
A7: dom f = the_Vertices_of G and
A8: 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:19;
then A9: rng (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) c= Fin NAT by A5, XBOOLE_1:1;
A10: 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
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 5;
A13: 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 A6, Def2;
then A14: y = (f . x) \/ ((((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) . x) by A6, A11, A12, 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 A11, A13, XBOOLE_0:def 3;

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

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

end;

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

A20: f . x = {} by A18, FUNCT_1:def 4;
(((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) . x in rng (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)}) by A19, FUNCT_1:12;
hence y in Fin NAT by A9, A14, A20; :: thesis: verum

end;

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

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

end;

end;

end;

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;
then dom ((L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' n)})) = the_Vertices_of G by A6, A7, 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 A4, ZFMISC_1:def 2; :: thesis: verum