set VG = the_Vertices_of G;
set V2G = L `2 ;
set VLG = L `1 ;
set F = (L `2) | ((the_Vertices_of G) \ (dom (L `1)));
set S = rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1))));
A1: ex f being Function st
( L `2 = f & dom f = the_Vertices_of G & rng f c= Fin NAT ) by FUNCT_2:def 2;

per cases ( dom (L `1) = the_Vertices_of G or dom (L `1) <> the_Vertices_of G ) ;

suppose dom (L `1) = the_Vertices_of G ; :: thesis: ( ( dom (L `1) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b₁ = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )

hence ( ( dom (L `1) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G st b<sub>1</sub> = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b₁ being Vertex of G ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b₁ = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) ) ; :: thesis: verum

end;

suppose A2: dom (L `1) <> the_Vertices_of G ; :: thesis: ( ( dom (L `1) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b₁ = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )

dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) = (dom (L `2)) /\ ((the_Vertices_of G) \ (dom (L `1))) by RELAT_1:61;
then A3: dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) = ((the_Vertices_of G) /\ (the_Vertices_of G)) \ (dom (L `1)) by A1, XBOOLE_1:49;

A4: now :: thesis: not dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) = {}

assume dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) = {} ; :: thesis: contradiction
then the_Vertices_of G c= dom (L `1) by A3, XBOOLE_1:37;
hence contradiction by A2, XBOOLE_0:def 10; :: thesis: verum

end;

A5: for x being set st x in rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) holds
x is finite ;
A6: rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) c= rng (L `2) by RELAT_1:70;

now :: thesis: for x being set st x in rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) holds
( x in bool NAT & x is finite )

A7: rng (L `2) c= bool NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (L `2) or x in bool NAT )
reconsider xx = x as set by TARSKI:1;
assume x in rng (L `2) ; :: thesis: x in bool NAT
then xx c= NAT by FINSUB_1:def 5;
hence x in bool NAT ; :: thesis: verum

end;

let x be set ; :: thesis: ( x in rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) implies ( x in bool NAT & x is finite ) )
assume A8: x in rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) ; :: thesis: ( x in bool NAT & x is finite )
x in rng (L `2) by A6, A8;
hence x in bool NAT by A7; :: thesis: x is finite
thus x is finite by A8; :: thesis: verum

end;

then for x being object st x in rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) holds
x in bool NAT ;
then reconsider S = rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) as non empty finite with_finite-elements Subset of (bool NAT) by A4, A5, FINSET_1:def 6, RELAT_1:42, TARSKI:def 3;
deffunc H₁( finite Subset of NAT) -> Element of Bags NAT = ($1,1) -bag ;
set B = { H₁(x) where x is Element of S : x in S } ;
consider z being object such that
A9: z in S by XBOOLE_0:def 1;
reconsider z = z as finite Subset of NAT by A9;
A10: (z,1) -bag in { H₁(x) where x is Element of S : x in S } by A9;
A11: S is finite ;
A12: { H₁(x) where x is Element of S : x in S } is finite from FRAENKEL:sch 21(A11);

now :: thesis: for x being object st x in { H₁(x) where x is Element of S : x in S } holds
x in Bags NAT

let x be object ; :: thesis: ( x in { H₁(x) where x is Element of S : x in S } implies x in Bags NAT )
assume x in { H₁(x) where x is Element of S : x in S } ; :: thesis: x in Bags NAT
then ex y being Element of S st
( x = (y,1) -bag & y in S ) ;
hence x in Bags NAT ; :: thesis: verum

end;

then reconsider B = { H₁(x) where x is Element of S : x in S } as non empty finite Subset of (Bags NAT) by A12, A10, TARSKI:def 3;
A13: for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag )

proof

let x be set ; :: thesis: ( x in B implies ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) )
assume x in B ; :: thesis: ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag )
then ex y being Element of S st
( x = (y,1) -bag & y in S ) ;
hence ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ; :: thesis: verum

end;

set mw = max (B,(InvLexOrder NAT));
max (B,(InvLexOrder NAT)) in B by Def4;
then consider y being finite Subset of NAT such that
A14: y in S and
A15: max (B,(InvLexOrder NAT)) = (y,1) -bag by A13;
set IT = the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(support (max (B,(InvLexOrder NAT))))};
y = support (max (B,(InvLexOrder NAT))) by A15, UPROOTS:8;
then not ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(support (max (B,(InvLexOrder NAT))))} is empty by A14, FUNCT_1:72;
then the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(support (max (B,(InvLexOrder NAT))))} in dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) by FUNCT_1:def 7;
then the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(support (max (B,(InvLexOrder NAT))))} in dom (L `2) by RELAT_1:57;
then reconsider IT = the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(support (max (B,(InvLexOrder NAT))))} as Vertex of G ;
for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ;
then ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & IT = the Element of F " {(support (max (B,(InvLexOrder NAT))))} & IT is Vertex of G ) by A13;
hence ( ( dom (L `1) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & b₁ = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) ) ; :: thesis: verum

end;

end;