let G1, G2, G3, G4 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st ex E1, E2 being set st

( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) holds

F is PGraphMapping of G3,G4

let F be PGraphMapping of G1,G2; :: thesis: ( ex E1, E2 being set st

( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) implies F is PGraphMapping of G3,G4 )

given E1, E2 being set such that A1: ( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) ; :: thesis: F is PGraphMapping of G3,G4

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 A1, GLIB_007:4;

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;

hence F is PGraphMapping of G3,G4 ; :: thesis: verum

( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) holds

F is PGraphMapping of G3,G4

let F be PGraphMapping of G1,G2; :: thesis: ( ex E1, E2 being set st

( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) implies F is PGraphMapping of G3,G4 )

given E1, E2 being set such that A1: ( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) ; :: thesis: F is PGraphMapping of G3,G4

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 A1, GLIB_007:4;

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 :: thesis: ( ( 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 ) )

assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( 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_007:9; :: thesis: verum

end;

then
[f,g] is PGraphMapping of G3,G4
by Th8;( (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 ) )

hereby :: thesis: 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 ; :: thesis: ( 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 )g . e Joins f . v,f . w,G4

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G3) . b_{1} in dom f & (the_Target_of G3) . b_{1} in dom f ) )

assume A3: e in dom g ; :: thesis: ( (the_Source_of G3) . b_{1} in dom f & (the_Target_of G3) . b_{1} in dom f )

then A4: ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by Th5;

e in the_Edges_of G1 by A2, A3;

then A5: e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 14;

end;assume A3: e in dom g ; :: thesis: ( (the_Source_of G3) . b

then A4: ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by Th5;

e in the_Edges_of G1 by A2, A3;

then A5: e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 14;

per cases
( E1 c= the_Edges_of G1 or not E1 c= the_Edges_of G1 )
;

end;

suppose A6:
E1 c= the_Edges_of G1
; :: thesis: ( (the_Source_of G3) . b_{1} in dom f & (the_Target_of G3) . b_{1} in dom f )

end;

per cases
( e in E1 or not e in E1 )
;

end;

suppose
e in E1
; :: thesis: ( (the_Source_of G3) . b_{1} in dom f & (the_Target_of G3) . b_{1} in dom f )

then
e DJoins (the_Target_of G1) . e,(the_Source_of G1) . e,G3
by A1, A5, A6, GLIB_007:7;

hence ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) by A4, GLIB_000:def 14; :: thesis: verum

end;hence ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) by A4, GLIB_000:def 14; :: thesis: verum

suppose
not e in E1
; :: thesis: ( (the_Source_of G3) . b_{1} in dom f & (the_Target_of G3) . b_{1} in dom f )

then
e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G3
by A1, A5, A6, GLIB_007:8;

hence ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) by A4, GLIB_000:def 14; :: thesis: verum

end;hence ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) by A4, GLIB_000:def 14; :: thesis: verum

suppose
not E1 c= the_Edges_of G1
; :: thesis: ( (the_Source_of G3) . b_{1} in dom f & (the_Target_of G3) . b_{1} in dom f )

then
G1 == G3
by A1, GLIB_007:def 1;

hence ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) by A4, GLIB_000:def 34; :: thesis: verum

end;hence ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) by A4, GLIB_000:def 34; :: thesis: verum

assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( 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_007:9; :: thesis: verum

hence F is PGraphMapping of G3,G4 ; :: thesis: verum