let G1, G2 be _Graph; for f being directed PVertexMapping of G1,G2
for E1 being RepDEdgeSelection of G1
for E2 being RepDEdgeSelection of G2 ex F being directed PGraphMapping of G1,G2 st
( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )
let f be directed PVertexMapping of G1,G2; for E1 being RepDEdgeSelection of G1
for E2 being RepDEdgeSelection of G2 ex F being directed PGraphMapping of G1,G2 st
( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )
let E1 be RepDEdgeSelection of G1; for E2 being RepDEdgeSelection of G2 ex F being directed PGraphMapping of G1,G2 st
( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )
let E2 be RepDEdgeSelection of G2; ex F being directed PGraphMapping of G1,G2 st
( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )
defpred S1[ object , object ] means ex v, w being object st
( v in dom f & w in dom f & $1 in E1 & $2 in E2 & $1 DJoins v,w,G1 & $2 DJoins f . v,f . w,G2 );
A1:
for e1, e2, e3 being object st e1 in E1 /\ (G1 .edgesBetween (dom f)) & S1[e1,e2] & S1[e1,e3] holds
e2 = e3
proof
let e1,
e2,
e3 be
object ;
( e1 in E1 /\ (G1 .edgesBetween (dom f)) & S1[e1,e2] & S1[e1,e3] implies e2 = e3 )
assume A2:
(
e1 in E1 /\ (G1 .edgesBetween (dom f)) &
S1[
e1,
e2] &
S1[
e1,
e3] )
;
e2 = e3
then consider v2,
w2 being
object such that A3:
(
v2 in dom f &
w2 in dom f &
e1 in E1 &
e2 in E2 &
e1 DJoins v2,
w2,
G1 &
e2 DJoins f . v2,
f . w2,
G2 )
;
consider v3,
w3 being
object such that A4:
(
v3 in dom f &
w3 in dom f &
e1 in E1 &
e3 in E2 &
e1 DJoins v3,
w3,
G1 &
e3 DJoins f . v3,
f . w3,
G2 )
by A2;
A5:
(
v2 = v3 &
w2 = w3 )
by A3, A4, GLIB_009:6;
then consider e0 being
object such that
(
e0 DJoins f . v2,
f . w2,
G2 &
e0 in E2 )
and A6:
for
e9 being
object st
e9 DJoins f . v2,
f . w2,
G2 &
e9 in E2 holds
e9 = e0
by A4, GLIB_009:def 6;
(
e2 = e0 &
e3 = e0 )
by A3, A4, A5, A6;
hence
e2 = e3
;
verum
end;
A7:
for e1 being object st e1 in E1 /\ (G1 .edgesBetween (dom f)) holds
ex e2 being object st S1[e1,e2]
proof
let e1 be
object ;
( e1 in E1 /\ (G1 .edgesBetween (dom f)) implies ex e2 being object st S1[e1,e2] )
set v =
(the_Source_of G1) . e1;
set w =
(the_Target_of G1) . e1;
assume A8:
e1 in E1 /\ (G1 .edgesBetween (dom f))
;
ex e2 being object st S1[e1,e2]
then
e1 in G1 .edgesBetween (dom f)
by XBOOLE_0:def 4;
then A9:
(
e1 in the_Edges_of G1 &
(the_Source_of G1) . e1 in dom f &
(the_Target_of G1) . e1 in dom f )
by GLIB_000:31;
then A10:
e1 DJoins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G1
by GLIB_000:def 14;
then consider e0 being
object such that A11:
e0 DJoins f . ((the_Source_of G1) . e1),
f . ((the_Target_of G1) . e1),
G2
by A9, Def2;
consider e2 being
object such that A12:
(
e2 DJoins f . ((the_Source_of G1) . e1),
f . ((the_Target_of G1) . e1),
G2 &
e2 in E2 )
and
for
e9 being
object st
e9 DJoins f . ((the_Source_of G1) . e1),
f . ((the_Target_of G1) . e1),
G2 &
e9 in E2 holds
e9 = e2
by A11, GLIB_009:def 6;
take
e2
;
S1[e1,e2]
take
(the_Source_of G1) . e1
;
ex w being object st
( (the_Source_of G1) . e1 in dom f & w in dom f & e1 in E1 & e2 in E2 & e1 DJoins (the_Source_of G1) . e1,w,G1 & e2 DJoins f . ((the_Source_of G1) . e1),f . w,G2 )
take
(the_Target_of G1) . e1
;
( (the_Source_of G1) . e1 in dom f & (the_Target_of G1) . e1 in dom f & e1 in E1 & e2 in E2 & e1 DJoins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 & e2 DJoins f . ((the_Source_of G1) . e1),f . ((the_Target_of G1) . e1),G2 )
thus
(
(the_Source_of G1) . e1 in dom f &
(the_Target_of G1) . e1 in dom f &
e1 in E1 )
by A8, A9, XBOOLE_0:def 4;
( e2 in E2 & e1 DJoins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 & e2 DJoins f . ((the_Source_of G1) . e1),f . ((the_Target_of G1) . e1),G2 )
thus
(
e2 in E2 &
e1 DJoins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G1 &
e2 DJoins f . ((the_Source_of G1) . e1),
f . ((the_Target_of G1) . e1),
G2 )
by A10, A12;
verum
end;
consider g being Function such that
A13:
dom g = E1 /\ (G1 .edgesBetween (dom f))
and
A14:
for e1 being object st e1 in E1 /\ (G1 .edgesBetween (dom f)) holds
S1[e1,g . e1]
from FUNCT_1:sch 2(A1, A7);
for y being object st y in rng g holds
y in E2 /\ (G2 .edgesBetween (rng f))
proof
let y be
object ;
( y in rng g implies y in E2 /\ (G2 .edgesBetween (rng f)) )
assume
y in rng g
;
y in E2 /\ (G2 .edgesBetween (rng f))
then consider x being
object such that A15:
(
x in dom g &
g . x = y )
by FUNCT_1:def 3;
consider v,
w being
object such that A16:
(
v in dom f &
w in dom f &
x in E1 &
g . x in E2 )
and A17:
(
x DJoins v,
w,
G1 &
g . x DJoins f . v,
f . w,
G2 )
by A13, A14, A15;
(
f . v in rng f &
f . w in rng f )
by A16, FUNCT_1:3;
then
(
(the_Source_of G2) . y in rng f &
(the_Target_of G2) . y in rng f &
y in the_Edges_of G2 )
by A15, A17, GLIB_000:def 14;
then
y in G2 .edgesBetween (rng f)
by GLIB_000:31;
hence
y in E2 /\ (G2 .edgesBetween (rng f))
by A15, A16, XBOOLE_0:def 4;
verum
end;
then A18:
rng g c= E2 /\ (G2 .edgesBetween (rng f))
by TARSKI:def 3;
rng g c= the_Edges_of G2
by A18, XBOOLE_1:1;
then reconsider g = g as PartFunc of (the_Edges_of G1),(the_Edges_of G2) by A13, RELSET_1:4;
now ( ( 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 ) ) & ( 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 ) )let e,
v,
w be
object ;
( e in dom g & v in dom f & w in dom f & e DJoins v,w,G1 implies g . e DJoins f . v,f . w,G2 )assume
(
e in dom g &
v in dom f &
w in dom f )
;
( e DJoins v,w,G1 implies g . e DJoins f . v,f . w,G2 )then consider v0,
w0 being
object such that
(
v0 in dom f &
w0 in dom f &
e in E1 &
g . e in E2 )
and A20:
(
e DJoins v0,
w0,
G1 &
g . e DJoins f . v0,
f . w0,
G2 )
by A13, A14;
assume
e DJoins v,
w,
G1
;
g . e DJoins f . v,f . w,G2then
(
v = v0 &
w = w0 )
by A20, GLIB_009:6;
hence
g . e DJoins f . v,
f . w,
G2
by A20;
verum end;
then reconsider F = [f,g] as directed PGraphMapping of G1,G2 by GLIB_010:30;
take
F
; ( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )
thus
( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )
by A13, A18; verum