let G1 be non-multi _Graph; :: thesis: for G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 holds F _E is one-to-one
let G2 be _Graph; :: thesis: 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; :: thesis: F _E is one-to-one

now :: thesis: for e1, e2 being object st e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 holds
e1 = e2

let e1, e2 be object ; :: thesis: ( 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 ) ; :: thesis: e1 = e2
then 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; :: thesis: verum

end;

hence F _E is one-to-one by FUNCT_1:def 4; :: thesis: verum