let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F _V is one-to-one holds

F is semi-continuous

let F be PGraphMapping of G1,G2; :: thesis: ( F _V is one-to-one implies F is semi-continuous )

assume A1: F _V is one-to-one ; :: thesis: F is semi-continuous

let e, v, w be object ; :: according to GLIB_010:def 15 :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 implies e Joins v,w,G1 )

assume that

A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) and

A3: (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ; :: thesis: e Joins v,w,G1

set v1 = (the_Source_of G1) . e;

set v2 = (the_Target_of G1) . e;

A4: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A2, GLIB_000:def 13;

A5: ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by A2, Th5;

then (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Target_of G1) . e),G2 by A2, A4, Th4;

F is semi-continuous

let F be PGraphMapping of G1,G2; :: thesis: ( F _V is one-to-one implies F is semi-continuous )

assume A1: F _V is one-to-one ; :: thesis: F is semi-continuous

let e, v, w be object ; :: according to GLIB_010:def 15 :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 implies e Joins v,w,G1 )

assume that

A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) and

A3: (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ; :: thesis: e Joins v,w,G1

set v1 = (the_Source_of G1) . e;

set v2 = (the_Target_of G1) . e;

A4: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A2, GLIB_000:def 13;

A5: ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by A2, Th5;

then (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Target_of G1) . e),G2 by A2, A4, Th4;

per cases then
( ( (F _V) . ((the_Source_of G1) . e) = (F _V) . v & (F _V) . ((the_Target_of G1) . e) = (F _V) . w ) or ( (F _V) . ((the_Source_of G1) . e) = (F _V) . w & (F _V) . ((the_Target_of G1) . e) = (F _V) . v ) )
by A3, GLIB_000:15;

end;

suppose
( (F _V) . ((the_Source_of G1) . e) = (F _V) . v & (F _V) . ((the_Target_of G1) . e) = (F _V) . w )
; :: thesis: e Joins v,w,G1

then
( (the_Source_of G1) . e = v & (the_Target_of G1) . e = w )
by A1, A2, A5, FUNCT_1:def 4;

hence e Joins v,w,G1 by A4; :: thesis: verum

end;hence e Joins v,w,G1 by A4; :: thesis: verum

suppose
( (F _V) . ((the_Source_of G1) . e) = (F _V) . w & (F _V) . ((the_Target_of G1) . e) = (F _V) . v )
; :: thesis: e Joins v,w,G1

then
( (the_Source_of G1) . e = w & (the_Target_of G1) . e = v )
by A1, A2, A5, FUNCT_1:def 4;

hence e Joins v,w,G1 by A4, GLIB_000:14; :: thesis: verum

end;hence e Joins v,w,G1 by A4, GLIB_000:14; :: thesis: verum