let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding & F is onto holds
(F _E) .: (G1 .edgesBetween (X,Y)) = G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
let F be PGraphMapping of G1,G2; :: thesis: for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding & F is onto holds
(F _E) .: (G1 .edgesBetween (X,Y)) = G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
let X, Y be Subset of (the_Vertices_of G1); :: thesis: ( F is weak_SG-embedding & F is onto implies (F _E) .: (G1 .edgesBetween (X,Y)) = G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) )
assume A1: ( F is weak_SG-embedding & F is onto ) ; :: thesis: (F _E) .: (G1 .edgesBetween (X,Y)) = G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
then reconsider F9 = F as one-to-one PGraphMapping of G1,G2 ;
A2: (F _E) .: (G1 .edgesBetween (X,Y)) c= G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by A1, Th91;
A3: ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 ) by A1, GLIB_010:def 11;
G1 .edgesBetween ((((F9 ") _V) .: ((F _V) .: X)),(((F9 ") _V) .: ((F _V) .: Y))) = G1 .edgesBetween (((F9 _V) " ((F9 _V) .: X)),(((F9 _V) ") .: ((F _V) .: Y))) by FUNCT_1:85
.= G1 .edgesBetween (((F9 _V) " ((F9 _V) .: X)),((F9 _V) " ((F _V) .: Y))) by FUNCT_1:85
.= G1 .edgesBetween (X,((F9 _V) " ((F _V) .: Y))) by A3, FUNCT_1:94
.= G1 .edgesBetween (X,Y) by A3, FUNCT_1:94 ;
then A4: ((F9 ") _E) .: (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) c= G1 .edgesBetween (X,Y) by A1, GLIB_010:72, Th91;
A5: rng (F _E) = the_Edges_of G2 by A1, GLIB_010:def 12;
(F _E) .: (((F9 ") _E) .: (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))) = (F _E) .: ((F9 _E) " (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))) by FUNCT_1:85
.= G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by A5, FUNCT_1:77 ;
then G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) c= (F _E) .: (G1 .edgesBetween (X,Y)) by A4, RELAT_1:123;
hence (F _E) .: (G1 .edgesBetween (X,Y)) = G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)) by A2, XBOOLE_0:def 10; :: thesis: verum