set VLG = L `1 ;
set V2G = L `2 ;
set VG = the_Vertices_of G;
set F = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )));
set S = rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 ))));
AAa: for x being set st x in rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) holds
x is finite ;
Add: 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 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₁ = 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 )))}) ) ) )

A3: ( dom ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) c= dom (L `2 ) & rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) c= rng (L `2 ) ) by RELAT_1:89, RELAT_1:99;
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 A6: dom ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) = ((the_Vertices_of G) /\ (the_Vertices_of G)) \ (dom (L `1 )) by Add, XBOOLE_1:49;

A7: now

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

end;

then A8: not rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) is empty by RELAT_1:65;

now

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 A10: x in rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) ; :: thesis: ( x in bool NAT & x is finite )
A11: x in rng (L `2 ) by A3, A10;
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;

hence x in bool NAT by A11; :: thesis: x is finite
thus x is finite by A10; :: thesis: verum

end;

then A12: for x being set st x in rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) holds
x in bool NAT ;
A13: for x being Element of rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) holds x is finite by A8, AAa;
reconsider S = rng ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) as non empty finite with_finite-elements Subset of (bool NAT ) by A7, A12, A13, Def1, FINSET_1:26, RELAT_1:65, TARSKI:def 3;
deffunc H₁( finite Subset of NAT ) -> Element of Bags NAT = $1,1 -bag ;
A14: S is finite ;
set B = { H₁(x) where x is Element of S : x in S } ;
A15: { H₁(x) where x is Element of S : x in S } is finite from FRAENKEL:sch 21(A14);
consider z being set such that
A16: z in S by XBOOLE_0:def 1;
reconsider z = z as finite Subset of NAT by A16;
A17: z,1 -bag in { H₁(x) where x is Element of S : x in S } by A16;

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 A18: x in { H₁(x) where x is Element of S : x in S } ; :: thesis: x in Bags NAT
consider y being Element of S such that
A19: ( x = y,1 -bag & y in S ) by A18;
thus x in Bags NAT by A19; :: 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 A15, A17, TARSKI:def 3;
A20: for x being finite Subset of NAT st x in S holds
x,1 -bag in B ;
A21: 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 A22: x in B ; :: thesis: ex y being finite Subset of NAT st
( y in S & x = y,1 -bag )
consider y being Element of S such that
A23: ( x = y,1 -bag & y in S ) by A22;
thus ex y being finite Subset of NAT st
( y in S & x = y,1 -bag ) by A23; :: thesis: verum

end;

set mw = max B,(InvLexOrder NAT );
set IT = choose (((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) " {(support (max B,(InvLexOrder NAT )))});
max B,(InvLexOrder NAT ) in B by Def5;
then consider y being finite Subset of NAT such that
A24: ( y in S & max B,(InvLexOrder NAT ) = y,1 -bag ) by A21;
y = support (max B,(InvLexOrder NAT )) by A24, UPROOTS:10;
then not ((L `2 ) | ((the_Vertices_of G) \ (dom (L `1 )))) " {(support (max B,(InvLexOrder NAT )))} is empty by A24, 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 ;
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 A20, A21;
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;