let G1, G2 be _Graph; 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; ( ( 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 )
; F _V is one-to-one
hence
F _V is one-to-one
by FUNCT_1:def 4; verum