let G1 be non-multi _Graph; for G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 holds F _E is one-to-one
let G2 be _Graph; for F being semi-continuous PGraphMapping of G1,G2 holds F _E is one-to-one
let F be semi-continuous PGraphMapping of G1,G2; F _E is one-to-one
now for e1, e2 being object st e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 holds
e1 = e2let e1,
e2 be
object ;
( e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 implies e1 = e2 )assume A1:
(
e1 in dom (F _E) &
e2 in dom (F _E) &
(F _E) . e1 = (F _E) . e2 )
;
e1 = e2then A2:
(
(the_Source_of G1) . e1 in dom (F _V) &
(the_Target_of G1) . e1 in dom (F _V) )
by Th5;
A3:
e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G1
by A1, GLIB_000:def 13;
then
(F _E) . e2 Joins (F _V) . ((the_Source_of G1) . e1),
(F _V) . ((the_Target_of G1) . e1),
G2
by A1, A2, Th4;
then
e2 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G1
by A1, A2, Def15;
hence
e1 = e2
by A3, GLIB_000:def 20;
verum end;
hence
F _E is one-to-one
by FUNCT_1:def 4; verum