let G1, G2 be _Graph; 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; 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); ( F is isomorphism implies card (G1 .edgesBetween (X,Y)) = card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))) )
assume A1:
F is isomorphism
; 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; verum