let G1, G2 be _Graph; for F being semi-continuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds
F is continuous
let F be semi-continuous PGraphMapping of G1,G2; ( rng (F _E) = the_Edges_of G2 implies F is continuous )
assume A1:
rng (F _E) = the_Edges_of G2
; F is continuous
let e9, v, w be object ; GLIB_010:def 16 ( v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 implies ex e being object st
( e Joins 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 Joins (F _V) . v,(F _V) . w,G2 )
; ex e being object st
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
then
e9 in the_Edges_of G2
by GLIB_000:def 13;
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
; ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
thus
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
by A2, A3, Def15; verum