let G be _Graph; for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )
let v be object ; for V being set
for G1, G2 being addAdjVertexAll of G,v,V ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )
let V be set ; for G1, G2 being addAdjVertexAll of G,v,V ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )
let G1, G2 be addAdjVertexAll of G,v,V; ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )
per cases
( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G )
;
suppose A1:
(
V c= the_Vertices_of G & not
v in the_Vertices_of G )
;
ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )defpred S1[
object ,
object ]
means for
v1,
v2 being
object st $1
Joins v1,
v2,
G1 holds
$2
Joins v1,
v2,
G2;
A2:
for
e1 being
object st
e1 in the_Edges_of G1 holds
ex
e2 being
object st
(
e2 in the_Edges_of G2 &
S1[
e1,
e2] )
proof
let e1 be
object ;
( e1 in the_Edges_of G1 implies ex e2 being object st
( e2 in the_Edges_of G2 & S1[e1,e2] ) )
assume
e1 in the_Edges_of G1
;
ex e2 being object st
( e2 in the_Edges_of G2 & S1[e1,e2] )
then
e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G1
by GLIB_000:def 13;
then consider e2 being
object such that A3:
e2 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G2
by Th67;
take
e2
;
( e2 in the_Edges_of G2 & S1[e1,e2] )
thus
e2 in the_Edges_of G2
by A3, GLIB_000:def 13;
S1[e1,e2]
let v1,
v2 be
object ;
( e1 Joins v1,v2,G1 implies e2 Joins v1,v2,G2 )
assume
e1 Joins v1,
v2,
G1
;
e2 Joins v1,v2,G2
end; consider f1 being
Function of
(the_Edges_of G1),
(the_Edges_of G2) such that A4:
for
e1 being
object st
e1 in the_Edges_of G1 holds
S1[
e1,
f1 . e1]
from FUNCT_2:sch 1(A2);
set f =
f1 +* (id (the_Edges_of G));
A5:
the_Edges_of G c= the_Edges_of G1
by GLIB_006:def 9;
A6:
dom f1 = the_Edges_of G1
A9:
dom (f1 +* (id (the_Edges_of G))) =
(dom f1) \/ (dom (id (the_Edges_of G)))
by FUNCT_4:def 1
.=
the_Edges_of G1
by A5, A6, XBOOLE_1:12
;
A10:
rng (id (the_Edges_of G)) c= the_Edges_of G2
by GLIB_006:def 9;
A11:
(rng f1) \/ (rng (id (the_Edges_of G))) c= the_Edges_of G2
by A10, XBOOLE_1:8;
rng (f1 +* (id (the_Edges_of G))) c= (rng f1) \/ (rng (id (the_Edges_of G)))
by FUNCT_4:17;
then reconsider f =
f1 +* (id (the_Edges_of G)) as
Function of
(the_Edges_of G1),
(the_Edges_of G2) by A9, FUNCT_2:2, A11, XBOOLE_1:1;
take
f
;
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )thus f | (the_Edges_of G) =
f | (dom (id (the_Edges_of G)))
.=
id (the_Edges_of G)
;
( f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )consider E1 being
set such that
card V = card E1
and A12:
(
E1 misses the_Edges_of G &
the_Edges_of G1 = (the_Edges_of G) \/ E1 )
and A13:
for
v1 being
object st
v1 in V holds
ex
e1 being
object st
(
e1 in E1 &
e1 Joins v1,
v,
G1 & ( for
e2 being
object st
e2 Joins v1,
v,
G1 holds
e1 = e2 ) )
by A1, Def4;
consider E2 being
set such that
card V = card E2
and A14:
(
E2 misses the_Edges_of G &
the_Edges_of G2 = (the_Edges_of G) \/ E2 )
and A15:
for
v1 being
object st
v1 in V holds
ex
e1 being
object st
(
e1 in E2 &
e1 Joins v1,
v,
G2 & ( for
e2 being
object st
e2 Joins v1,
v,
G2 holds
e1 = e2 ) )
by A1, Def4;
for
e1,
e2 being
object st
e1 in dom f &
e2 in dom f &
f . e1 = f . e2 holds
e1 = e2
proof
let e1,
e2 be
object ;
( e1 in dom f & e2 in dom f & f . e1 = f . e2 implies e1 = e2 )
assume that A16:
(
e1 in dom f &
e2 in dom f )
and A17:
f . e1 = f . e2
;
e1 = e2
set x1 =
(the_Source_of G1) . e1;
set y1 =
(the_Target_of G1) . e1;
set x2 =
(the_Source_of G1) . e2;
set y2 =
(the_Target_of G1) . e2;
A18:
(
e1 in the_Edges_of G1 &
e2 in the_Edges_of G1 )
by A16;
per cases
( ( e1 in the_Edges_of G & e2 in the_Edges_of G ) or ( not e1 in the_Edges_of G & e2 in the_Edges_of G ) or ( not e2 in the_Edges_of G & e1 in the_Edges_of G ) or ( not e1 in the_Edges_of G & not e2 in the_Edges_of G ) )
;
suppose A20:
( not
e1 in the_Edges_of G &
e2 in the_Edges_of G )
;
e1 = e2then
( not
e1 in dom (id (the_Edges_of G)) &
e2 in dom (id (the_Edges_of G)) )
;
then A21:
(
f . e1 = f1 . e1 &
f . e2 = (id (the_Edges_of G)) . e2 )
by FUNCT_4:11, FUNCT_4:13;
A22:
e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G1
by A18, GLIB_000:def 13;
then A23:
( not
(the_Source_of G1) . e1 in the_Vertices_of G or not
(the_Target_of G1) . e1 in the_Vertices_of G )
by A1, A12, A20, Th51;
e2 Joins (the_Source_of G1) . e2,
(the_Target_of G1) . e2,
G1
by A18, GLIB_000:def 13;
then A24:
e2 Joins (the_Source_of G1) . e2,
(the_Target_of G1) . e2,
G
by A20, GLIB_006:72;
then A25:
(
(the_Source_of G1) . e2 in the_Vertices_of G &
(the_Target_of G1) . e2 in the_Vertices_of G )
by GLIB_000:13;
A26:
f . e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G2
by A21, A18, A22, A4;
A27:
e2 Joins (the_Source_of G1) . e2,
(the_Target_of G1) . e2,
G2
by A24, GLIB_006:70;
f . e2 = e2
by A20, A21, FUNCT_1:18;
hence
e1 = e2
by A23, A25, A26, GLIB_000:15, A17, A27;
verum end; suppose A28:
( not
e2 in the_Edges_of G &
e1 in the_Edges_of G )
;
e1 = e2then
( not
e2 in dom (id (the_Edges_of G)) &
e1 in dom (id (the_Edges_of G)) )
;
then A29:
(
f . e2 = f1 . e2 &
f . e1 = (id (the_Edges_of G)) . e1 )
by FUNCT_4:11, FUNCT_4:13;
A30:
e2 Joins (the_Source_of G1) . e2,
(the_Target_of G1) . e2,
G1
by A18, GLIB_000:def 13;
then
(
e2 in E1 & ( (
(the_Source_of G1) . e2 = v &
(the_Target_of G1) . e2 in V ) or (
(the_Target_of G1) . e2 = v &
(the_Source_of G1) . e2 in V ) ) )
by A1, A12, A28, Th51;
then A31:
( not
(the_Source_of G1) . e2 in the_Vertices_of G or not
(the_Target_of G1) . e2 in the_Vertices_of G )
by A1;
e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G1
by A18, GLIB_000:def 13;
then A32:
e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G
by A28, GLIB_006:72;
then A33:
(
(the_Source_of G1) . e1 in the_Vertices_of G &
(the_Target_of G1) . e1 in the_Vertices_of G )
by GLIB_000:13;
A34:
f . e2 Joins (the_Source_of G1) . e2,
(the_Target_of G1) . e2,
G2
by A29, A18, A30, A4;
A35:
e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G2
by A32, GLIB_006:70;
f . e1 = e1
by A28, A29, FUNCT_1:18;
then
f . e2 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G2
by A17, A35;
hence
e1 = e2
by A31, A33, A34, GLIB_000:15;
verum end; suppose A36:
( not
e1 in the_Edges_of G & not
e2 in the_Edges_of G )
;
e1 = e2then
( not
e1 in dom (id (the_Edges_of G)) & not
e2 in dom (id (the_Edges_of G)) )
;
then A37:
(
f . e1 = f1 . e1 &
f . e2 = f1 . e2 )
by FUNCT_4:11;
A38:
e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G1
by A18, GLIB_000:def 13;
then A39:
(
e1 in E1 & ( (
(the_Source_of G1) . e1 = v &
(the_Target_of G1) . e1 in V ) or (
(the_Target_of G1) . e1 = v &
(the_Source_of G1) . e1 in V ) ) )
by A1, A12, A36, Th51;
A40:
e2 Joins (the_Source_of G1) . e2,
(the_Target_of G1) . e2,
G1
by A18, GLIB_000:def 13;
A41:
f . e1 Joins (the_Source_of G1) . e1,
(the_Target_of G1) . e1,
G2
by A18, A38, A37, A4;
f . e2 Joins (the_Source_of G1) . e2,
(the_Target_of G1) . e2,
G2
by A18, A40, A37, A4;
per cases then
( ( (the_Source_of G1) . e1 = (the_Source_of G1) . e2 & (the_Target_of G1) . e1 = (the_Target_of G1) . e2 ) or ( (the_Source_of G1) . e1 = (the_Target_of G1) . e2 & (the_Target_of G1) . e1 = (the_Source_of G1) . e2 ) )
by A17, A41, GLIB_000:15;
suppose A42:
(
(the_Source_of G1) . e1 = (the_Source_of G1) . e2 &
(the_Target_of G1) . e1 = (the_Target_of G1) . e2 )
;
e1 = e2per cases
( ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 in V ) or ( (the_Target_of G1) . e1 = v & (the_Source_of G1) . e1 in V ) )
by A39;
suppose A43:
(
(the_Source_of G1) . e1 = v &
(the_Target_of G1) . e1 in V )
;
e1 = e2then consider e being
object such that
(
e in E1 &
e Joins (the_Target_of G1) . e1,
v,
G1 )
and A44:
for
e3 being
object st
e3 Joins (the_Target_of G1) . e1,
v,
G1 holds
e = e3
by A13;
e1 = e
by A44, A38, A43, GLIB_000:14;
hence
e1 = e2
by A44, A40, A42, A43, GLIB_000:14;
verum end; suppose A46:
(
(the_Target_of G1) . e1 = v &
(the_Source_of G1) . e1 in V )
;
e1 = e2then consider e being
object such that
(
e in E1 &
e Joins (the_Source_of G1) . e1,
v,
G1 )
and A47:
for
e3 being
object st
e3 Joins (the_Source_of G1) . e1,
v,
G1 holds
e = e3
by A13;
e1 Joins (the_Source_of G1) . e1,
v,
G1
by A38, A46;
then
e1 = e
by A47;
hence
e1 = e2
by A47, A40, A42, A46;
verum end; end; end; suppose A49:
(
(the_Source_of G1) . e1 = (the_Target_of G1) . e2 &
(the_Target_of G1) . e1 = (the_Source_of G1) . e2 )
;
e1 = e2per cases
( ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 in V ) or ( (the_Target_of G1) . e1 = v & (the_Source_of G1) . e1 in V ) )
by A39;
suppose A50:
(
(the_Source_of G1) . e1 = v &
(the_Target_of G1) . e1 in V )
;
e1 = e2then consider e being
object such that
(
e in E1 &
e Joins (the_Target_of G1) . e1,
v,
G1 )
and A51:
for
e3 being
object st
e3 Joins (the_Target_of G1) . e1,
v,
G1 holds
e = e3
by A13;
e1 = e
by A51, A38, A50, GLIB_000:14;
hence
e1 = e2
by A51, A40, A49, A50;
verum end; suppose A53:
(
(the_Target_of G1) . e1 = v &
(the_Source_of G1) . e1 in V )
;
e1 = e2then consider e being
object such that
(
e in E1 &
e Joins (the_Source_of G1) . e1,
v,
G1 )
and A54:
for
e3 being
object st
e3 Joins (the_Source_of G1) . e1,
v,
G1 holds
e = e3
by A13;
e1 Joins (the_Source_of G1) . e1,
v,
G1
by A38, A53;
then A55:
e1 = e
by A54;
e2 Joins (the_Source_of G1) . e1,
v,
G1
by A40, A49, A53, GLIB_000:14;
hence
e1 = e2
by A54, A55;
verum end; end; end; end; end; end;
end; hence
f is
one-to-one
by FUNCT_1:def 4;
( f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )
for
e being
object st
e in the_Edges_of G2 holds
e in rng f
proof
let e be
object ;
( e in the_Edges_of G2 implies e in rng f )
assume A56:
e in the_Edges_of G2
;
e in rng f
per cases
( e in the_Edges_of G or not e in the_Edges_of G )
;
suppose A59:
not
e in the_Edges_of G
;
e in rng fset v1 =
(the_Source_of G2) . e;
set v2 =
(the_Target_of G2) . e;
A60:
e Joins (the_Source_of G2) . e,
(the_Target_of G2) . e,
G2
by A56, GLIB_000:def 13;
per cases then
( ( (the_Source_of G2) . e = v & (the_Target_of G2) . e in V ) or ( (the_Target_of G2) . e = v & (the_Source_of G2) . e in V ) )
by A1, A14, A59, Th51;
suppose A61:
(
(the_Source_of G2) . e = v &
(the_Target_of G2) . e in V )
;
e in rng fthen consider e1 being
object such that A62:
(
e1 in E1 &
e1 Joins (the_Target_of G2) . e,
v,
G1 )
and
for
e2 being
object st
e2 Joins (the_Target_of G2) . e,
v,
G1 holds
e1 = e2
by A13;
A63:
e1 in the_Edges_of G1
by A62, GLIB_000:def 13;
then A64:
f1 . e1 Joins (the_Target_of G2) . e,
v,
G2
by A62, A4;
E1 /\ (the_Edges_of G) = {}
by A12, XBOOLE_0:def 7;
then
not
e1 in dom (id (the_Edges_of G))
by A62, Lm7;
then A65:
f . e1 Joins (the_Target_of G2) . e,
v,
G2
by A64, FUNCT_4:11;
consider e3 being
object such that
(
e3 in E2 &
e3 Joins (the_Target_of G2) . e,
v,
G2 )
and A66:
for
e2 being
object st
e2 Joins (the_Target_of G2) . e,
v,
G2 holds
e3 = e2
by A15, A61;
f . e1 = e3
by A65, A66;
then
f . e1 = e
by A66, A61, A60, GLIB_000:14;
hence
e in rng f
by A63, A9, FUNCT_1:def 3;
verum end; suppose A68:
(
(the_Target_of G2) . e = v &
(the_Source_of G2) . e in V )
;
e in rng fthen consider e1 being
object such that A69:
(
e1 in E1 &
e1 Joins (the_Source_of G2) . e,
v,
G1 )
and
for
e2 being
object st
e2 Joins (the_Source_of G2) . e,
v,
G1 holds
e1 = e2
by A13;
A70:
e1 in the_Edges_of G1
by A69, GLIB_000:def 13;
then A71:
f1 . e1 Joins (the_Source_of G2) . e,
v,
G2
by A69, A4;
E1 /\ (the_Edges_of G) = {}
by A12, XBOOLE_0:def 7;
then
not
e1 in dom (id (the_Edges_of G))
by A69, Lm7;
then A72:
f . e1 Joins (the_Source_of G2) . e,
v,
G2
by A71, FUNCT_4:11;
consider e3 being
object such that
(
e3 in E2 &
e3 Joins (the_Source_of G2) . e,
v,
G2 )
and A73:
for
e2 being
object st
e2 Joins (the_Source_of G2) . e,
v,
G2 holds
e3 = e2
by A15, A68;
f . e1 = e3
by A72, A73;
then
f . e1 = e
by A73, A68, A60;
hence
e in rng f
by A70, A9, FUNCT_1:def 3;
verum end; end; end; end;
end; then
the_Edges_of G2 c= rng f
by TARSKI:def 3;
hence
f is
onto
by FUNCT_2:def 3, XBOOLE_0:def 10;
for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2let v1,
e,
v2 be
object ;
( e Joins v1,v2,G1 implies f . e Joins v1,v2,G2 )assume A75:
e Joins v1,
v2,
G1
;
f . e Joins v1,v2,G2 end; suppose
( not
V c= the_Vertices_of G or
v in the_Vertices_of G )
;
ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )then A79:
(
G1 == G &
G2 == G )
by Def4;
then A80:
(
the_Edges_of G1 = the_Edges_of G &
the_Edges_of G2 = the_Edges_of G )
by GLIB_000:def 34;
set f =
id (the_Edges_of G);
reconsider f =
id (the_Edges_of G) as
Function of
(the_Edges_of G1),
(the_Edges_of G2) by A80;
take
f
;
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )thus
f | (the_Edges_of G) = id (the_Edges_of G)
;
( f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )thus
(
f is
one-to-one &
f is
onto )
by A80;
for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2let v1,
e,
v2 be
object ;
( e Joins v1,v2,G1 implies f . e Joins v1,v2,G2 )assume A81:
e Joins v1,
v2,
G1
;
f . e Joins v1,v2,G2
G1 == G2
by A79, GLIB_000:85;
then A82:
e Joins v1,
v2,
G2
by A81, GLIB_000:88;
e in the_Edges_of G1
by A81, GLIB_000:def 13;
hence
f . e Joins v1,
v2,
G2
by A80, A82, FUNCT_1:18;
verum end; end;