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

proof

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

now :: thesis: for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G4 holds
e Joins v,w,G3

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

end;

hence F is semi-continuous ; :: thesis: verum

end;

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

proof

assume A3: F0 is continuous ; :: thesis: F is continuous

now :: thesis: for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G4 holds
ex e being object st
( e Joins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G4 implies ex e being object st
( e Joins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 ) )
assume ( v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G4 ) ; :: thesis: ex e being object st
( e Joins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 )
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: ( e Joins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 )
thus e Joins v,w,G3 by A4, GLIB_007:9; :: thesis: ( e in dom (F _E) & (F _E) . e = e9 )
thus ( e in dom (F _E) & (F _E) . e = e9 ) by A4; :: thesis: verum

end;

hence F is continuous ; :: thesis: verum

end;