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

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

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 natural-membered finite set ex F being Function st

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b_{1} = the Element of F " {(max S)} ) ) )

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & 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 natural-membered finite set ex F being Function st

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b_{1} = the Element of F " {(max S)} ) ) )
; :: thesis: verum

end;( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b

suppose A1:
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 natural-membered finite set ex F being Function st

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b_{1} = the Element of F " {(max S)} ) ) )

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b

A2:
dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) = (dom (L `2)) /\ ((the_Vertices_of G) \ (dom (L `1)))
by RELAT_1:61;

dom (L `2) = the_Vertices_of G by FUNCT_2:def 1;

then A3: 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;

set y = max S;

set IT = the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)};

max S in S by XXREAL_2:def 8;

then not ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)} is empty by FUNCT_1:72;

then the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)} 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)))) " {(max S)} in dom (L `2) by RELAT_1:57;

then reconsider IT = the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)} as Vertex of G ;

ex S being non empty natural-membered finite set ex F being Function st

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & IT = the Element of F " {(max S)} & IT is Vertex of G ) ;

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 natural-membered finite set ex F being Function st

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b_{1} = the Element of F " {(max S)} ) ) )
; :: thesis: verum

end;dom (L `2) = the_Vertices_of G by FUNCT_2:def 1;

then A3: 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;

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

then reconsider S = rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) as non empty natural-membered finite set by RELAT_1:42;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 A1, XBOOLE_0:def 10; :: thesis: verum

end;then the_Vertices_of G c= dom (L `1) by A3, XBOOLE_1:37;

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

set y = max S;

set IT = the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)};

max S in S by XXREAL_2:def 8;

then not ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)} is empty by FUNCT_1:72;

then the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)} 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)))) " {(max S)} in dom (L `2) by RELAT_1:57;

then reconsider IT = the Element of ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)} as Vertex of G ;

ex S being non empty natural-membered finite set ex F being Function st

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & IT = the Element of F " {(max S)} & IT is Vertex of G ) ;

hence ( ( dom (L `1) = the_Vertices_of G implies ex b

( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b