let G1, G2 be non-Dmulti _Graph; :: thesis: for f being PVertexMapping of G1,G2 st f is total & f is one-to-one & f is directed & f is Dcontinuous holds
for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) )
let f be PVertexMapping of G1,G2; :: thesis: ( f is total & f is one-to-one & f is directed & f is Dcontinuous implies for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) ) )
assume A1: ( f is total & f is one-to-one & f is directed & f is Dcontinuous ) ; :: thesis: for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) )
let v, w be Vertex of G1; :: thesis: ( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) )

hereby :: thesis: card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)}))

per cases ( G1 .edgesDBetween ({v},{w}) = {} or G1 .edgesDBetween ({v},{w}) <> {} ) ;

suppose A2: G1 .edgesDBetween ({v},{w}) = {} ; :: thesis: card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)}))

G2 .edgesDBetween ({(f . v)},{(f . w)}) = {}

proof

assume G2 .edgesDBetween ({(f . v)},{(f . w)}) <> {} ; :: thesis: contradiction
then consider e2 being object such that
A3: G2 .edgesDBetween ({(f . v)},{(f . w)}) = {e2} by ZFMISC_1:131;
set v1 = (the_Source_of G2) . e2;
set v2 = (the_Target_of G2) . e2;
e2 in G2 .edgesDBetween ({(f . v)},{(f . w)}) by A3, TARSKI:def 1;
then e2 DSJoins {(f . v)},{(f . w)},G2 by GLIB_000:def 31;
then A4: ( e2 in the_Edges_of G2 & (the_Source_of G2) . e2 in {(f . v)} & (the_Target_of G2) . e2 in {(f . w)} ) by GLIB_000:def 16;
then A5: ( (the_Source_of G2) . e2 = f . v & (the_Target_of G2) . e2 = f . w ) by TARSKI:def 1;
( v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total ) by A1;
then ( v in dom f & w in dom f ) by FUNCT_2:def 1;
then consider e1 being object such that
A6: e1 DJoins v,w,G1 by A1, A4, A5, GLIB_000:def 14;
( v in {v} & w in {w} ) by TARSKI:def 1;
then e1 DSJoins {v},{w},G1 by A6, GLIB_000:126;
hence contradiction by A2, GLIB_000:def 31; :: thesis: verum

end;

hence card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) by A2; :: thesis: verum

end;

suppose G1 .edgesDBetween ({v},{w}) <> {} ; :: thesis: card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)}))

then consider e1 being object such that
A7: G1 .edgesDBetween ({v},{w}) = {e1} by ZFMISC_1:131;
set v1 = (the_Source_of G1) . e1;
set v2 = (the_Target_of G1) . e1;
e1 in G1 .edgesDBetween ({v},{w}) by A7, TARSKI:def 1;
then e1 DSJoins {v},{w},G1 by GLIB_000:def 31;
then A8: ( e1 in the_Edges_of G1 & (the_Source_of G1) . e1 in {v} & (the_Target_of G1) . e1 in {w} ) by GLIB_000:def 16;
then ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 = w ) by TARSKI:def 1;
then A9: e1 DJoins v,w,G1 by A8, GLIB_000:def 14;
( v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total ) by A1;
then ( v in dom f & w in dom f ) by FUNCT_2:def 1;
then consider e2 being object such that
A10: e2 DJoins f . v,f . w,G2 by A1, A9;
( f . v in {(f . v)} & f . w in {(f . w)} ) by TARSKI:def 1;
then e2 DSJoins {(f . v)},{(f . w)},G2 by A10, GLIB_000:126;
then e2 in G2 .edgesDBetween ({(f . v)},{(f . w)}) by GLIB_000:def 31;
then consider e being object such that
A11: G2 .edgesDBetween ({(f . v)},{(f . w)}) = {e} by ZFMISC_1:131;
( card (G1 .edgesDBetween ({v},{w})) = 1 & card (G2 .edgesDBetween ({(f . v)},{(f . w)})) = 1 ) by A7, A11, CARD_1:30;
hence card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) ; :: thesis: verum

end;

end;

end;

per cases ( G1 .edgesDBetween ({w},{v}) = {} or G1 .edgesDBetween ({w},{v}) <> {} ) ;

suppose A12: G1 .edgesDBetween ({w},{v}) = {} ; :: thesis: card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)}))

G2 .edgesDBetween ({(f . w)},{(f . v)}) = {}

proof

assume G2 .edgesDBetween ({(f . w)},{(f . v)}) <> {} ; :: thesis: contradiction
then consider e2 being object such that
A13: G2 .edgesDBetween ({(f . w)},{(f . v)}) = {e2} by ZFMISC_1:131;
set v1 = (the_Source_of G2) . e2;
set v2 = (the_Target_of G2) . e2;
e2 in G2 .edgesDBetween ({(f . w)},{(f . v)}) by A13, TARSKI:def 1;
then e2 DSJoins {(f . w)},{(f . v)},G2 by GLIB_000:def 31;
then A14: ( e2 in the_Edges_of G2 & (the_Source_of G2) . e2 in {(f . w)} & (the_Target_of G2) . e2 in {(f . v)} ) by GLIB_000:def 16;
then A15: ( (the_Source_of G2) . e2 = f . w & (the_Target_of G2) . e2 = f . v ) by TARSKI:def 1;
( v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total ) by A1;
then ( v in dom f & w in dom f ) by FUNCT_2:def 1;
then consider e1 being object such that
A16: e1 DJoins w,v,G1 by A1, A14, A15, GLIB_000:def 14;
( v in {v} & w in {w} ) by TARSKI:def 1;
then e1 DSJoins {w},{v},G1 by A16, GLIB_000:126;
hence contradiction by A12, GLIB_000:def 31; :: thesis: verum

end;

hence card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) by A12; :: thesis: verum

end;

suppose G1 .edgesDBetween ({w},{v}) <> {} ; :: thesis: card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)}))

then consider e1 being object such that
A17: G1 .edgesDBetween ({w},{v}) = {e1} by ZFMISC_1:131;
set v1 = (the_Source_of G1) . e1;
set v2 = (the_Target_of G1) . e1;
e1 in G1 .edgesDBetween ({w},{v}) by A17, TARSKI:def 1;
then e1 DSJoins {w},{v},G1 by GLIB_000:def 31;
then A18: ( e1 in the_Edges_of G1 & (the_Source_of G1) . e1 in {w} & (the_Target_of G1) . e1 in {v} ) by GLIB_000:def 16;
then ( (the_Source_of G1) . e1 = w & (the_Target_of G1) . e1 = v ) by TARSKI:def 1;
then A19: e1 DJoins w,v,G1 by A18, GLIB_000:def 14;
( v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total ) by A1;
then ( v in dom f & w in dom f ) by FUNCT_2:def 1;
then consider e2 being object such that
A20: e2 DJoins f . w,f . v,G2 by A1, A19;
( f . v in {(f . v)} & f . w in {(f . w)} ) by TARSKI:def 1;
then e2 DSJoins {(f . w)},{(f . v)},G2 by A20, GLIB_000:126;
then e2 in G2 .edgesDBetween ({(f . w)},{(f . v)}) by GLIB_000:def 31;
then consider e being object such that
A21: G2 .edgesDBetween ({(f . w)},{(f . v)}) = {e} by ZFMISC_1:131;
( card (G1 .edgesDBetween ({w},{v})) = 1 & card (G2 .edgesDBetween ({(f . w)},{(f . v)})) = 1 ) by A17, A21, CARD_1:30;
hence card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) ; :: thesis: verum

end;

end;