let G1, G2 be _Graph; :: thesis: for F being semi-continuous PGraphMapping of G1,G2 st ( for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ) holds

F _V is one-to-one

let F be semi-continuous PGraphMapping of G1,G2; :: thesis: ( ( for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ) implies F _V is one-to-one )

assume A1: for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ; :: thesis: F _V is one-to-one

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ) holds

F _V is one-to-one

let F be semi-continuous PGraphMapping of G1,G2; :: thesis: ( ( for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ) implies F _V is one-to-one )

assume A1: for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ; :: thesis: F _V is one-to-one

now :: thesis: for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 holds

v1 = v2

hence
F _V is one-to-one
by FUNCT_1:def 4; :: thesis: verumv1 = v2

let v1, v2 be object ; :: thesis: ( v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 implies v1 = v2 )

assume A2: ( v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 ) ; :: thesis: v1 = v2

then consider e, w being object such that

A3: ( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v1,(F _V) . w,G2 ) by A1;

thus v1 = v2 by A2, A3, Th26; :: thesis: verum

end;assume A2: ( v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 ) ; :: thesis: v1 = v2

then consider e, w being object such that

A3: ( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v1,(F _V) . w,G2 ) by A1;

thus v1 = v2 by A2, A3, Th26; :: thesis: verum