let G1, G2 be _Graph; :: thesis: for f being PartFunc of (),()
for g being PartFunc of (),() st ( for e being object st e in dom g holds
( () . e in dom f & () . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G1 holds
g . e DJoins f . v,f . w,G2 ) holds
[f,g] is directed PGraphMapping of G1,G2

let f be PartFunc of (),(); :: thesis: for g being PartFunc of (),() st ( for e being object st e in dom g holds
( () . e in dom f & () . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G1 holds
g . e DJoins f . v,f . w,G2 ) holds
[f,g] is directed PGraphMapping of G1,G2

let g be PartFunc of (),(); :: thesis: ( ( for e being object st e in dom g holds
( () . e in dom f & () . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G1 holds
g . e DJoins f . v,f . w,G2 ) implies [f,g] is directed PGraphMapping of G1,G2 )

assume that
A1: for e being object st e in dom g holds
( () . e in dom f & () . e in dom f ) and
A2: for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G1 holds
g . e DJoins f . v,f . w,G2 ; :: thesis: [f,g] is directed PGraphMapping of G1,G2
A3: now :: thesis: 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
let e, v, w be object ; :: thesis: ( e in dom g & v in dom f & w in dom f & e Joins v,w,G1 implies g . b1 Joins f . b2,f . b3,G2 )
assume A4: ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G1 implies g . b1 Joins f . b2,f . b3,G2 )
assume e Joins v,w,G1 ; :: thesis: g . b1 Joins f . b2,f . b3,G2
per cases then ( e DJoins v,w,G1 or e DJoins w,v,G1 ) by GLIB_000:16;
suppose e DJoins v,w,G1 ; :: thesis: g . b1 Joins f . b2,f . b3,G2
then g . e DJoins f . v,f . w,G2 by A2, A4;
hence g . e Joins f . v,f . w,G2 by GLIB_000:16; :: thesis: verum
end;
suppose e DJoins w,v,G1 ; :: thesis: g . b1 Joins f . b2,f . b3,G2
then g . e DJoins f . w,f . v,G2 by A2, A4;
hence g . e Joins f . v,f . w,G2 by GLIB_000:16; :: thesis: verum
end;
end;
end;
reconsider F = [f,g] as PGraphMapping of G1,G2 by A1, A3, Th8;
F is directed by A2;
hence [f,g] is directed PGraphMapping of G1,G2 ; :: thesis: verum