let G1, G2 be _Graph; :: thesis: for F0 being PGraphMapping of G1,G2 st F0 _E is one-to-one holds
ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )
let F0 be PGraphMapping of G1,G2; :: thesis: ( F0 _E is one-to-one implies ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) ) )
assume A1: F0 _E is one-to-one ; :: thesis: ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )

per cases ( the_Edges_of G2 <> {} or the_Edges_of G2 = {} ) ;

suppose the_Edges_of G2 <> {} ; :: thesis: ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )

set E = { e9 where e9 is Element of the_Edges_of G2 : ( e9 in rng (F0 _E) & ( for e being object st e in dom (F0 _E) & (F0 _E) . e = e9 holds
e9 DJoins (F0 _V) . ((the_Target_of G1) . e),(F0 _V) . ((the_Source_of G1) . e),G2 ) ) } ;

now :: thesis: for x being object st x in { e9 where e9 is Element of the_Edges_of G2 : ( e9 in rng (F0 _E) & ( for e being object st e in dom (F0 _E) & (F0 _E) . e = e9 holds
e9 DJoins (F0 _V) . ((the_Target_of G1) . e),(F0 _V) . ((the_Source_of G1) . e),G2 ) ) } holds
x in the_Edges_of G2

let x be object ; :: thesis: ( x in { e9 where e9 is Element of the_Edges_of G2 : ( e9 in rng (F0 _E) & ( for e being object st e in dom (F0 _E) & (F0 _E) . e = e9 holds
e9 DJoins (F0 _V) . ((the_Target_of G1) . e),(F0 _V) . ((the_Source_of G1) . e),G2 ) ) } implies x in the_Edges_of G2 )
assume x in { e9 where e9 is Element of the_Edges_of G2 : ( e9 in rng (F0 _E) & ( for e being object st e in dom (F0 _E) & (F0 _E) . e = e9 holds
e9 DJoins (F0 _V) . ((the_Target_of G1) . e),(F0 _V) . ((the_Source_of G1) . e),G2 ) ) } ; :: thesis: x in the_Edges_of G2
then consider e9 being Element of the_Edges_of G2 such that
A2: x = e9 and
A3: e9 in rng (F0 _E) and
for e being object st e in dom (F0 _E) & (F0 _E) . e = e9 holds
e9 DJoins (F0 _V) . ((the_Target_of G1) . e),(F0 _V) . ((the_Source_of G1) . e),G2 ;
e9 in the_Edges_of G2 by A3;
hence x in the_Edges_of G2 by A2; :: thesis: verum

end;

then reconsider E = { e9 where e9 is Element of the_Edges_of G2 : ( e9 in rng (F0 _E) & ( for e being object st e in dom (F0 _E) & (F0 _E) . e = e9 holds
e9 DJoins (F0 _V) . ((the_Target_of G1) . e),(F0 _V) . ((the_Source_of G1) . e),G2 ) ) } as Subset of (the_Edges_of G2) by TARSKI:def 3;
take E ; :: thesis: for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )
let G3 be reverseEdgeDirections of G2,E; :: thesis: ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )
consider F9 being PGraphMapping of G2,G3 such that
A4: ( F9 = id G2 & F9 is isomorphism ) by Th83;
take F9 * F0 ; :: thesis: ( F9 * F0 = F0 & F9 * F0 is directed & ( not F0 is empty implies not F9 * F0 is empty ) & ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) )
thus A5: F9 * F0 = (id G2) * F0 by A4
.= F0 by GLIB_010:116 ; :: thesis: ( F9 * F0 is directed & ( not F0 is empty implies not F9 * F0 is empty ) & ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) )

now :: thesis: for e, v, w being object st e in dom ((F9 * F0) _E) & v in dom ((F9 * F0) _V) & w in dom ((F9 * F0) _V) & e DJoins v,w,G1 holds
((F9 * F0) _E) . e DJoins ((F9 * F0) _V) . v,((F9 * F0) _V) . w,G3

let e, v, w be object ; :: thesis: ( e in dom ((F9 * F0) _E) & v in dom ((F9 * F0) _V) & w in dom ((F9 * F0) _V) & e DJoins v,w,G1 implies ((F9 * F0) _E) . b₁ DJoins ((F9 * F0) _V) . b₂,((F9 * F0) _V) . b₃,G3 )
assume ( e in dom ((F9 * F0) _E) & v in dom ((F9 * F0) _V) & w in dom ((F9 * F0) _V) ) ; :: thesis: ( e DJoins v,w,G1 implies ((F9 * F0) _E) . b₁ DJoins ((F9 * F0) _V) . b₂,((F9 * F0) _V) . b₃,G3 )
then A6: ( e in dom (F0 _E) & v in dom (F0 _V) & w in dom (F0 _V) ) by A5;
assume A7: e DJoins v,w,G1 ; :: thesis: ((F9 * F0) _E) . b₁ DJoins ((F9 * F0) _V) . b₂,((F9 * F0) _V) . b₃,G3
A8: (F0 _E) . e in rng (F0 _E) by A6, FUNCT_1:3;
then reconsider e9 = (F0 _E) . e as Element of the_Edges_of G2 ;

per cases ( e9 in E or not e9 in E ) ;

suppose A11: e9 in E ; :: thesis: ((F9 * F0) _E) . b₁ DJoins ((F9 * F0) _V) . b₂,((F9 * F0) _V) . b₃,G3

then consider e8 being Element of the_Edges_of G2 such that
A12: ( e8 = e9 & e8 in rng (F0 _E) ) and
A13: for e0 being object st e0 in dom (F0 _E) & (F0 _E) . e0 = e8 holds
e8 DJoins (F0 _V) . ((the_Target_of G1) . e0),(F0 _V) . ((the_Source_of G1) . e0),G2 ;
A14: e9 DJoins (F0 _V) . ((the_Target_of G1) . e),(F0 _V) . ((the_Source_of G1) . e),G2 by A6, A12, A13;
( (the_Source_of G1) . e = v & (the_Target_of G1) . e = w ) by A7, GLIB_000:def 14;
then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G3 by A11, A14, GLIB_007:7;
hence ((F9 * F0) _E) . e DJoins ((F9 * F0) _V) . v,((F9 * F0) _V) . w,G3 by A5; :: thesis: verum

end;

suppose A15: not e9 in E ; :: thesis: ((F9 * F0) _E) . b₁ DJoins ((F9 * F0) _V) . b₂,((F9 * F0) _V) . b₃,G3

e Joins v,w,G1 by A7, GLIB_000:16;
then A16: (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G2 by A6, GLIB_010:4;
not (F0 _E) . e DJoins (F0 _V) . w,(F0 _V) . v,G2

proof

assume A17: (F0 _E) . e DJoins (F0 _V) . w,(F0 _V) . v,G2 ; :: thesis: contradiction
for e0 being object st e0 in dom (F0 _E) & (F0 _E) . e0 = e9 holds
e9 DJoins (F0 _V) . ((the_Target_of G1) . e0),(F0 _V) . ((the_Source_of G1) . e0),G2

proof

let e0 be object ; :: thesis: ( e0 in dom (F0 _E) & (F0 _E) . e0 = e9 implies e9 DJoins (F0 _V) . ((the_Target_of G1) . e0),(F0 _V) . ((the_Source_of G1) . e0),G2 )
assume ( e0 in dom (F0 _E) & (F0 _E) . e0 = e9 ) ; :: thesis: e9 DJoins (F0 _V) . ((the_Target_of G1) . e0),(F0 _V) . ((the_Source_of G1) . e0),G2
then e = e0 by A1, A6, FUNCT_1:def 4;
then ( (the_Source_of G1) . e0 = v & (the_Target_of G1) . e0 = w ) by A7, GLIB_000:def 14;
hence e9 DJoins (F0 _V) . ((the_Target_of G1) . e0),(F0 _V) . ((the_Source_of G1) . e0),G2 by A17; :: thesis: verum

end;

hence contradiction by A8, A15; :: thesis: verum

end;

then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G2 by A16, GLIB_000:16;
then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G3 by A15, GLIB_007:8;
hence ((F9 * F0) _E) . e DJoins ((F9 * F0) _V) . v,((F9 * F0) _V) . w,G3 by A5; :: thesis: verum

end;

end;

end;

hence F9 * F0 is directed by GLIB_010:def 14; :: thesis: ( ( not F0 is empty implies not F9 * F0 is empty ) & ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) )
thus ( not F0 is empty implies not F9 * F0 is empty ) by A5; :: thesis: ( ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) )
thus ( ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) ) by A4, GLIB_010:104, GLIB_010:106; :: thesis: verum

end;

suppose A18: the_Edges_of G2 = {} ; :: thesis: ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )

take E = {} (the_Edges_of G2); :: thesis: for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )
let G3 be reverseEdgeDirections of G2,E; :: thesis: ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )
consider F9 being PGraphMapping of G2,G3 such that
A19: ( F9 = id G2 & F9 is isomorphism ) by Th83;
take F9 * F0 ; :: thesis: ( F9 * F0 = F0 & F9 * F0 is directed & ( not F0 is empty implies not F9 * F0 is empty ) & ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) )
thus A20: F9 * F0 = (id G2) * F0 by A19
.= F0 by GLIB_010:116 ; :: thesis: ( F9 * F0 is directed & ( not F0 is empty implies not F9 * F0 is empty ) & ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) )
the_Edges_of G3 = {} by A18, GLIB_007:4;
then G3 is edgeless ;
hence F9 * F0 is directed ; :: thesis: ( ( not F0 is empty implies not F9 * F0 is empty ) & ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) )
thus ( not F0 is empty implies not F9 * F0 is empty ) by A20; :: thesis: ( ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) )
thus ( ( F0 is total implies F9 * F0 is total ) & ( F0 is one-to-one implies F9 * F0 is one-to-one ) & ( F0 is onto implies F9 * F0 is onto ) & ( F0 is semi-continuous implies F9 * F0 is semi-continuous ) & ( F0 is continuous implies F9 * F0 is continuous ) ) by A19, GLIB_010:104, GLIB_010:106; :: thesis: verum

end;

end;