let G1, G2, G3, G4 be _Graph; for F being PGraphMapping of G1,G2 st G1 == G3 & G2 == G4 holds
F is PGraphMapping of G3,G4
let F be PGraphMapping of G1,G2; ( G1 == G3 & G2 == G4 implies F is PGraphMapping of G3,G4 )
assume A1:
( G1 == G3 & G2 == G4 )
; F is PGraphMapping of G3,G4
then A2:
( the_Vertices_of G1 = the_Vertices_of G3 & the_Edges_of G1 = the_Edges_of G3 & the_Vertices_of G2 = the_Vertices_of G4 & the_Edges_of G2 = the_Edges_of G4 )
by GLIB_000:def 34;
then reconsider f = F _V as PartFunc of (the_Vertices_of G3),(the_Vertices_of G4) ;
reconsider g = F _E as PartFunc of (the_Edges_of G3),(the_Edges_of G4) by A2;
now ( ( for e being object st e in dom g holds
( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G3 holds
g . e Joins f . v,f . w,G4 ) )let e,
v,
w be
object ;
( e in dom g & v in dom f & w in dom f & e Joins v,w,G3 implies g . e Joins f . v,f . w,G4 )assume
(
e in dom g &
v in dom f &
w in dom f )
;
( e Joins v,w,G3 implies g . e Joins f . v,f . w,G4 )then
(
e Joins v,
w,
G1 implies
g . e Joins f . v,
f . w,
G2 )
by Th4;
hence
(
e Joins v,
w,
G3 implies
g . e Joins f . v,
f . w,
G4 )
by A1, GLIB_000:88;
verum end;
then
[f,g] is PGraphMapping of G3,G4
by Th8;
hence
F is PGraphMapping of G3,G4
; verum