let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 holds
( F is directed iff ( (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) & (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) ) )
let F be PGraphMapping of G1,G2; :: thesis: ( F is directed iff ( (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) & (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) ) )

hereby :: thesis: ( (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) & (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) implies F is directed )

assume F is directed ; :: thesis: ( (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) & (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) )
then A1: for e being object st e in dom (F _E) holds
( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) by Th13;
for x being object holds
( x in dom ((the_Source_of G2) * (F _E)) iff x in dom ((F _V) * ((the_Source_of G1) | (dom (F _E)))) )

proof

let x be object ; :: thesis: ( x in dom ((the_Source_of G2) * (F _E)) iff x in dom ((F _V) * ((the_Source_of G1) | (dom (F _E)))) )

hereby :: thesis: ( x in dom ((F _V) * ((the_Source_of G1) | (dom (F _E)))) implies x in dom ((the_Source_of G2) * (F _E)) )

assume x in dom ((the_Source_of G2) * (F _E)) ; :: thesis: x in dom ((F _V) * ((the_Source_of G1) | (dom (F _E))))
then A2: x in dom (F _E) by FUNCT_1:11;
then x in the_Edges_of G1 ;
then x in dom (the_Source_of G1) by FUNCT_2:def 1;
then A3: x in dom ((the_Source_of G1) | (dom (F _E))) by A2, RELAT_1:57;
(the_Source_of G1) . x in dom (F _V) by A2, Th5;
then ((the_Source_of G1) | (dom (F _E))) . x in dom (F _V) by A2, FUNCT_1:49;
hence x in dom ((F _V) * ((the_Source_of G1) | (dom (F _E)))) by A3, FUNCT_1:11; :: thesis: verum

end;

assume x in dom ((F _V) * ((the_Source_of G1) | (dom (F _E)))) ; :: thesis: x in dom ((the_Source_of G2) * (F _E))
then x in dom ((the_Source_of G1) | (dom (F _E))) by FUNCT_1:11;
then A4: ( x in dom (the_Source_of G1) & x in dom (F _E) ) by RELAT_1:57;
then (F _E) . x in the_Edges_of G2 by PARTFUN1:4;
then (F _E) . x in dom (the_Source_of G2) by FUNCT_2:def 1;
hence x in dom ((the_Source_of G2) * (F _E)) by A4, FUNCT_1:11; :: thesis: verum

end;

then A5: dom ((the_Source_of G2) * (F _E)) = dom ((F _V) * ((the_Source_of G1) | (dom (F _E)))) by TARSKI:2;
for x being object st x in dom ((the_Source_of G2) * (F _E)) holds
((the_Source_of G2) * (F _E)) . x = ((F _V) * ((the_Source_of G1) | (dom (F _E)))) . x

proof

let x be object ; :: thesis: ( x in dom ((the_Source_of G2) * (F _E)) implies ((the_Source_of G2) * (F _E)) . x = ((F _V) * ((the_Source_of G1) | (dom (F _E)))) . x )
assume A6: x in dom ((the_Source_of G2) * (F _E)) ; :: thesis: ((the_Source_of G2) * (F _E)) . x = ((F _V) * ((the_Source_of G1) | (dom (F _E)))) . x
then A7: x in dom (F _E) by FUNCT_1:11;
A8: x in dom ((the_Source_of G1) | (dom (F _E))) by A5, A6, FUNCT_1:11;
thus ((the_Source_of G2) * (F _E)) . x = (the_Source_of G2) . ((F _E) . x) by A6, FUNCT_1:12
.= (F _V) . ((the_Source_of G1) . x) by A1, A7
.= (F _V) . (((the_Source_of G1) | (dom (F _E))) . x) by A8, FUNCT_1:47
.= ((F _V) * ((the_Source_of G1) | (dom (F _E)))) . x by A8, FUNCT_1:13 ; :: thesis: verum

end;

hence (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) by A5, FUNCT_1:2; :: thesis: (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E)))
for x being object holds
( x in dom ((the_Target_of G2) * (F _E)) iff x in dom ((F _V) * ((the_Target_of G1) | (dom (F _E)))) )

proof

let x be object ; :: thesis: ( x in dom ((the_Target_of G2) * (F _E)) iff x in dom ((F _V) * ((the_Target_of G1) | (dom (F _E)))) )

hereby :: thesis: ( x in dom ((F _V) * ((the_Target_of G1) | (dom (F _E)))) implies x in dom ((the_Target_of G2) * (F _E)) )

assume x in dom ((the_Target_of G2) * (F _E)) ; :: thesis: x in dom ((F _V) * ((the_Target_of G1) | (dom (F _E))))
then A9: x in dom (F _E) by FUNCT_1:11;
then x in the_Edges_of G1 ;
then x in dom (the_Target_of G1) by FUNCT_2:def 1;
then A10: x in dom ((the_Target_of G1) | (dom (F _E))) by A9, RELAT_1:57;
(the_Target_of G1) . x in dom (F _V) by A9, Th5;
then ((the_Target_of G1) | (dom (F _E))) . x in dom (F _V) by A9, FUNCT_1:49;
hence x in dom ((F _V) * ((the_Target_of G1) | (dom (F _E)))) by A10, FUNCT_1:11; :: thesis: verum

end;

assume x in dom ((F _V) * ((the_Target_of G1) | (dom (F _E)))) ; :: thesis: x in dom ((the_Target_of G2) * (F _E))
then x in dom ((the_Target_of G1) | (dom (F _E))) by FUNCT_1:11;
then A11: ( x in dom (the_Target_of G1) & x in dom (F _E) ) by RELAT_1:57;
then (F _E) . x in the_Edges_of G2 by PARTFUN1:4;
then (F _E) . x in dom (the_Target_of G2) by FUNCT_2:def 1;
hence x in dom ((the_Target_of G2) * (F _E)) by A11, FUNCT_1:11; :: thesis: verum

end;

then A12: dom ((the_Target_of G2) * (F _E)) = dom ((F _V) * ((the_Target_of G1) | (dom (F _E)))) by TARSKI:2;
for x being object st x in dom ((the_Target_of G2) * (F _E)) holds
((the_Target_of G2) * (F _E)) . x = ((F _V) * ((the_Target_of G1) | (dom (F _E)))) . x

proof

let x be object ; :: thesis: ( x in dom ((the_Target_of G2) * (F _E)) implies ((the_Target_of G2) * (F _E)) . x = ((F _V) * ((the_Target_of G1) | (dom (F _E)))) . x )
assume A13: x in dom ((the_Target_of G2) * (F _E)) ; :: thesis: ((the_Target_of G2) * (F _E)) . x = ((F _V) * ((the_Target_of G1) | (dom (F _E)))) . x
then A14: x in dom (F _E) by FUNCT_1:11;
x in dom ((F _V) * ((the_Target_of G1) | (dom (F _E)))) by A12, A13;
then A15: x in dom ((the_Target_of G1) | (dom (F _E))) by FUNCT_1:11;
thus ((the_Target_of G2) * (F _E)) . x = (the_Target_of G2) . ((F _E) . x) by A13, FUNCT_1:12
.= (F _V) . ((the_Target_of G1) . x) by A1, A14
.= (F _V) . (((the_Target_of G1) | (dom (F _E))) . x) by A15, FUNCT_1:47
.= ((F _V) * ((the_Target_of G1) | (dom (F _E)))) . x by A15, FUNCT_1:13 ; :: thesis: verum

end;

hence (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) by A12, FUNCT_1:2; :: thesis: verum

end;

assume A16: ( (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) & (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) ) ; :: thesis: F is directed

now :: thesis: for x being object st x in dom (F _E) holds
( (the_Source_of G2) . ((F _E) . x) = (F _V) . ((the_Source_of G1) . x) & (the_Target_of G2) . ((F _E) . x) = (F _V) . ((the_Target_of G1) . x) )

let x be object ; :: thesis: ( x in dom (F _E) implies ( (the_Source_of G2) . ((F _E) . x) = (F _V) . ((the_Source_of G1) . x) & (the_Target_of G2) . ((F _E) . x) = (F _V) . ((the_Target_of G1) . x) ) )
assume A17: x in dom (F _E) ; :: thesis: ( (the_Source_of G2) . ((F _E) . x) = (F _V) . ((the_Source_of G1) . x) & (the_Target_of G2) . ((F _E) . x) = (F _V) . ((the_Target_of G1) . x) )
then x in the_Edges_of G1 ;
then ( x in dom (the_Source_of G1) & x in dom (the_Target_of G1) ) by FUNCT_2:def 1;
then A18: ( x in dom ((the_Source_of G1) | (dom (F _E))) & x in dom ((the_Target_of G1) | (dom (F _E))) ) by A17, RELAT_1:57;
thus (the_Source_of G2) . ((F _E) . x) = ((the_Source_of G2) * (F _E)) . x by A17, FUNCT_1:13
.= (F _V) . (((the_Source_of G1) | (dom (F _E))) . x) by A16, A18, FUNCT_1:13
.= (F _V) . ((the_Source_of G1) . x) by A17, FUNCT_1:49 ; :: thesis: (the_Target_of G2) . ((F _E) . x) = (F _V) . ((the_Target_of G1) . x)
thus (the_Target_of G2) . ((F _E) . x) = ((the_Target_of G2) * (F _E)) . x by A17, FUNCT_1:13
.= (F _V) . (((the_Target_of G1) | (dom (F _E))) . x) by A16, A18, FUNCT_1:13
.= (F _V) . ((the_Target_of G1) . x) by A17, FUNCT_1:49 ; :: thesis: verum

end;

hence F is directed by Th13; :: thesis: verum