let G1, G2 be _Graph; :: thesis: for F being directed PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

let F be directed PGraphMapping of G1,G2; :: thesis: for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

let X, Y be Subset of (the_Vertices_of G1); :: thesis: ( F is isomorphism implies card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y))) )

assume A1: F is isomorphism ; :: thesis: card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

then A2: card (G1 .edgesDBetween (X,Y)) c= card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y))) by Th48;

reconsider F0 = F as one-to-one PGraphMapping of G1,G2 by A1;

F0 " is isomorphism by A1, Th75;

then A3: card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y))) c= card (G1 .edgesDBetween ((((F0 ") _V) .: ((F _V) .: X)),(((F0 ") _V) .: ((F _V) .: Y)))) by Th48;

A4: dom (F _V) = the_Vertices_of G1 by A1, Def11;

A5: ((F0 ") _V) .: ((F _V) .: X) = (F _V) " ((F _V) .: X) by FUNCT_1:85

.= X by A1, A4, FUNCT_1:94 ;

((F0 ") _V) .: ((F _V) .: Y) = (F _V) " ((F _V) .: Y) by FUNCT_1:85

.= Y by A1, A4, FUNCT_1:94 ;

hence card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y))) by A2, A3, A5, XBOOLE_0:def 10; :: thesis: verum

for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

let F be directed PGraphMapping of G1,G2; :: thesis: for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

let X, Y be Subset of (the_Vertices_of G1); :: thesis: ( F is isomorphism implies card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y))) )

assume A1: F is isomorphism ; :: thesis: card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

then A2: card (G1 .edgesDBetween (X,Y)) c= card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y))) by Th48;

reconsider F0 = F as one-to-one PGraphMapping of G1,G2 by A1;

F0 " is isomorphism by A1, Th75;

then A3: card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y))) c= card (G1 .edgesDBetween ((((F0 ") _V) .: ((F _V) .: X)),(((F0 ") _V) .: ((F _V) .: Y)))) by Th48;

A4: dom (F _V) = the_Vertices_of G1 by A1, Def11;

A5: ((F0 ") _V) .: ((F _V) .: X) = (F _V) " ((F _V) .: X) by FUNCT_1:85

.= X by A1, A4, FUNCT_1:94 ;

((F0 ") _V) .: ((F _V) .: Y) = (F _V) " ((F _V) .: Y) by FUNCT_1:85

.= Y by A1, A4, FUNCT_1:94 ;

hence card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y))) by A2, A3, A5, XBOOLE_0:def 10; :: thesis: verum