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

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

card (G1 .edgesBetween X) = card (G2 .edgesBetween ((F _V) .: X))

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

card (G1 .edgesBetween X) = card (G2 .edgesBetween ((F _V) .: X))

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

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

then A2: card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X)) by Th47;

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

F0 " is isomorphism by A1, Th75;

then A3: card (G2 .edgesBetween ((F _V) .: X)) c= card (G1 .edgesBetween (((F0 ") _V) .: ((F _V) .: X))) by Th47;

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

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

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

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

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

card (G1 .edgesBetween X) = card (G2 .edgesBetween ((F _V) .: X))

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

card (G1 .edgesBetween X) = card (G2 .edgesBetween ((F _V) .: X))

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

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

then A2: card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X)) by Th47;

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

F0 " is isomorphism by A1, Th75;

then A3: card (G2 .edgesBetween ((F _V) .: X)) c= card (G1 .edgesBetween (((F0 ") _V) .: ((F _V) .: X))) by Th47;

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

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

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

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