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 )

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

thus
( F0 is continuous implies F is continuous )
:: thesis: verum
assume A1:
F0 is semi-continuous
; :: thesis: F is semi-continuous

end;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

hence
F is semi-continuous
; :: thesis: verume 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;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

proof

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

end;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 )

hence
F is continuous
; :: thesis: verumex 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;( 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