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;

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 )
;

end;

suppose
dom (L `1) = the_Vertices_of G
; :: thesis: ( ( dom (L `1) = the_Vertices_of G implies ex b_{1} being Vertex of G st b_{1} = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b_{1} 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_{1} = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )

( 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

hence
( ( dom (L `1) = the_Vertices_of G implies ex b_{1} being Vertex of G st b_{1} = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b_{1} 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_{1} = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )
; :: thesis: verum

end;( 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

suppose A2:
dom (L `1) <> the_Vertices_of G
; :: thesis: ( ( dom (L `1) = the_Vertices_of G implies ex b_{1} being Vertex of G st b_{1} = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b_{1} 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_{1} = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )

( 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

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;

x is finite ;

A6: rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) c= rng (L `2) by RELAT_1:70;

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_{1}( finite Subset of NAT) -> Element of Bags NAT = ($1,1) -bag ;

set B = { H_{1}(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_{1}(x) where x is Element of S : x in S }
by A9;

A11: S is finite ;

A12: { H_{1}(x) where x is Element of S : x in S } is finite
from FRAENKEL:sch 21(A11);

_{1}(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 )

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_{1} being Vertex of G st b_{1} = the Element of the_Vertices_of G ) & ( not dom (L `1) = the_Vertices_of G implies ex b_{1} 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_{1} = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) ) )
; :: thesis: verum

end;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)))) = {}

A5:
for x being set st x in rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) holds 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;then the_Vertices_of G c= dom (L `1) by A3, XBOOLE_1:37;

hence contradiction by A2, XBOOLE_0:def 10; :: thesis: verum

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 )

then
for x being object 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

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;proof

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 ) )
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;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

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

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

set B = { H

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

A11: S is finite ;

A12: { H

now :: thesis: for x being object st x in { H_{1}(x) where x is Element of S : x in S } holds

x in Bags NAT

then reconsider B = { Hx in Bags NAT

let x be object ; :: thesis: ( x in { H_{1}(x) where x is Element of S : x in S } implies x in Bags NAT )

assume x in { H_{1}(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;assume x in { H

then ex y being Element of S st

( x = (y,1) -bag & y in S ) ;

hence x in Bags NAT ; :: thesis: verum

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

set mw = max (B,(InvLexOrder NAT));
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;( 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

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

( 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