let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
SG2SGFunc F is one-to-one
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding implies SG2SGFunc F is one-to-one )
assume A1: F is weak_SG-embedding ; :: thesis: SG2SGFunc F is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom (SG2SGFunc F) & x2 in dom (SG2SGFunc F) & (SG2SGFunc F) . x1 = (SG2SGFunc F) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (SG2SGFunc F) & x2 in dom (SG2SGFunc F) & (SG2SGFunc F) . x1 = (SG2SGFunc F) . x2 implies x1 = x2 )
set f = SG2SGFunc F;
assume A2: ( x1 in dom (SG2SGFunc F) & x2 in dom (SG2SGFunc F) & (SG2SGFunc F) . x1 = (SG2SGFunc F) . x2 ) ; :: thesis: x1 = x2
then reconsider H1 = x1, H2 = x2 as plain Subgraph of G1 by Th1;
A3: rng (F | H1) = (SG2SGFunc F) . x1 by Def5
.= rng (F | H2) by A2, Def5 ;
A4: ( F | H1 is total & F | H2 is total ) by A1, GLIB_010:57;
A5: (F _V) .: (the_Vertices_of H1) = rng ((F _V) | (the_Vertices_of H1)) by RELAT_1:115
.= the_Vertices_of (rng (F | H1)) by A4, GLIB_010:54
.= rng ((F | H2) _V) by A3, A4, GLIB_010:54
.= (F _V) .: (the_Vertices_of H2) by RELAT_1:115 ;
( the_Vertices_of H1 c= the_Vertices_of G1 & the_Vertices_of H2 c= the_Vertices_of G1 ) ;
then ( the_Vertices_of H1 c= dom (F _V) & the_Vertices_of H2 c= dom (F _V) ) by A1, GLIB_010:def 11;
then A6: ( the_Vertices_of H1 c= the_Vertices_of H2 & the_Vertices_of H2 c= the_Vertices_of H1 ) by A1, A5, FUNCT_1:87;
A7: (F _E) .: (the_Edges_of H1) = rng ((F _E) | (the_Edges_of H1)) by RELAT_1:115
.= the_Edges_of (rng (F | H1)) by A4, GLIB_010:54
.= rng ((F | H2) _E) by A3, A4, GLIB_010:54
.= (F _E) .: (the_Edges_of H2) by RELAT_1:115 ;
( the_Edges_of H1 c= the_Edges_of G1 & the_Edges_of H2 c= the_Edges_of G1 ) ;
then ( the_Edges_of H1 c= dom (F _E) & the_Edges_of H2 c= dom (F _E) ) by A1, GLIB_010:def 11;
then ( the_Edges_of H1 c= the_Edges_of H2 & the_Edges_of H2 c= the_Edges_of H1 ) by A1, A7, FUNCT_1:87;
then ( H1 is Subgraph of H2 & H2 is Subgraph of H1 ) by A6, GLIB_000:44;
hence x1 = x2 by GLIB_000:87, GLIB_009:44; :: thesis: verum

end;

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