let G1, G2 be _Graph; :: thesis:
let G3 be removeLoops of G1; :: thesis:
let G4 be removeLoops of G2; :: thesis:
let F0 be one-to-one PGraphMapping of G1,G2; :: thesis:
reconsider F = G4 |` (F0 | G3) as one-to-one PGraphMapping of G3,G4 ;
take F ; :: thesis:
A1: F _V = (the_Vertices_of G2) |` ((F0 | G3) _V) by GLIB_000:def 33
.= (F0 | G3) _V ;

now :: thesis:

let y be object ; :: thesis:
assume A2: y in rng ((F0 | G3) _E) ; :: thesis:
not y in G2 .loops()

proof

consider x being object such that
A3: ( x in dom ((F0 _E) | (the_Edges_of G3)) & ((F0 _E) | (the_Edges_of G3)) . x = y ) by A2, FUNCT_1:def 3;
A4: ( x in dom (F0 _E) & x in the_Edges_of G3 ) by A3, RELAT_1:57;
set v = (the_Source_of G1) . x;
set w = (the_Target_of G1) . x;
A5: ( (the_Source_of G1) . x in dom (F0 _V) & (the_Target_of G1) . x in dom (F0 _V) ) by A4, Th5;
A6: ( x Joins (the_Source_of G1) . x,(the_Target_of G1) . x,G1 & (F0 _E) . x = y ) by A3, A4, GLIB_000:def 13, FUNCT_1:49;
then A7: y Joins (F0 _V) . ((the_Source_of G1) . x),(F0 _V) . ((the_Target_of G1) . x),G2 by A4, A5, Th4;
x in (the_Edges_of G1) \ (G1 .loops()) by A4, GLIB_000:53;
then not x in G1 .loops() by XBOOLE_0:def 5;
then (the_Source_of G1) . x <> (the_Target_of G1) . x by A6, GLIB_009:def 2;
then A8: (F0 _V) . ((the_Source_of G1) . x) <> (F0 _V) . ((the_Target_of G1) . x) by A5, FUNCT_1:def 4;
for u being object holds not y Joins u,u,G2

proof

given u being object such that A9: y Joins u,u,G2 ; :: thesis:
( (F0 _V) . ((the_Source_of G1) . x) = u & (F0 _V) . ((the_Target_of G1) . x) = u ) by A7, A9, GLIB_000:15;
hence contradiction by A8; :: thesis:

end;

hence not y in G2 .loops() by GLIB_009:def 2; :: thesis:

end;

then y in (the_Edges_of G2) \ (G2 .loops()) by A2, XBOOLE_0:def 5;
hence y in the_Edges_of G4 by GLIB_000:53; :: thesis:

end;

then A10: rng ((F0 | G3) _E) c= the_Edges_of G4 by TARSKI:def 3;
F _E = (F0 | G3) _E by A10, RELAT_1:94;
hence A11: F = F0 | G3 by A1, XTUPLE_0:2; :: thesis:
thus ( F0 is total implies F is total ) :: thesis:

proof

assume F0 is total ; :: thesis:
then F0 | G3 is total by Th57;
hence F is total by A11; :: thesis:

end;

thus ( F0 is onto implies F is onto ) :: thesis:

proof

assume F0 is onto ; :: thesis:
then A12: ( rng (F0 _V) = the_Vertices_of G2 & rng (F0 _E) = the_Edges_of G2 ) ;
A13: rng (F _V) = rng ((F0 | G3) _V) by A1
.= rng ((F0 _V) | (the_Vertices_of G1)) by GLIB_000:def 33
.= the_Vertices_of G4 by A12, GLIB_000:def 33 ;

now :: thesis:

let y be object ; :: thesis:
assume y in the_Edges_of G4 ; :: thesis:
then y in (the_Edges_of G2) \ (G2 .loops()) by GLIB_000:53;
then A14: ( y in rng (F0 _E) & not y in G2 .loops() ) by A12, XBOOLE_0:def 5;
set w1 = (the_Source_of G2) . y;
set w2 = (the_Target_of G2) . y;
(the_Source_of G2) . y in rng (F0 _V) by A14, Th6;
then consider v1 being object such that
A15: ( v1 in dom (F0 _V) & (F0 _V) . v1 = (the_Source_of G2) . y ) by FUNCT_1:def 3;
(the_Target_of G2) . y in rng (F0 _V) by A14, Th6;
then consider v2 being object such that
A16: ( v2 in dom (F0 _V) & (F0 _V) . v2 = (the_Target_of G2) . y ) by FUNCT_1:def 3;
consider x being object such that
A17: ( x in dom (F0 _E) & (F0 _E) . x = y ) by A14, FUNCT_1:def 3;
A18: y Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 by A14, GLIB_000:def 13;
then A19: x Joins v1,v2,G1 by A15, A16, A17, Def15;
A20: v1 <> v2 by A14, A15, A16, A18, GLIB_009:def 2;
for u being object holds not x Joins u,u,G1

proof

let u be object ; :: thesis:
assume x Joins u,u,G1 ; :: thesis:
then ( v1 = u & v2 = u ) by A19, GLIB_000:15;
hence contradiction by A20; :: thesis:

end;

then not x in G1 .loops() by GLIB_009:def 2;
then x in (the_Edges_of G1) \ (G1 .loops()) by A17, XBOOLE_0:def 5;
then x in the_Edges_of G3 by GLIB_000:53;
then A21: x in dom ((F0 | G3) _E) by A17, RELAT_1:57;
then ((F0 | G3) _E) . x = y by A17, FUNCT_1:47;
hence y in rng ((F0 | G3) _E) by A21, FUNCT_1:3; :: thesis:

end;

then the_Edges_of G4 c= rng ((F0 | G3) _E) by TARSKI:def 3;
then the_Edges_of G4 = rng (F _E) by A11, XBOOLE_0:def 10;
hence F is onto by A13; :: thesis:

end;

thus ( F0 is directed implies F is directed ) ; :: thesis:
thus ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) ; :: thesis: