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

( 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 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 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)))) )

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

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

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

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

then A5:
dom ((the_Source_of G2) * (F _E)) = dom ((F _V) * ((the_Source_of G1) | (dom (F _E))))
by TARSKI:2;
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)))) )

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;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 ((F _V) * ((the_Source_of G1) | (dom (F _E))))
; :: thesis: 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;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

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

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

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

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

then A12:
dom ((the_Target_of G2) * (F _E)) = dom ((F _V) * ((the_Target_of G1) | (dom (F _E))))
by TARSKI:2;
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)))) )

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;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 ((F _V) * ((the_Target_of G1) | (dom (F _E))))
; :: thesis: 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;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

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

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

hence
(the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E)))
by A12, FUNCT_1:2; :: thesis: verum
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;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

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

hence
F is directed
by Th13; :: thesis: verum( (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;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