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