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 isomorphism holds
card (G1 .edgesBetween (X,Y)) = card (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 isomorphism holds
card (G1 .edgesBetween (X,Y)) = card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))
let X, Y be Subset of (the_Vertices_of G1); :: thesis: ( F is isomorphism implies card (G1 .edgesBetween (X,Y)) = card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) )
assume A1: F is isomorphism ; :: thesis: card (G1 .edgesBetween (X,Y)) = card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))
then A2: card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) by Th46;
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),((F _V) .: Y))) c= card (G1 .edgesBetween ((((F0 ") _V) .: ((F _V) .: X)),(((F0 ") _V) .: ((F _V) .: Y)))) by Th46;
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 .edgesBetween (X,Y)) = card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) by A2, A3, A5, XBOOLE_0:def 10; :: thesis: verum