let G1, G2 be _Graph; :: thesis: for G3 being removeLoops of G1

for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

let G4 be removeLoops of G2; :: thesis: for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

let F0 be one-to-one PGraphMapping of G1,G2; :: thesis: ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

reconsider F = G4 |` (F0 | G3) as one-to-one PGraphMapping of G3,G4 ;

take F ; :: thesis: ( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

A1: F _V = (the_Vertices_of G2) |` ((F0 | G3) _V) by GLIB_000:def 33

.= (F0 | G3) _V ;

F _E = (F0 | G3) _E by A10, RELAT_1:94;

hence A11: F = F0 | G3 by A1, XTUPLE_0:2; :: thesis: ( ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

thus ( F0 is total implies F is total ) :: thesis: ( ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

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

for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

let G4 be removeLoops of G2; :: thesis: for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

let F0 be one-to-one PGraphMapping of G1,G2; :: thesis: ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

reconsider F = G4 |` (F0 | G3) as one-to-one PGraphMapping of G3,G4 ;

take F ; :: thesis: ( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

A1: F _V = (the_Vertices_of G2) |` ((F0 | G3) _V) by GLIB_000:def 33

.= (F0 | G3) _V ;

now :: thesis: for y being object st y in rng ((F0 | G3) _E) holds

y in the_Edges_of G4

then A10:
rng ((F0 | G3) _E) c= the_Edges_of G4
by TARSKI:def 3;y in the_Edges_of G4

let y be object ; :: thesis: ( y in rng ((F0 | G3) _E) implies y in the_Edges_of G4 )

assume A2: y in rng ((F0 | G3) _E) ; :: thesis: y in the_Edges_of G4

not y in G2 .loops()

hence y in the_Edges_of G4 by GLIB_000:53; :: thesis: verum

end;assume A2: y in rng ((F0 | G3) _E) ; :: thesis: y in the_Edges_of G4

not y in G2 .loops()

proof

then
y in (the_Edges_of G2) \ (G2 .loops())
by A2, XBOOLE_0:def 5;
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

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

hence
not y in G2 .loops()
by GLIB_009:def 2; :: thesis: verum
given u being object such that A9:
y Joins u,u,G2
; :: thesis: contradiction

( (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: verum

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

hence y in the_Edges_of G4 by GLIB_000:53; :: thesis: verum

F _E = (F0 | G3) _E by A10, RELAT_1:94;

hence A11: F = F0 | G3 by A1, XTUPLE_0:2; :: thesis: ( ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

thus ( F0 is total implies F is total ) :: thesis: ( ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

proof

thus
( F0 is onto implies F is onto )
:: thesis: ( ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )
assume
F0 is total
; :: thesis: F is total

then F0 | G3 is total by Th57;

hence F is total by A11; :: thesis: verum

end;then F0 | G3 is total by Th57;

hence F is total by A11; :: thesis: verum

proof

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

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 ;

then the_Edges_of G4 = rng (F _E) by A11, XBOOLE_0:def 10;

hence F is onto by A13; :: thesis: verum

end;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: for y being object st y in the_Edges_of G4 holds

y in rng ((F0 | G3) _E)

then
the_Edges_of G4 c= rng ((F0 | G3) _E)
by TARSKI:def 3;y in rng ((F0 | G3) _E)

let y be object ; :: thesis: ( y in the_Edges_of G4 implies y in rng ((F0 | G3) _E) )

assume y in the_Edges_of G4 ; :: thesis: y in rng ((F0 | G3) _E)

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

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: verum

end;assume y in the_Edges_of G4 ; :: thesis: y in rng ((F0 | G3) _E)

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

then
not x in G1 .loops()
by GLIB_009:def 2;
let u be object ; :: thesis: not x Joins u,u,G1

assume x Joins u,u,G1 ; :: thesis: contradiction

then ( v1 = u & v2 = u ) by A19, GLIB_000:15;

hence contradiction by A20; :: thesis: verum

end;assume x Joins u,u,G1 ; :: thesis: contradiction

then ( v1 = u & v2 = u ) by A19, GLIB_000:15;

hence contradiction by A20; :: thesis: verum

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: verum

then the_Edges_of G4 = rng (F _E) by A11, XBOOLE_0:def 10;

hence F is onto by A13; :: thesis: verum

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