let G1, G2 be _Graph; :: thesis: for F being semi-Dcontinuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds

F is Dcontinuous

let F be semi-Dcontinuous PGraphMapping of G1,G2; :: thesis: ( rng (F _E) = the_Edges_of G2 implies F is Dcontinuous )

assume A1: rng (F _E) = the_Edges_of G2 ; :: thesis: F is Dcontinuous

let e9, v, w be object ; :: according to GLIB_010:def 18 :: thesis: ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 implies ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) )

assume A2: ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

then e9 in the_Edges_of G2 by GLIB_000:def 14;

then consider e being object such that

A3: ( e in dom (F _E) & (F _E) . e = e9 ) by A1, FUNCT_1:def 3;

take e ; :: thesis: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

thus ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A2, A3, Def17; :: thesis: verum

F is Dcontinuous

let F be semi-Dcontinuous PGraphMapping of G1,G2; :: thesis: ( rng (F _E) = the_Edges_of G2 implies F is Dcontinuous )

assume A1: rng (F _E) = the_Edges_of G2 ; :: thesis: F is Dcontinuous

let e9, v, w be object ; :: according to GLIB_010:def 18 :: thesis: ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 implies ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) )

assume A2: ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

then e9 in the_Edges_of G2 by GLIB_000:def 14;

then consider e being object such that

A3: ( e in dom (F _E) & (F _E) . e = e9 ) by A1, FUNCT_1:def 3;

take e ; :: thesis: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

thus ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A2, A3, Def17; :: thesis: verum