let G1, G2 be _Graph; :: thesis: for F being semi-Dcontinuous PGraphMapping of G1,G2
for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v1,(F _V) . w,G2 ) holds
v1 = v2
let F be semi-Dcontinuous PGraphMapping of G1,G2; :: thesis: for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v1,(F _V) . w,G2 ) 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 & ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v1,(F _V) . w,G2 ) implies v1 = v2 )
assume that
A1: ( v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 ) and
A2: ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v1,(F _V) . w,G2 ) ; :: thesis: v1 = v2
consider e, w being object such that
A3: ( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v1,(F _V) . w,G2 ) by A2;
A4: e DJoins v1,w,G1 by A1, A3, Def17;
e DJoins v2,w,G1 by A1, A3, Def17;
hence v1 = v2 by A4, GLIB_000:125; :: thesis: verum