let G1, G2 be _Graph; :: thesis:
let E1, E2 be set ; :: thesis:
let G3 be reverseEdgeDirections of G1,E1; :: thesis:
let G4 be reverseEdgeDirections of G2,E2; :: thesis:
let F0 be PGraphMapping of G1,G2; :: thesis:
reconsider F = F0 as PGraphMapping of G3,G4 by Th10;
take F ; :: thesis:
thus F = F0 ; :: thesis:
thus ( not F0 is empty implies not F is empty ) ; :: thesis:
thus ( F0 is total implies F is total ) by GLIB_007:4; :: thesis:
thus ( F0 is onto implies F is onto ) by GLIB_007:4; :: thesis:
thus ( F0 is one-to-one implies F is one-to-one ) ; :: thesis:
thus ( F0 is semi-continuous implies F is semi-continuous ) :: thesis:

proof

assume A1: F0 is semi-continuous ; :: thesis:

now :: thesis:

let e, v, w be object ; :: thesis:
assume A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis:
assume (F _E) . e Joins (F _V) . v,(F _V) . w,G4 ; :: thesis:
then e Joins v,w,G1 by A1, A2, GLIB_007:9;
hence e Joins v,w,G3 by GLIB_007:9; :: thesis:

end;

hence F is semi-continuous ; :: thesis:

end;

thus ( F0 is continuous implies F is continuous ) :: thesis:

proof

assume A3: F0 is continuous ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume ( v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G4 ) ; :: thesis:
then consider e being object such that
A4: ( e Joins v,w,G1 & e in dom (F0 _E) & (F0 _E) . e = e9 ) by A3, GLIB_007:9;
take e = e; :: thesis:
thus e Joins v,w,G3 by A4, GLIB_007:9; :: thesis:
thus ( e in dom (F _E) & (F _E) . e = e9 ) by A4; :: thesis:

end;

hence F is continuous ; :: thesis:

end;