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

let F be PGraphMapping of G1,G2; :: thesis: ( F is directed iff ( () * (F _E) = (F _V) * (() | (dom (F _E))) & () * (F _E) = (F _V) * (() | (dom (F _E))) ) )
hereby :: thesis: ( () * (F _E) = (F _V) * (() | (dom (F _E))) & () * (F _E) = (F _V) * (() | (dom (F _E))) implies F is directed )
assume F is directed ; :: thesis: ( () * (F _E) = (F _V) * (() | (dom (F _E))) & () * (F _E) = (F _V) * (() | (dom (F _E))) )
then A1: for e being object st e in dom (F _E) holds
( () . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . e) ) by Th13;
for x being object holds
( x in dom (() * (F _E)) iff x in dom ((F _V) * (() | (dom (F _E)))) )
proof
let x be object ; :: thesis: ( x in dom (() * (F _E)) iff x in dom ((F _V) * (() | (dom (F _E)))) )
hereby :: thesis: ( x in dom ((F _V) * (() | (dom (F _E)))) implies x in dom (() * (F _E)) )
assume x in dom (() * (F _E)) ; :: thesis: x in dom ((F _V) * (() | (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 () by FUNCT_2:def 1;
then A3: x in dom (() | (dom (F _E))) by ;
(the_Source_of G1) . x in dom (F _V) by ;
then ((the_Source_of G1) | (dom (F _E))) . x in dom (F _V) by ;
hence x in dom ((F _V) * (() | (dom (F _E)))) by ; :: thesis: verum
end;
assume x in dom ((F _V) * (() | (dom (F _E)))) ; :: thesis: x in dom (() * (F _E))
then x in dom (() | (dom (F _E))) by FUNCT_1:11;
then A4: ( x in dom () & 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 () by FUNCT_2:def 1;
hence x in dom (() * (F _E)) by ; :: thesis: verum
end;
then A5: dom (() * (F _E)) = dom ((F _V) * (() | (dom (F _E)))) by TARSKI:2;
for x being object st x in dom (() * (F _E)) holds
(() * (F _E)) . x = ((F _V) * (() | (dom (F _E)))) . x
proof
let x be object ; :: thesis: ( x in dom (() * (F _E)) implies (() * (F _E)) . x = ((F _V) * (() | (dom (F _E)))) . x )
assume A6: x in dom (() * (F _E)) ; :: thesis: (() * (F _E)) . x = ((F _V) * (() | (dom (F _E)))) . x
then A7: x in dom (F _E) by FUNCT_1:11;
A8: x in dom (() | (dom (F _E))) by ;
thus (() * (F _E)) . x = () . ((F _E) . x) by
.= (F _V) . (() . x) by A1, A7
.= (F _V) . ((() | (dom (F _E))) . x) by
.= ((F _V) * (() | (dom (F _E)))) . x by ; :: thesis: verum
end;
hence (the_Source_of G2) * (F _E) = (F _V) * (() | (dom (F _E))) by ; :: thesis: () * (F _E) = (F _V) * (() | (dom (F _E)))
for x being object holds
( x in dom (() * (F _E)) iff x in dom ((F _V) * (() | (dom (F _E)))) )
proof
let x be object ; :: thesis: ( x in dom (() * (F _E)) iff x in dom ((F _V) * (() | (dom (F _E)))) )
hereby :: thesis: ( x in dom ((F _V) * (() | (dom (F _E)))) implies x in dom (() * (F _E)) )
assume x in dom (() * (F _E)) ; :: thesis: x in dom ((F _V) * (() | (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 () by FUNCT_2:def 1;
then A10: x in dom (() | (dom (F _E))) by ;
(the_Target_of G1) . x in dom (F _V) by ;
then ((the_Target_of G1) | (dom (F _E))) . x in dom (F _V) by ;
hence x in dom ((F _V) * (() | (dom (F _E)))) by ; :: thesis: verum
end;
assume x in dom ((F _V) * (() | (dom (F _E)))) ; :: thesis: x in dom (() * (F _E))
then x in dom (() | (dom (F _E))) by FUNCT_1:11;
then A11: ( x in dom () & 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 () by FUNCT_2:def 1;
hence x in dom (() * (F _E)) by ; :: thesis: verum
end;
then A12: dom (() * (F _E)) = dom ((F _V) * (() | (dom (F _E)))) by TARSKI:2;
for x being object st x in dom (() * (F _E)) holds
(() * (F _E)) . x = ((F _V) * (() | (dom (F _E)))) . x
proof
let x be object ; :: thesis: ( x in dom (() * (F _E)) implies (() * (F _E)) . x = ((F _V) * (() | (dom (F _E)))) . x )
assume A13: x in dom (() * (F _E)) ; :: thesis: (() * (F _E)) . x = ((F _V) * (() | (dom (F _E)))) . x
then A14: x in dom (F _E) by FUNCT_1:11;
x in dom ((F _V) * (() | (dom (F _E)))) by ;
then A15: x in dom (() | (dom (F _E))) by FUNCT_1:11;
thus (() * (F _E)) . x = () . ((F _E) . x) by
.= (F _V) . (() . x) by
.= (F _V) . ((() | (dom (F _E))) . x) by
.= ((F _V) * (() | (dom (F _E)))) . x by ; :: thesis: verum
end;
hence (the_Target_of G2) * (F _E) = (F _V) * (() | (dom (F _E))) by ; :: thesis: verum
end;
assume A16: ( (the_Source_of G2) * (F _E) = (F _V) * (() | (dom (F _E))) & () * (F _E) = (F _V) * (() | (dom (F _E))) ) ; :: thesis: F is directed
now :: thesis: for x being object st x in dom (F _E) holds
( () . ((F _E) . x) = (F _V) . (() . x) & () . ((F _E) . x) = (F _V) . (() . x) )
let x be object ; :: thesis: ( x in dom (F _E) implies ( () . ((F _E) . x) = (F _V) . (() . x) & () . ((F _E) . x) = (F _V) . (() . x) ) )
assume A17: x in dom (F _E) ; :: thesis: ( () . ((F _E) . x) = (F _V) . (() . x) & () . ((F _E) . x) = (F _V) . (() . x) )
then x in the_Edges_of G1 ;
then ( x in dom () & x in dom () ) by FUNCT_2:def 1;
then A18: ( x in dom (() | (dom (F _E))) & x in dom (() | (dom (F _E))) ) by ;
thus () . ((F _E) . x) = (() * (F _E)) . x by
.= (F _V) . ((() | (dom (F _E))) . x) by
.= (F _V) . (() . x) by ; :: thesis: () . ((F _E) . x) = (F _V) . (() . x)
thus () . ((F _E) . x) = (() * (F _E)) . x by
.= (F _V) . ((() | (dom (F _E))) . x) by
.= (F _V) . (() . x) by ; :: thesis: verum
end;
hence F is directed by Th13; :: thesis: verum