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: for x being set st x in rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) holds
x is finite ;
A2: 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₁ = choose (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₁ = choose (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> = choose (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₁ = choose (F " {(support (max B,(InvLexOrder NAT )))}) ) ) ) ; :: thesis: verum

end;

suppose A3: dom (L `1 ) <> the_Vertices_of G ; :: thesis: ( ( dom (L `1 ) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = choose (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₁ = choose (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:90;
then A4: dom ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) = ((the_Vertices_of G) /\ (the_Vertices_of G)) \ (dom (L `1 )) by A2, XBOOLE_1:49;

A5: now

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

end;

then not rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) is empty by RELAT_1:65;
then A6: for x being Element of rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) holds x is finite by A1;
A7: rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) c= rng (L `2 ) by RELAT_1:99;

now

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (L `2 ) or x in bool NAT )
assume x in rng (L `2 ) ; :: thesis: x in bool NAT
then x 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 A9: 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 A7, A9;
hence x in bool NAT by A8; :: thesis: x is finite
thus x is finite by A9; :: thesis: verum

end;

then for x being set 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 A5, A6, Def1, FINSET_1:26, RELAT_1:65, 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 set such that
A10: z in S by XBOOLE_0:def 1;
reconsider z = z as finite Subset of NAT by A10;
A11: z,1 -bag in { H₁(x) where x is Element of S : x in S } by A10;
A12: S is finite ;
A13: { H₁(x) where x is Element of S : x in S } is finite from FRAENKEL:sch 21(A12);

now

let x be set ; :: 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 A13, A11, TARSKI:def 3;
A14: 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 Def5;
then consider y being finite Subset of NAT such that
A15: y in S and
A16: max B,(InvLexOrder NAT ) = y,1 -bag by A14;
set IT = choose (((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) " {(support (max B,(InvLexOrder NAT )))});
y = support (max B,(InvLexOrder NAT )) by A16, UPROOTS:10;
then not ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) " {(support (max B,(InvLexOrder NAT )))} is empty by A15, FUNCT_1:142;
then choose (((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 13;
then reconsider IT = choose (((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 = choose (F " {(support (max B,(InvLexOrder NAT )))}) & IT is Vertex of G ) by A14;
hence ( ( dom (L `1 ) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G st b<sub>1</sub> = choose (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₁ = choose (F " {(support (max B,(InvLexOrder NAT )))}) ) ) ) ; :: thesis: verum

end;

end;