let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2

for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 holds

(F _E) . e Joins (F _V) . v,(F _V) . w,G2

let F be PGraphMapping of G1,G2; :: thesis: for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 holds

(F _E) . e Joins (F _V) . v,(F _V) . w,G2

let e, v, w be object ; :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 implies (F _E) . e Joins (F _V) . v,(F _V) . w,G2 )

assume A1: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( not e Joins v,w,G1 or (F _E) . e Joins (F _V) . v,(F _V) . w,G2 )

consider f, g being Function such that

A2: F = [f,g] and

( dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) ) and

A3: for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 by Def8;

thus ( not e Joins v,w,G1 or (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) by A1, A2, A3; :: thesis: verum

for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 holds

(F _E) . e Joins (F _V) . v,(F _V) . w,G2

let F be PGraphMapping of G1,G2; :: thesis: for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 holds

(F _E) . e Joins (F _V) . v,(F _V) . w,G2

let e, v, w be object ; :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 implies (F _E) . e Joins (F _V) . v,(F _V) . w,G2 )

assume A1: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( not e Joins v,w,G1 or (F _E) . e Joins (F _V) . v,(F _V) . w,G2 )

consider f, g being Function such that

A2: F = [f,g] and

( dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) ) and

A3: for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 by Def8;

thus ( not e Joins v,w,G1 or (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) by A1, A2, A3; :: thesis: verum