let G3, G4 be _Graph; :: thesis: for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2
for F0 being PGraphMapping of G3,G4
for f being one-to-one Function st dom f = V1 \ () & rng f = V2 \ () holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let V1, V2 be set ; :: thesis: for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2
for F0 being PGraphMapping of G3,G4
for f being one-to-one Function st dom f = V1 \ () & rng f = V2 \ () holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let G1 be addVertices of G3,V1; :: thesis: for G2 being addVertices of G4,V2
for F0 being PGraphMapping of G3,G4
for f being one-to-one Function st dom f = V1 \ () & rng f = V2 \ () holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let G2 be addVertices of G4,V2; :: thesis: for F0 being PGraphMapping of G3,G4
for f being one-to-one Function st dom f = V1 \ () & rng f = V2 \ () holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let F0 be PGraphMapping of G3,G4; :: thesis: for f being one-to-one Function st dom f = V1 \ () & rng f = V2 \ () holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let f be one-to-one Function; :: thesis: ( dom f = V1 \ () & rng f = V2 \ () implies ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) ) )

assume A1: ( dom f = V1 \ () & rng f = V2 \ () ) ; :: thesis: ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

set h = (F0 _V) +* f;
A2: dom ((F0 _V) +* f) = (dom (F0 _V)) \/ (V1 \ ()) by ;
dom ((F0 _V) +* f) c= () \/ V1 by ;
then A3: dom ((F0 _V) +* f) c= the_Vertices_of G1 by GLIB_006:def 10;
(rng (F0 _V)) \/ (rng f) c= () \/ V2 by ;
then A4: (rng (F0 _V)) \/ (rng f) c= the_Vertices_of G2 by GLIB_006:def 10;
rng ((F0 _V) +* f) c= (rng (F0 _V)) \/ (rng f) by FUNCT_4:17;
then rng ((F0 _V) +* f) c= the_Vertices_of G2 by ;
then reconsider h = (F0 _V) +* f as PartFunc of (),() by ;
( the_Edges_of G1 = the_Edges_of G3 & the_Edges_of G2 = the_Edges_of G4 ) by GLIB_006:def 10;
then reconsider g = F0 _E as PartFunc of (),() ;
A5: (dom f) /\ () = {} by ;
(dom (F0 _V)) /\ (dom f) c= (dom f) /\ () by XBOOLE_1:26;
then A6: dom (F0 _V) misses dom f by ;
A7: (rng f) /\ () = {} by ;
(rng (F0 _V)) /\ (rng f) c= (rng f) /\ () by XBOOLE_1:26;
then A8: rng (F0 _V) misses rng f by ;
A9: (dom h) /\ () = ((dom (F0 _V)) \/ (dom f)) /\ () by FUNCT_4:def 1
.= ((dom (F0 _V)) /\ ()) \/ ((dom f) /\ ()) by XBOOLE_1:23
.= dom (F0 _V) by ;
now :: thesis: ( ( for e being object st e in dom g holds
( () . e in dom h & () . e in dom h ) ) & ( for e, v, w being object st e in dom g & v in dom h & w in dom h & e Joins v,w,G1 holds
g . e Joins h . v,h . w,G2 ) )
hereby :: thesis: for e, v, w being object st e in dom g & v in dom h & w in dom h & e Joins v,w,G1 holds
g . e Joins h . v,h . w,G2
let e be object ; :: thesis: ( e in dom g implies ( () . e in dom h & () . e in dom h ) )
assume A10: e in dom g ; :: thesis: ( () . e in dom h & () . e in dom h )
( (the_Source_of G1) . e = () . e & () . e = () . e ) by GLIB_006:def 10;
then A11: ( (the_Source_of G1) . e in dom (F0 _V) & () . e in dom (F0 _V) ) by ;
dom (F0 _V) c= dom h by FUNCT_4:10;
hence ( (the_Source_of G1) . e in dom h & () . e in dom h ) by A11; :: thesis: verum
end;
let e, v, w be object ; :: thesis: ( e in dom g & v in dom h & w in dom h & e Joins v,w,G1 implies g . e Joins h . v,h . w,G2 )
assume A12: ( e in dom g & v in dom h & w in dom h & e Joins v,w,G1 ) ; :: thesis: g . e Joins h . v,h . w,G2
A13: e Joins v,w,G3 by ;
then A14: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by GLIB_000:13;
then ( v in dom (F0 _V) & w in dom (F0 _V) ) by ;
then (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by ;
then A15: g . e Joins (F0 _V) . v,(F0 _V) . w,G2 by GLIB_009:41;
( not v in dom f & not w in dom f ) by ;
then ( h . v = (F0 _V) . v & h . w = (F0 _V) . w ) by FUNCT_4:11;
hence g . e Joins h . v,h . w,G2 by A15; :: thesis: verum
end;
then reconsider F = [h,g] as PGraphMapping of G1,G2 by Th8;
take F ; :: thesis: ( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
thus F = [((F0 _V) +* f),(F0 _E)] ; :: thesis: ( ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
thus ( not F0 is empty implies not F is empty ) by ; :: thesis: ( ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
thus ( F0 is total implies F is total ) :: thesis: ( ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
proof
assume F0 is total ; :: thesis: F is total
then A16: ( dom (F0 _V) = the_Vertices_of G3 & dom (F0 _E) = the_Edges_of G3 ) ;
then dom h = () \/ (V1 \ ()) by
.= () \/ V1 by XBOOLE_1:39
.= the_Vertices_of G1 by GLIB_006:def 10 ;
hence F is total by ; :: thesis: verum
end;
thus ( F0 is onto implies F is onto ) :: thesis: ( ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
proof
assume F0 is onto ; :: thesis: F is onto
then A17: ( rng (F0 _V) = the_Vertices_of G4 & rng (F0 _E) = the_Edges_of G4 ) ;
rng h = (rng (F0 _V)) \/ (rng f) by
.= () \/ V2 by
.= the_Vertices_of G2 by GLIB_006:def 10 ;
hence F is onto by ; :: thesis: verum
end;
thus ( F0 is one-to-one implies F is one-to-one ) by ; :: thesis: ( ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
thus ( F0 is directed implies F is directed ) :: thesis: ( ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
proof
assume A18: F0 is directed ; :: thesis: F is directed
now :: thesis: for e, v, w being object st e in dom g & v in dom h & w in dom h & e DJoins v,w,G1 holds
g . e DJoins h . v,h . w,G2
let e, v, w be object ; :: thesis: ( e in dom g & v in dom h & w in dom h & e DJoins v,w,G1 implies g . e DJoins h . v,h . w,G2 )
assume A19: ( e in dom g & v in dom h & w in dom h & e DJoins v,w,G1 ) ; :: thesis: g . e DJoins h . v,h . w,G2
A20: e DJoins v,w,G3 by ;
then e Joins v,w,G3 by GLIB_000:16;
then A21: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by GLIB_000:13;
then ( v in dom (F0 _V) & w in dom (F0 _V) ) by ;
then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G4 by ;
then A22: g . e DJoins (F0 _V) . v,(F0 _V) . w,G2 by GLIB_009:41;
( not v in dom f & not w in dom f ) by ;
then ( h . v = (F0 _V) . v & h . w = (F0 _V) . w ) by FUNCT_4:11;
hence g . e DJoins h . v,h . w,G2 by A22; :: thesis: verum
end;
hence F is directed ; :: thesis: verum
end;
thus ( F0 is semi-continuous implies F is semi-continuous ) :: thesis: ( ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
proof
assume A23: F0 is semi-continuous ; :: thesis:
now :: thesis: for e, v, w being object st e in dom g & v in dom h & w in dom h & g . e Joins h . v,h . w,G2 holds
e Joins v,w,G1
let e, v, w be object ; :: thesis: ( e in dom g & v in dom h & w in dom h & g . e Joins h . v,h . w,G2 implies e Joins v,w,G1 )
assume A24: ( e in dom g & v in dom h & w in dom h & g . e Joins h . v,h . w,G2 ) ; :: thesis: e Joins v,w,G1
then A25: (F0 _E) . e Joins h . v,h . w,G4 by GLIB_009:41;
then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;
then A26: ( not h . v in rng f & not h . w in rng f ) by ;
A27: ( not v in dom f & not w in dom f )
proof
assume ( v in dom f or w in dom f ) ; :: thesis: contradiction
per cases then ( v in dom f or w in dom f ) ;
suppose v in dom f ; :: thesis: contradiction
then ( f . v in rng f & h . v = f . v ) by ;
hence contradiction by A26; :: thesis: verum
end;
suppose w in dom f ; :: thesis: contradiction
then ( f . w in rng f & h . w = f . w ) by ;
hence contradiction by A26; :: thesis: verum
end;
end;
end;
( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) ) by ;
then A28: ( v in dom (F0 _V) & w in dom (F0 _V) ) by ;
( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by ;
then (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by A25;
then A29: e Joins v,w,G3 by ;
( v is set & w is set ) by TARSKI:1;
hence e Joins v,w,G1 by ; :: thesis: verum
end;
hence F is semi-continuous ; :: thesis: verum
end;
thus ( F0 is continuous implies F is continuous ) :: thesis: ( ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
proof
assume A30: F0 is continuous ; :: thesis: F is continuous
now :: thesis: for e9, v, w being object st v in dom h & w in dom h & e9 Joins h . v,h . w,G2 holds
ex e being object st
( e Joins v,w,G1 & e in dom g & g . e = e9 )
let e9, v, w be object ; :: thesis: ( v in dom h & w in dom h & e9 Joins h . v,h . w,G2 implies ex e being object st
( e Joins v,w,G1 & e in dom g & g . e = e9 ) )

assume A31: ( v in dom h & w in dom h & e9 Joins h . v,h . w,G2 ) ; :: thesis: ex e being object st
( e Joins v,w,G1 & e in dom g & g . e = e9 )

then A32: e9 Joins h . v,h . w,G4 by GLIB_009:41;
then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;
then A33: ( not h . v in rng f & not h . w in rng f ) by ;
A34: ( not v in dom f & not w in dom f )
proof
assume ( v in dom f or w in dom f ) ; :: thesis: contradiction
per cases then ( v in dom f or w in dom f ) ;
suppose v in dom f ; :: thesis: contradiction
then ( f . v in rng f & h . v = f . v ) by ;
hence contradiction by A33; :: thesis: verum
end;
suppose w in dom f ; :: thesis: contradiction
then ( f . w in rng f & h . w = f . w ) by ;
hence contradiction by A33; :: thesis: verum
end;
end;
end;
( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) ) by ;
then A35: ( v in dom (F0 _V) & w in dom (F0 _V) ) by ;
( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by ;
then consider e being object such that
A36: ( e Joins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 ) by ;
take e = e; :: thesis: ( e Joins v,w,G1 & e in dom g & g . e = e9 )
( v is set & w is set ) by TARSKI:1;
hence e Joins v,w,G1 by ; :: thesis: ( e in dom g & g . e = e9 )
thus ( e in dom g & g . e = e9 ) by A36; :: thesis: verum
end;
hence F is continuous ; :: thesis: verum
end;
thus ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) :: thesis: ( F0 is Dcontinuous implies F is Dcontinuous )
proof
assume A37: F0 is semi-Dcontinuous ; :: thesis:
now :: thesis: for e, v, w being object st e in dom g & v in dom h & w in dom h & g . e DJoins h . v,h . w,G2 holds
e DJoins v,w,G1
let e, v, w be object ; :: thesis: ( e in dom g & v in dom h & w in dom h & g . e DJoins h . v,h . w,G2 implies e DJoins v,w,G1 )
assume A38: ( e in dom g & v in dom h & w in dom h & g . e DJoins h . v,h . w,G2 ) ; :: thesis: e DJoins v,w,G1
then A39: (F0 _E) . e DJoins h . v,h . w,G4 by GLIB_009:41;
then (F0 _E) . e Joins h . v,h . w,G4 by GLIB_000:16;
then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;
then A40: ( not h . v in rng f & not h . w in rng f ) by ;
A41: ( not v in dom f & not w in dom f )
proof
assume ( v in dom f or w in dom f ) ; :: thesis: contradiction
per cases then ( v in dom f or w in dom f ) ;
suppose v in dom f ; :: thesis: contradiction
then ( f . v in rng f & h . v = f . v ) by ;
hence contradiction by A40; :: thesis: verum
end;
suppose w in dom f ; :: thesis: contradiction
then ( f . w in rng f & h . w = f . w ) by ;
hence contradiction by A40; :: thesis: verum
end;
end;
end;
( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) ) by ;
then A42: ( v in dom (F0 _V) & w in dom (F0 _V) ) by ;
( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by ;
then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G4 by A39;
then A43: e DJoins v,w,G3 by ;
( v is set & w is set ) by TARSKI:1;
hence e DJoins v,w,G1 by ; :: thesis: verum
end;
hence F is semi-Dcontinuous ; :: thesis: verum
end;
thus ( F0 is Dcontinuous implies F is Dcontinuous ) :: thesis: verum
proof
assume A44: F0 is Dcontinuous ; :: thesis: F is Dcontinuous
now :: thesis: for e9, v, w being object st v in dom h & w in dom h & e9 DJoins h . v,h . w,G2 holds
ex e being object st
( e DJoins v,w,G1 & e in dom g & g . e = e9 )
let e9, v, w be object ; :: thesis: ( v in dom h & w in dom h & e9 DJoins h . v,h . w,G2 implies ex e being object st
( e DJoins v,w,G1 & e in dom g & g . e = e9 ) )

assume A45: ( v in dom h & w in dom h & e9 DJoins h . v,h . w,G2 ) ; :: thesis: ex e being object st
( e DJoins v,w,G1 & e in dom g & g . e = e9 )

then A46: e9 DJoins h . v,h . w,G4 by GLIB_009:41;
then e9 Joins h . v,h . w,G4 by GLIB_000:16;
then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;
then A47: ( not h . v in rng f & not h . w in rng f ) by ;
A48: ( not v in dom f & not w in dom f )
proof
assume ( v in dom f or w in dom f ) ; :: thesis: contradiction
per cases then ( v in dom f or w in dom f ) ;
suppose v in dom f ; :: thesis: contradiction
then ( f . v in rng f & h . v = f . v ) by ;
hence contradiction by A47; :: thesis: verum
end;
suppose w in dom f ; :: thesis: contradiction
then ( f . w in rng f & h . w = f . w ) by ;
hence contradiction by A47; :: thesis: verum
end;
end;
end;
( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) ) by ;
then A49: ( v in dom (F0 _V) & w in dom (F0 _V) ) by ;
( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by ;
then consider e being object such that
A50: ( e DJoins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 ) by ;
take e = e; :: thesis: ( e DJoins v,w,G1 & e in dom g & g . e = e9 )
( v is set & w is set ) by TARSKI:1;
hence e DJoins v,w,G1 by ; :: thesis: ( e in dom g & g . e = e9 )
thus ( e in dom g & g . e = e9 ) by A50; :: thesis: verum
end;
hence F is Dcontinuous ; :: thesis: verum
end;