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
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
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;
hence F _V is one-to-one by FUNCT_1:def 4; :: thesis: verum