let G1, G2 be non-multi _Graph; :: thesis: for f being PVertexMapping of G1,G2 st f is total & f is one-to-one & f is continuous holds
for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
let f be PVertexMapping of G1,G2; :: thesis: ( f is total & f is one-to-one & f is continuous implies for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) )
assume A1: ( f is total & f is one-to-one & f is continuous ) ; :: thesis: for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
let v, w be Vertex of G1; :: thesis: card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
per cases ( G1 .edgesBetween ({v},{w}) = {} or G1 .edgesBetween ({v},{w}) <> {} ) ;
suppose A2: G1 .edgesBetween ({v},{w}) = {} ; :: thesis: card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
G2 .edgesBetween ({(f . v)},{(f . w)}) = {}
proof
assume G2 .edgesBetween ({(f . v)},{(f . w)}) <> {} ; :: thesis: contradiction
then consider e2 being object such that
A3: G2 .edgesBetween ({(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 .edgesBetween ({(f . v)},{(f . w)}) by A3, TARSKI:def 1;
then e2 SJoins {(f . v)},{(f . w)},G2 by GLIB_000:def 30;
then A4: ( e2 in the_Edges_of G2 & ( ( (the_Source_of G2) . e2 in {(f . v)} & (the_Target_of G2) . e2 in {(f . w)} ) or ( (the_Source_of G2) . e2 in {(f . w)} & (the_Target_of G2) . e2 in {(f . v)} ) ) ) by GLIB_000:def 15;
then ( ( (the_Source_of G2) . e2 = f . v & (the_Target_of G2) . e2 = f . w ) or ( (the_Source_of G2) . e2 = f . w & (the_Target_of G2) . e2 = f . v ) ) by TARSKI:def 1;
then A5: e2 Joins f . v,f . w,G2 by A4, GLIB_000:def 13;
( 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 Joins v,w,G1 by A1, A5, Th2;
( v in {v} & w in {w} ) by TARSKI:def 1;
then e1 SJoins {v},{w},G1 by A6, GLIB_000:17;
hence contradiction by A2, GLIB_000:def 30; :: thesis: verum
end;
hence card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) by A2; :: thesis: verum
end;
suppose G1 .edgesBetween ({v},{w}) <> {} ; :: thesis: card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
then consider e1 being object such that
A7: G1 .edgesBetween ({v},{w}) = {e1} by ZFMISC_1:131;
set v1 = (the_Source_of G1) . e1;
set v2 = (the_Target_of G1) . e1;
e1 in G1 .edgesBetween ({v},{w}) by A7, TARSKI:def 1;
then e1 SJoins {v},{w},G1 by GLIB_000:def 30;
then A8: ( e1 in the_Edges_of G1 & ( ( (the_Source_of G1) . e1 in {v} & (the_Target_of G1) . e1 in {w} ) or ( (the_Source_of G1) . e1 in {w} & (the_Target_of G1) . e1 in {v} ) ) ) by GLIB_000:def 15;
then ( ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 = w ) or ( (the_Source_of G1) . e1 = w & (the_Target_of G1) . e1 = v ) ) by TARSKI:def 1;
then A9: e1 Joins v,w,G1 by A8, GLIB_000:def 13;
( 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 Joins f . v,f . w,G2 by A9, Th1;
( f . v in {(f . v)} & f . w in {(f . w)} ) by TARSKI:def 1;
then e2 SJoins {(f . v)},{(f . w)},G2 by A10, GLIB_000:17;
then e2 in G2 .edgesBetween ({(f . v)},{(f . w)}) by GLIB_000:def 30;
then consider e being object such that
A11: G2 .edgesBetween ({(f . v)},{(f . w)}) = {e} by ZFMISC_1:131;
( card (G1 .edgesBetween ({v},{w})) = 1 & card (G2 .edgesBetween ({(f . v)},{(f . w)})) = 1 ) by A7, A11, CARD_1:30;
hence card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) ; :: thesis: verum
end;
end;