:: About Graph Mappings
:: by Sebastian Koch
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


:: into FUNCT_1 ?
theorem Th1: :: GLIB_010:1
for A, B, C, D being Function st D * A = C | (dom A) holds
(D | (dom B)) * A = C | (dom (B * A))
proof end;

:: into FUNCT_1 ?
theorem Th2: :: GLIB_010:2
for A being one-to-one Function
for C, D being Function st D * A = C | (dom A) holds
C * (A ") = D | (dom (A "))
proof end;

:: BEGIN into GLIB_003 ?
registration
let G be non _finite _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> non _finite ;
coherence
not G .set (WeightSelector,X) is _finite
proof end;
cluster G .set (ELabelSelector,X) -> non _finite ;
coherence
not G .set (ELabelSelector,X) is _finite
proof end;
cluster G .set (VLabelSelector,X) -> non _finite ;
coherence
not G .set (VLabelSelector,X) is _finite
proof end;
end;

registration
let G be non loopless _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> non loopless ;
coherence
not G .set (WeightSelector,X) is loopless
proof end;
cluster G .set (ELabelSelector,X) -> non loopless ;
coherence
not G .set (ELabelSelector,X) is loopless
proof end;
cluster G .set (VLabelSelector,X) -> non loopless ;
coherence
not G .set (VLabelSelector,X) is loopless
proof end;
end;

registration
let G be non non-multi _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> non non-multi ;
coherence
not G .set (WeightSelector,X) is non-multi
proof end;
cluster G .set (ELabelSelector,X) -> non non-multi ;
coherence
not G .set (ELabelSelector,X) is non-multi
proof end;
cluster G .set (VLabelSelector,X) -> non non-multi ;
coherence
not G .set (VLabelSelector,X) is non-multi
proof end;
end;

registration
let G be non non-Dmulti _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> non non-Dmulti ;
coherence
not G .set (WeightSelector,X) is non-Dmulti
proof end;
cluster G .set (ELabelSelector,X) -> non non-Dmulti ;
coherence
not G .set (ELabelSelector,X) is non-Dmulti
proof end;
cluster G .set (VLabelSelector,X) -> non non-Dmulti ;
coherence
not G .set (VLabelSelector,X) is non-Dmulti
proof end;
end;

registration
let G be non connected _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> non connected ;
coherence
not G .set (WeightSelector,X) is connected
proof end;
cluster G .set (ELabelSelector,X) -> non connected ;
coherence
not G .set (ELabelSelector,X) is connected
proof end;
cluster G .set (VLabelSelector,X) -> non connected ;
coherence
not G .set (VLabelSelector,X) is connected
proof end;
end;

registration
let G be non acyclic _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> non acyclic ;
coherence
not G .set (WeightSelector,X) is acyclic
proof end;
cluster G .set (ELabelSelector,X) -> non acyclic ;
coherence
not G .set (ELabelSelector,X) is acyclic
proof end;
cluster G .set (VLabelSelector,X) -> non acyclic ;
coherence
not G .set (VLabelSelector,X) is acyclic
proof end;
end;

definition
let G be _Graph;
attr G is elabel-full means :Def1: :: GLIB_010:def 1
( ELabelSelector in dom G & ex f being ManySortedSet of the_Edges_of G st G . ELabelSelector = f );
attr G is vlabel-full means :Def2: :: GLIB_010:def 2
( VLabelSelector in dom G & ex f being ManySortedSet of the_Vertices_of G st G . VLabelSelector = f );
end;

:: deftheorem Def1 defines elabel-full GLIB_010:def 1 :
for G being _Graph holds
( G is elabel-full iff ( ELabelSelector in dom G & ex f being ManySortedSet of the_Edges_of G st G . ELabelSelector = f ) );

:: deftheorem Def2 defines vlabel-full GLIB_010:def 2 :
for G being _Graph holds
( G is vlabel-full iff ( VLabelSelector in dom G & ex f being ManySortedSet of the_Vertices_of G st G . VLabelSelector = f ) );

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] elabel-full -> [ELabeled] for set ;
coherence
for b1 being _Graph st b1 is elabel-full holds
b1 is [ELabeled]
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] vlabel-full -> [VLabeled] for set ;
coherence
for b1 being _Graph st b1 is vlabel-full holds
b1 is [VLabeled]
proof end;
end;

definition
let G be EGraph;
attr G is elabel-distinct means :Def3: :: GLIB_010:def 3
 the_ELabel_of G is one-to-one ;
end;

:: deftheorem Def3 defines elabel-distinct GLIB_010:def 3 :
for G being EGraph holds
( G is elabel-distinct iff the_ELabel_of G is one-to-one );

definition
let G be VGraph;
attr G is vlabel-distinct means :Def4: :: GLIB_010:def 4
 the_VLabel_of G is one-to-one ;
end;

:: deftheorem Def4 defines vlabel-distinct GLIB_010:def 4 :
for G being VGraph holds
( G is vlabel-distinct iff the_VLabel_of G is one-to-one );

registration
let G be _Graph;
cluster G .set (ELabelSelector,(id (the_Edges_of G))) -> elabel-full elabel-distinct ;
coherence
( G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-full & G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct )
proof end;
cluster G .set (VLabelSelector,(id (the_Vertices_of G))) -> vlabel-full vlabel-distinct ;
coherence
( G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-full & G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-distinct )
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] elabel-full elabel-distinct for set ;
existence
ex b1 being EGraph st
( b1 is elabel-distinct & b1 is elabel-full )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] [VLabeled] vlabel-full vlabel-distinct for set ;
existence
ex b1 being VGraph st
( b1 is vlabel-distinct & b1 is vlabel-full )
proof end;
end;

definition
let G be elabel-full _Graph;
:: original: the_ELabel_of
redefine func the_ELabel_of G -> ManySortedSet of the_Edges_of G;
coherence
the_ELabel_of G is ManySortedSet of the_Edges_of G
proof end;
end;

definition
let G be vlabel-full _Graph;
:: original: the_VLabel_of
redefine func the_VLabel_of G -> ManySortedSet of the_Vertices_of G;
coherence
the_VLabel_of G is ManySortedSet of the_Vertices_of G
proof end;
end;

registration
let G be elabel-distinct EGraph;
cluster the_ELabel_of G -> one-to-one ;
coherence
the_ELabel_of G is one-to-one by Def3;
end;

registration
let G be vlabel-distinct VGraph;
cluster the_VLabel_of G -> one-to-one ;
coherence
the_VLabel_of G is one-to-one by Def4;
end;

registration
let G be elabel-full _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> elabel-full ;
coherence
G .set (WeightSelector,X) is elabel-full
proof end;
cluster G .set (VLabelSelector,X) -> elabel-full ;
coherence
G .set (VLabelSelector,X) is elabel-full
proof end;
end;

registration
let G be vlabel-full _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> vlabel-full ;
coherence
G .set (WeightSelector,X) is vlabel-full
proof end;
cluster G .set (ELabelSelector,X) -> vlabel-full ;
coherence
G .set (ELabelSelector,X) is vlabel-full
proof end;
end;

registration
let G be elabel-distinct EGraph;
let X be set ;
cluster G .set (WeightSelector,X) -> elabel-distinct ;
coherence
G .set (WeightSelector,X) is elabel-distinct
proof end;
cluster G .set (VLabelSelector,X) -> elabel-distinct ;
coherence
G .set (VLabelSelector,X) is elabel-distinct
proof end;
end;

registration
let G be vlabel-distinct VGraph;
let X be set ;
cluster G .set (WeightSelector,X) -> vlabel-distinct ;
coherence
G .set (WeightSelector,X) is vlabel-distinct
proof end;
cluster G .set (ELabelSelector,X) -> vlabel-distinct ;
coherence
G .set (ELabelSelector,X) is vlabel-distinct
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] [VLabeled] elabel-full vlabel-full elabel-distinct vlabel-distinct for set ;
existence
ex b1 being EVGraph st
( b1 is elabel-full & b1 is elabel-distinct & b1 is vlabel-full & b1 is vlabel-distinct )
proof end;
end;

:: END into GLIB_003 ?
registration
let G1 be WGraph;
let E be set ;
let G2 be reverseEdgeDirections of G1,E;
cluster G2 .set (WeightSelector,(the_Weight_of G1)) -> [Weighted] ;
coherence
G2 .set (WeightSelector,(the_Weight_of G1)) is [Weighted]
proof end;
end;

registration
let G1 be EGraph;
let E be set ;
let G2 be reverseEdgeDirections of G1,E;
cluster G2 .set (ELabelSelector,(the_ELabel_of G1)) -> [ELabeled] ;
coherence
G2 .set (ELabelSelector,(the_ELabel_of G1)) is [ELabeled]
proof end;
end;

registration
let G1 be VGraph;
let V be set ;
let G2 be reverseEdgeDirections of G1,V;
cluster G2 .set (VLabelSelector,(the_VLabel_of G1)) -> [VLabeled] ;
coherence
G2 .set (VLabelSelector,(the_VLabel_of G1)) is [VLabeled]
proof end;
end;

registration
let G1 be elabel-full _Graph;
let E be set ;
let G2 be reverseEdgeDirections of G1,E;
cluster G2 .set (ELabelSelector,(the_ELabel_of G1)) -> elabel-full ;
coherence
G2 .set (ELabelSelector,(the_ELabel_of G1)) is elabel-full
proof end;
end;

registration
let G1 be vlabel-full _Graph;
let V be set ;
let G2 be reverseEdgeDirections of G1,V;
cluster G2 .set (VLabelSelector,(the_VLabel_of G1)) -> vlabel-full ;
coherence
G2 .set (VLabelSelector,(the_VLabel_of G1)) is vlabel-full
proof end;
end;

registration
let G1 be elabel-distinct EGraph;
let E be set ;
let G2 be reverseEdgeDirections of G1,E;
cluster G2 .set (ELabelSelector,(the_ELabel_of G1)) -> elabel-distinct ;
coherence
G2 .set (ELabelSelector,(the_ELabel_of G1)) is elabel-distinct
proof end;
end;

registration
let G1 be vlabel-distinct VGraph;
let E be set ;
let G2 be reverseEdgeDirections of G1,E;
cluster G2 .set (VLabelSelector,(the_VLabel_of G1)) -> vlabel-distinct ;
coherence
G2 .set (VLabelSelector,(the_VLabel_of G1)) is vlabel-distinct
proof end;
end;

definition
func OrderingSelector -> Element of NAT equals :: GLIB_010:def 5
8;
correctness
coherence
8 is Element of NAT ;
;
end;

:: deftheorem defines OrderingSelector GLIB_010:def 5 :
OrderingSelector = 8;

definition
let G be GraphStruct;
attr G is [Ordered] means :Def6: :: GLIB_010:def 6
( OrderingSelector in dom G & G . OrderingSelector is Enumeration of (the_Vertices_of G) );
end;

:: deftheorem Def6 defines [Ordered] GLIB_010:def 6 :
for G being GraphStruct holds
( G is [Ordered] iff ( OrderingSelector in dom G & G . OrderingSelector is Enumeration of (the_Vertices_of G) ) );

Lm1: not OrderingSelector in _GraphSelectors
by GLIB_000:def 5, GLIB_000:1, ENUMSET1:def 2;

registration
let G be _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> [Graph-like] ;
coherence
G .set (OrderingSelector,X) is [Graph-like] by Lm1, GLIB_000:10;
end;

registration
let G be _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non plain ;
coherence
not G .set (OrderingSelector,X) is plain
proof end;
end;

registration
let G be WGraph;
let X be set ;
cluster G .set (OrderingSelector,X) -> [Weighted] ;
coherence
G .set (OrderingSelector,X) is [Weighted]
proof end;
end;

registration
let G be EGraph;
let X be set ;
cluster G .set (OrderingSelector,X) -> [ELabeled] ;
coherence
G .set (OrderingSelector,X) is [ELabeled]
proof end;
end;

registration
let G be VGraph;
let X be set ;
cluster G .set (OrderingSelector,X) -> [VLabeled] ;
coherence
G .set (OrderingSelector,X) is [VLabeled]
proof end;
end;

registration
let G be _Graph;
let X be Enumeration of (the_Vertices_of G);
cluster G .set (OrderingSelector,X) -> [Ordered] ;
coherence
G .set (OrderingSelector,X) is [Ordered]
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] [Ordered] for set ;
existence
ex b1 being GraphStruct st
( b1 is [Graph-like] & b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] & b1 is [Ordered] )
proof end;
end;

:: the definitions of O,WO,EO,VO,WEO,WVO,EVO and WEVOGraph are omitted
:: as is would simply clutter the already rich graph notation
definition
let G be [Ordered] _Graph;
func the_Ordering_of G -> Enumeration of (the_Vertices_of G) equals :: GLIB_010:def 7
G . OrderingSelector;
correctness
coherence
G . OrderingSelector is Enumeration of (the_Vertices_of G);
by Def6;
end;

:: deftheorem defines the_Ordering_of GLIB_010:def 7 :
for G being [Ordered] _Graph holds the_Ordering_of G = G . OrderingSelector;

theorem Th3: :: GLIB_010:3
for G being _Graph
for X being set holds G == G .set (OrderingSelector,X)
proof end;

registration
let G be elabel-full _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> elabel-full ;
coherence
G .set (OrderingSelector,X) is elabel-full
proof end;
end;

registration
let G be vlabel-full _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> vlabel-full ;
coherence
G .set (OrderingSelector,X) is vlabel-full
proof end;
end;

registration
let G be elabel-distinct EGraph;
let X be set ;
cluster G .set (OrderingSelector,X) -> elabel-distinct ;
coherence
G .set (OrderingSelector,X) is elabel-distinct
proof end;
end;

registration
let G be vlabel-distinct VGraph;
let X be set ;
cluster G .set (OrderingSelector,X) -> vlabel-distinct ;
coherence
G .set (OrderingSelector,X) is vlabel-distinct
proof end;
end;

registration
let G be _finite _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> _finite ;
coherence
G .set (OrderingSelector,X) is _finite
proof end;
end;

registration
let G be non _finite _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non _finite ;
coherence
not G .set (OrderingSelector,X) is _finite
proof end;
end;

registration
let G be loopless _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> loopless ;
coherence
G .set (OrderingSelector,X) is loopless
proof end;
end;

registration
let G be non loopless _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non loopless ;
coherence
not G .set (OrderingSelector,X) is loopless
proof end;
end;

registration
let G be _trivial _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> _trivial ;
coherence
G .set (OrderingSelector,X) is _trivial
proof end;
end;

registration
let G be non _trivial _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non _trivial ;
coherence
not G .set (OrderingSelector,X) is _trivial
proof end;
end;

registration
let G be non-multi _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non-multi ;
coherence
G .set (OrderingSelector,X) is non-multi
proof end;
end;

registration
let G be non non-multi _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non non-multi ;
coherence
not G .set (OrderingSelector,X) is non-multi
proof end;
end;

registration
let G be non-Dmulti _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non-Dmulti ;
coherence
G .set (OrderingSelector,X) is non-Dmulti
proof end;
end;

registration
let G be non non-Dmulti _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non non-Dmulti ;
coherence
not G .set (OrderingSelector,X) is non-Dmulti
proof end;
end;

registration
let G be connected _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> connected ;
coherence
G .set (OrderingSelector,X) is connected by Th3, GLIB_002:8;
end;

registration
let G be non connected _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non connected ;
coherence
not G .set (OrderingSelector,X) is connected
proof end;
end;

registration
let G be acyclic _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> acyclic ;
coherence
G .set (OrderingSelector,X) is acyclic by Th3, GLIB_002:44;
end;

registration
let G be non acyclic _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non acyclic ;
coherence
not G .set (OrderingSelector,X) is acyclic
proof end;
end;

registration
let G be edgeless _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> edgeless ;
coherence
G .set (OrderingSelector,X) is edgeless by Th3, GLIB_008:52;
end;

registration
let G be non edgeless _Graph;
let X be set ;
cluster G .set (OrderingSelector,X) -> non edgeless ;
coherence
not G .set (OrderingSelector,X) is edgeless
proof end;
end;

registration
let G be [Ordered] _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> [Ordered] ;
coherence
G .set (WeightSelector,X) is [Ordered]
proof end;
cluster G .set (ELabelSelector,X) -> [Ordered] ;
coherence
G .set (ELabelSelector,X) is [Ordered]
proof end;
cluster G .set (VLabelSelector,X) -> [Ordered] ;
coherence
G .set (VLabelSelector,X) is [Ordered]
proof end;
end;

:: Subgraph properties for ordered graphs are mostly omitted
:: because removing vertices of the graph creates gaps in the ordering.
:: A theorem describing how to fill these gaps (in such a way that:
:: for v1,v2 in V(G2) holds O(G2).v1 c= O(G2).v2 implies O(G1).v1 c= O(G1).v2)
:: is desirable, but will not be discussed here.
registration
let G1 be [Ordered] _Graph;
let G2 be spanning Subgraph of G1;
cluster G2 .set (OrderingSelector,(the_Ordering_of G1)) -> [Ordered] ;
coherence
G2 .set (OrderingSelector,(the_Ordering_of G1)) is [Ordered]
proof end;
end;

registration
let G1 be [Ordered] _Graph;
let E be set ;
let G2 be reverseEdgeDirections of G1,E;
cluster G2 .set (OrderingSelector,(the_Ordering_of G1)) -> [Ordered] ;
coherence
G2 .set (OrderingSelector,(the_Ordering_of G1)) is [Ordered]
proof end;
end;

Lm2: for G1, G2 being _Graph ex f, g being Function st
( [{},{}] = [f,g] & 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 ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f holds
( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) ) & ( 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 ) )
proof end;

definition
let G1, G2 be _Graph;
mode PGraphMapping of G1,G2 -> object means :Def8: :: GLIB_010:def 8
 ex f, g being Function st
( it = [f,g] & 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 ) ) & ( 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 ) );
existence
ex b1 being object ex f, g being Function st
( b1 = [f,g] & 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 ) ) & ( 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 ) )
proof end;
end;

:: deftheorem Def8 defines PGraphMapping GLIB_010:def 8 :
for G1, G2 being _Graph
for b3 being object holds
( b3 is PGraphMapping of G1,G2 iff ex f, g being Function st
( b3 = [f,g] & 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 ) ) & ( 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 ) ) );

Lm3: for G1, G2 being _Graph holds [{},{}] is PGraphMapping of G1,G2
proof end;

registration
let G1, G2 be _Graph;
cluster -> pair for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 holds b1 is pair
proof end;
end;

notation
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
synonym F _V for G1 `1 ;
synonym F _E for G1 `2 ;
end;

registration
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
reduce [( _V),( _E)] to F;
reducibility
[( _V),( _E)] = F ;
end;

registration
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
cluster _V -> Relation-like Function-like for set ;
coherence
for b1 being set st b1 = _V holds
( b1 is Function-like & b1 is Relation-like )
proof end;
cluster _E -> Relation-like Function-like for set ;
coherence
for b1 being set st b1 = _E holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
cluster _V -> the_Vertices_of G1 -defined the_Vertices_of G2 -valued for Function;
coherence
for b1 being Function st b1 = _V holds
( b1 is the_Vertices_of G1 -defined & b1 is the_Vertices_of G2 -valued )
proof end;
cluster _E -> the_Edges_of G1 -defined the_Edges_of G2 -valued for Function;
coherence
for b1 being Function st b1 = _E holds
( b1 is the_Edges_of G1 -defined & b1 is the_Edges_of G2 -valued )
proof end;
end;

definition
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
:: original: _V
redefine func F _V -> PartFunc of (the_Vertices_of G1),(the_Vertices_of G2);
coherence
_V is PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)
proof end;
:: original: _E
redefine func F _E -> PartFunc of (the_Edges_of G1),(the_Edges_of G2);
coherence
_E is PartFunc of (the_Edges_of G1),(the_Edges_of G2)
proof end;
end;

theorem Th4: :: GLIB_010:4
for G1, G2 being _Graph
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
proof end;

theorem Th5: :: GLIB_010:5
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for e being object st e in dom (F _E) holds
( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) )
proof end;

theorem Th6: :: GLIB_010:6
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for e being object st e in rng (F _E) holds
( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )
proof end;

theorem Th7: :: GLIB_010:7
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( dom (F _E) c= G1 .edgesBetween (dom (F _V)) & rng (F _E) c= G2 .edgesBetween (rng (F _V)) )
proof end;

theorem Th8: :: GLIB_010:8
for G1, G2 being _Graph
for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)
for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( 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 Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) holds
[f,g] is PGraphMapping of G1,G2
proof end;

theorem Th9: :: GLIB_010:9
for G1, G2, G3, G4 being _Graph
for F being PGraphMapping of G1,G2 st G1 == G3 & G2 == G4 holds
F is PGraphMapping of G3,G4
proof end;

theorem Th10: :: GLIB_010:10
for G1, G2, G3, G4 being _Graph
for F being PGraphMapping of G1,G2 st ex E1, E2 being set st
( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) holds
F is PGraphMapping of G3,G4
proof end;

definition
let G be _Graph;
func id G -> PGraphMapping of G,G equals :: GLIB_010:def 9
[(id (the_Vertices_of G)),(id (the_Edges_of G))];
coherence
[(id (the_Vertices_of G)),(id (the_Edges_of G))] is PGraphMapping of G,G
proof end;
end;

:: deftheorem defines id GLIB_010:def 9 :
for G being _Graph holds id G = [(id (the_Vertices_of G)),(id (the_Edges_of G))];

theorem :: GLIB_010:11
for G1, G2 being _Graph st G1 == G2 holds
( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )
proof end;

theorem :: GLIB_010:12
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )
proof end;

definition
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
attr F is empty means :Def10: :: GLIB_010:def 10
 dom (F _V) is empty ;
attr F is total means :Def11: :: GLIB_010:def 11
( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 );
attr F is onto means :Def12: :: GLIB_010:def 12
( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 );
attr F is one-to-one means :Def13: :: GLIB_010:def 13
( F _V is one-to-one & F _E is one-to-one );
attr F is directed means :Def14: :: GLIB_010:def 14
 for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds
(F _E) . e DJoins (F _V) . v,(F _V) . w,G2;
attr F is semi-continuous means :Def15: :: GLIB_010:def 15
 for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 holds
e Joins v,w,G1;
attr F is continuous means :Def16: :: GLIB_010:def 16
 for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 holds
ex e being object st
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 );
attr F is semi-Dcontinuous means :Def17: :: GLIB_010:def 17
 for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 holds
e DJoins v,w,G1;
attr F is Dcontinuous means :Def18: :: GLIB_010:def 18
 for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 holds
ex e being object st
( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 );
end;

:: deftheorem Def10 defines empty GLIB_010:def 10 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is empty iff dom (F _V) is empty );

:: deftheorem Def11 defines total GLIB_010:def 11 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is total iff ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 ) );

:: deftheorem Def12 defines onto GLIB_010:def 12 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is onto iff ( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 ) );

:: deftheorem Def13 defines one-to-one GLIB_010:def 13 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is one-to-one iff ( F _V is one-to-one & F _E is one-to-one ) );

:: deftheorem Def14 defines directed GLIB_010:def 14 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is directed iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds
(F _E) . e DJoins (F _V) . v,(F _V) . w,G2 );

:: deftheorem Def15 defines semi-continuous GLIB_010:def 15 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is semi-continuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 holds
e Joins v,w,G1 );

:: deftheorem Def16 defines continuous GLIB_010:def 16 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is continuous iff for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 holds
ex e being object st
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) );

:: deftheorem Def17 defines semi-Dcontinuous GLIB_010:def 17 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is semi-Dcontinuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 holds
e DJoins v,w,G1 );

:: deftheorem Def18 defines Dcontinuous GLIB_010:def 18 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is Dcontinuous iff for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 holds
ex e being object st
( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) );

:: at first properties of these attributes for the PGM are studied
:: regardless of the kinds of graph involved
theorem Th13: :: GLIB_010:13
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is directed iff 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) ) )
proof end;

:: |dom F_E is probably not required, as the PGM property
:: enforces such a relationship between F_V and F_E
theorem :: GLIB_010:14
for G1, G2 being _Graph
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))) ) )
proof end;

theorem Th15: :: GLIB_010:15
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is semi-continuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) holds
( e Joins v,w,G1 iff (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ) by Th4;

theorem Th16: :: GLIB_010:16
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is semi-Dcontinuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) holds
( e DJoins v,w,G1 iff (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) )
proof end;

registration
let G1, G2 be _Graph;
cluster pair empty one-to-one directed semi-continuous continuous semi-Dcontinuous Dcontinuous for PGraphMapping of G1,G2;
existence
ex b1 being PGraphMapping of G1,G2 st
( b1 is empty & b1 is one-to-one & b1 is Dcontinuous & b1 is directed & b1 is continuous & b1 is semi-Dcontinuous & b1 is semi-continuous )
proof end;
cluster pair non empty one-to-one directed semi-continuous semi-Dcontinuous for PGraphMapping of G1,G2;
existence
ex b1 being PGraphMapping of G1,G2 st
( not b1 is empty & b1 is one-to-one & b1 is directed & b1 is semi-Dcontinuous & b1 is semi-continuous )
proof end;
end;

registration
let G1, G2 be _Graph;
let F be empty PGraphMapping of G1,G2;
cluster _V -> empty for set ;
coherence
for b1 being set st b1 = F _V holds
b1 is empty
proof end;
cluster _E -> empty for set ;
coherence
for b1 being set st b1 = F _E holds
b1 is empty
proof end;
end;

registration
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1,G2;
cluster _V -> non empty for set ;
coherence
for b1 being set st b1 = F _V holds
not b1 is empty
proof end;
end;

registration
let G1, G2 be _Graph;
let F be one-to-one PGraphMapping of G1,G2;
cluster _V -> one-to-one for Function;
coherence
for b1 being Function st b1 = F _V holds
b1 is one-to-one by Def13;
cluster _E -> one-to-one for Function;
coherence
for b1 being Function st b1 = F _E holds
b1 is one-to-one by Def13;
end;

theorem Th17: :: GLIB_010:17
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F _V is one-to-one holds
F is semi-continuous
proof end;

theorem Th18: :: GLIB_010:18
for G1, G2 being _Graph
for F being directed PGraphMapping of G1,G2 st F _V is one-to-one holds
F is semi-Dcontinuous
proof end;

theorem Th19: :: GLIB_010:19
for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds
F is continuous
proof end;

theorem Th20: :: GLIB_010:20
for G1, G2 being _Graph
for F being semi-Dcontinuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds
F is Dcontinuous
proof end;

theorem Th21: :: GLIB_010:21
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F _V is one-to-one & rng (F _E) = the_Edges_of G2 holds
F is continuous
proof end;

theorem Th22: :: GLIB_010:22
for G1, G2 being _Graph
for F being directed PGraphMapping of G1,G2 st F _V is one-to-one & rng (F _E) = the_Edges_of G2 holds
F is Dcontinuous
proof end;

theorem :: GLIB_010:23
for G1, G2 being _Graph
for F being continuous PGraphMapping of G1,G2 st F _E is one-to-one holds
F is semi-continuous
proof end;

theorem Th24: :: GLIB_010:24
for G1, G2 being _Graph
for F being Dcontinuous PGraphMapping of G1,G2 st F _E is one-to-one holds
F is semi-Dcontinuous
proof end;

theorem Th25: :: GLIB_010:25
for G1, G2 being _Graph
for F being Dcontinuous PGraphMapping of G1,G2 st F _E is one-to-one holds
F is directed
proof end;

theorem Th26: :: GLIB_010:26
for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2
for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v1,(F _V) . w,G2 ) holds
v1 = v2
proof end;

:: a special case of the following theorem is when G2 is without isolated
:: vertices and F is onto
theorem :: GLIB_010:27
for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 st ( for v being object st v in dom (F _V) holds
ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ) holds
F _V is one-to-one
proof end;

theorem Th28: :: GLIB_010:28
for G1, G2 being _Graph
for F being semi-Dcontinuous PGraphMapping of G1,G2
for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v1,(F _V) . w,G2 ) holds
v1 = v2
proof end;

:: again, a special case of the following theorem is when G2 is without
:: isolated vertices and F is onto
theorem :: GLIB_010:29
for G1, G2 being _Graph
for F being semi-Dcontinuous PGraphMapping of G1,G2 st ( for v being object st v in dom (F _V) holds
ex e, w being object st
( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) ) holds
F _V is one-to-one
proof end;

registration
let G1, G2 be _Graph;
cluster one-to-one -> semi-continuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is one-to-one holds
b1 is semi-continuous by Th17;
cluster one-to-one directed -> semi-Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is one-to-one & b1 is directed holds
b1 is semi-Dcontinuous by Th18;
cluster onto one-to-one -> continuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is one-to-one & b1 is onto holds
b1 is continuous by Th21;
cluster onto one-to-one directed -> Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is directed & b1 is one-to-one & b1 is onto holds
b1 is Dcontinuous by Th22;
cluster onto semi-continuous -> continuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is semi-continuous & b1 is onto holds
b1 is continuous by Th19;
cluster semi-Dcontinuous -> directed semi-continuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is semi-Dcontinuous holds
( b1 is directed & b1 is semi-continuous )
proof end;
cluster onto semi-Dcontinuous -> Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is semi-Dcontinuous & b1 is onto holds
b1 is Dcontinuous by Th20;
cluster Dcontinuous -> continuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is Dcontinuous holds
b1 is continuous
proof end;
cluster one-to-one Dcontinuous -> directed semi-Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is Dcontinuous & b1 is one-to-one holds
( b1 is directed & b1 is semi-Dcontinuous ) by Th25, Th24;
cluster empty -> one-to-one directed continuous Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is empty holds
( b1 is one-to-one & b1 is Dcontinuous & b1 is directed & b1 is continuous ) ;
cluster total -> non empty for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is total holds
not b1 is empty ;
cluster onto -> non empty for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is onto holds
not b1 is empty ;
end;

registration
let G be _Graph;
cluster id G -> non empty total onto one-to-one Dcontinuous ;
coherence
( id G is total & not id G is empty & id G is onto & id G is one-to-one & id G is Dcontinuous )
proof end;
end;

theorem Th30: :: GLIB_010:30
for G1, G2 being _Graph
for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)
for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( 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 ) holds
[f,g] is directed PGraphMapping of G1,G2
proof end;

theorem Th31: :: GLIB_010:31
for G1, G2 being _Graph
for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)
for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( 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 holds
( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) ) holds
[f,g] is semi-continuous PGraphMapping of G1,G2
proof end;

theorem :: GLIB_010:32
for G1, G2 being _Graph
for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)
for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( 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 holds
( e DJoins v,w,G1 iff g . e DJoins f . v,f . w,G2 ) ) holds
[f,g] is semi-Dcontinuous PGraphMapping of G1,G2
proof end;

theorem :: GLIB_010:33
for G1, G2 being _Graph holds [{},{}] is empty one-to-one Dcontinuous PGraphMapping of G1,G2
proof end;

theorem Th34: :: GLIB_010:34
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total holds
for v being Vertex of G1 holds (F _V) . v is Vertex of G2
proof end;

theorem Th35: :: GLIB_010:35
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total holds
( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )
proof end;

theorem Th36: :: GLIB_010:36
for G1, G2 being _Graph
for F being continuous PGraphMapping of G1,G2 st rng (F _V) = the_Vertices_of G2 & G1 is loopless holds
G2 is loopless
proof end;

theorem :: GLIB_010:37
for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 st F is onto & G1 is loopless holds
G2 is loopless by Th36;

theorem :: GLIB_010:38
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 & G1 is edgeless holds
G2 is edgeless ;

theorem :: GLIB_010:39
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto & G1 is edgeless holds
G2 is edgeless ;

:: next properties of these attributes for the PGM are studied
:: when G1 or G2 has a certain property
theorem :: GLIB_010:40
for G1 being _Graph
for G2 being non-multi _Graph
for F1, F2 being PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds
F1 = F2
proof end;

theorem :: GLIB_010:41
for G1 being _Graph
for G2 being non-Dmulti _Graph
for F1, F2 being directed PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds
F1 = F2
proof end;

theorem :: GLIB_010:42
for G1 being non-multi _Graph
for G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 holds F _E is one-to-one
proof end;

theorem :: GLIB_010:43
for G1 being non-multi _Graph
for G2 being _Graph
for F being PGraphMapping of G1,G2 st F _V is one-to-one holds
F _E is one-to-one
proof end;

theorem :: GLIB_010:44
for G1 being non-Dmulti _Graph
for G2 being _Graph
for F being directed PGraphMapping of G1,G2 st F _V is one-to-one holds
F _E is one-to-one
proof end;

registration
let G1 be _Graph;
let G2 be loopless _Graph;
cluster directed semi-continuous -> semi-Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is directed & b1 is semi-continuous holds
b1 is semi-Dcontinuous
proof end;
cluster directed continuous -> Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is directed & b1 is continuous holds
b1 is Dcontinuous
proof end;
end;

registration
let G1 be _trivial _Graph;
let G2 be _Graph;
cluster -> directed for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 holds b1 is directed
proof end;
cluster semi-continuous -> semi-Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is semi-continuous holds
b1 is semi-Dcontinuous
proof end;
cluster continuous -> Dcontinuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is continuous holds
b1 is Dcontinuous
proof end;
end;

registration
let G1 be _trivial non-Dmulti _Graph;
let G2 be _Graph;
cluster -> one-to-one for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 holds b1 is one-to-one
proof end;
end;

registration
let G1 be _trivial edgeless _Graph;
let G2 be _Graph;
cluster non empty -> total for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st not b1 is empty holds
b1 is total
proof end;
end;

registration
let G1 be _Graph;
let G2 be _trivial edgeless _Graph;
cluster non empty -> onto for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st not b1 is empty holds
b1 is onto
proof end;
cluster -> semi-continuous continuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 holds
( b1 is semi-continuous & b1 is continuous ) by GLIB_000:def 13;
end;

:: define the concept of subgraph embedding and isomorphism
definition
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
attr F is weak_SG-embedding means :: GLIB_010:def 19
( F is total & F is one-to-one );
attr F is strong_SG-embedding means :: GLIB_010:def 20
( F is total & F is one-to-one & F is continuous );
attr F is isomorphism means :: GLIB_010:def 21
( F is total & F is one-to-one & F is onto );
:: the next one is not really important (since directed isomorphism works
:: just as well), but the term will be used with PVertexMappings later
:: anyway, so it is introduced here shortly as well.
attr F is Disomorphism means :: GLIB_010:def 22
( F is directed & F is total & F is one-to-one & F is onto );
end;

:: deftheorem defines weak_SG-embedding GLIB_010:def 19 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is weak_SG-embedding iff ( F is total & F is one-to-one ) );

:: deftheorem defines strong_SG-embedding GLIB_010:def 20 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is strong_SG-embedding iff ( F is total & F is one-to-one & F is continuous ) );

:: deftheorem defines isomorphism GLIB_010:def 21 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is isomorphism iff ( F is total & F is one-to-one & F is onto ) );

:: deftheorem defines Disomorphism GLIB_010:def 22 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is Disomorphism iff ( F is directed & F is total & F is one-to-one & F is onto ) );

registration
let G1, G2 be _Graph;
cluster weak_SG-embedding -> non empty total one-to-one semi-continuous for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is weak_SG-embedding holds
( b1 is total & not b1 is empty & b1 is one-to-one & b1 is semi-continuous ) ;
cluster total one-to-one -> weak_SG-embedding for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is total & b1 is one-to-one holds
b1 is weak_SG-embedding ;
cluster strong_SG-embedding -> non empty total one-to-one continuous weak_SG-embedding for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is strong_SG-embedding holds
( b1 is total & not b1 is empty & b1 is one-to-one & b1 is continuous & b1 is weak_SG-embedding ) ;
cluster total one-to-one continuous -> strong_SG-embedding for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is total & b1 is one-to-one & b1 is continuous holds
b1 is strong_SG-embedding ;
cluster continuous weak_SG-embedding -> strong_SG-embedding for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is weak_SG-embedding & b1 is continuous holds
b1 is strong_SG-embedding ;
cluster isomorphism -> non empty total onto one-to-one semi-continuous continuous weak_SG-embedding strong_SG-embedding for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is isomorphism holds
( b1 is onto & b1 is semi-continuous & b1 is continuous & b1 is total & not b1 is empty & b1 is one-to-one & b1 is weak_SG-embedding & b1 is strong_SG-embedding ) ;
cluster total onto one-to-one continuous -> isomorphism for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is total & b1 is one-to-one & b1 is onto & b1 is continuous holds
b1 is isomorphism ;
cluster onto strong_SG-embedding -> isomorphism for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is strong_SG-embedding & b1 is onto holds
b1 is isomorphism ;
cluster onto continuous weak_SG-embedding -> isomorphism for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is weak_SG-embedding & b1 is continuous & b1 is onto holds
b1 is isomorphism ;
cluster Disomorphism -> non empty total one-to-one directed semi-continuous continuous semi-Dcontinuous weak_SG-embedding strong_SG-embedding isomorphism for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is Disomorphism holds
( b1 is directed & b1 is isomorphism & b1 is continuous & b1 is total & not b1 is empty & b1 is semi-Dcontinuous & b1 is semi-continuous & b1 is one-to-one & b1 is weak_SG-embedding & b1 is strong_SG-embedding ) ;
cluster directed isomorphism -> Dcontinuous Disomorphism for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 st b1 is directed & b1 is isomorphism holds
( b1 is Dcontinuous & b1 is Disomorphism ) ;
end;

registration
let G be _Graph;
cluster id G -> weak_SG-embedding strong_SG-embedding isomorphism Disomorphism ;
coherence
( id G is weak_SG-embedding & id G is strong_SG-embedding & id G is isomorphism & id G is Disomorphism ) ;
end;

registration
let G be _Graph;
cluster pair weak_SG-embedding strong_SG-embedding isomorphism Disomorphism for PGraphMapping of G,G;
existence
ex b1 being PGraphMapping of G,G st
( b1 is weak_SG-embedding & b1 is strong_SG-embedding & b1 is isomorphism & b1 is Disomorphism )
proof end;
end;

theorem Th45: :: GLIB_010:45
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() )
proof end;

theorem Th46: :: GLIB_010:46
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds
card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))
proof end;

theorem Th47: :: GLIB_010:47
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds
card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X))
proof end;

theorem Th48: :: GLIB_010:48
for G1, G2 being _Graph
for F being directed PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds
card (G1 .edgesDBetween (X,Y)) c= card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))
proof end;

theorem Th49: :: GLIB_010:49
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
( ( G2 is _trivial implies G1 is _trivial ) & ( G2 is non-multi implies G1 is non-multi ) & ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) )
proof end;

theorem Th50: :: GLIB_010:50
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is directed & F is weak_SG-embedding holds
( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) )
proof end;

theorem Th51: :: GLIB_010:51
for G1, G2 being _finite _Graph
for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G1 .order() = G2 .order() & G1 .size() = G2 .size() holds
F is isomorphism
proof end;

theorem Th52: :: GLIB_010:52
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G2 is complete holds
G1 is complete
proof end;

:: isomorphism as an attribute
definition
let G1, G2 be _Graph;
attr G2 is G1 -isomorphic means :Def23: :: GLIB_010:def 23
 ex F being PGraphMapping of G1,G2 st F is isomorphism ;
attr G2 is G1 -Disomorphic means :Def24: :: GLIB_010:def 24
 ex F being PGraphMapping of G1,G2 st F is Disomorphism ;
end;

:: deftheorem Def23 defines -isomorphic GLIB_010:def 23 :
for G1, G2 being _Graph holds
( G2 is G1 -isomorphic iff ex F being PGraphMapping of G1,G2 st F is isomorphism );

:: deftheorem Def24 defines -Disomorphic GLIB_010:def 24 :
for G1, G2 being _Graph holds
( G2 is G1 -Disomorphic iff ex F being PGraphMapping of G1,G2 st F is Disomorphism );

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] G -Disomorphic -> G -isomorphic for set ;
coherence
for b1 being _Graph st b1 is G -Disomorphic holds
b1 is G -isomorphic ;
end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] G -isomorphic G -Disomorphic for set ;
existence
ex b1 being _Graph st
( b1 is G -Disomorphic & b1 is G -isomorphic )
proof end;
end;

theorem Th53: :: GLIB_010:53
for G being _Graph holds
( G is G -Disomorphic & G is G -isomorphic )
proof end;

registration
let G1 be _Graph;
let G2 be G1 -isomorphic _Graph;
cluster pair non empty total onto one-to-one semi-continuous continuous weak_SG-embedding strong_SG-embedding isomorphism for PGraphMapping of G1,G2;
existence
ex b1 being PGraphMapping of G1,G2 st
( b1 is isomorphism & b1 is strong_SG-embedding & b1 is weak_SG-embedding & b1 is total & not b1 is empty & b1 is one-to-one & b1 is onto & b1 is semi-continuous & b1 is continuous )
proof end;
end;

:: this is the main reason for using an attribute instead of predicate
:: for isomorphism
definition
let G1 be _Graph;
let G2 be G1 -isomorphic _Graph;
mode Isomorphism of G1,G2 is isomorphism PGraphMapping of G1,G2;
end;

registration
let G1 be _Graph;
let G2 be G1 -Disomorphic _Graph;
cluster pair non empty total onto one-to-one directed semi-Dcontinuous Dcontinuous weak_SG-embedding strong_SG-embedding isomorphism for PGraphMapping of G1,G2;
existence
ex b1 being PGraphMapping of G1,G2 st
( b1 is isomorphism & b1 is strong_SG-embedding & b1 is weak_SG-embedding & b1 is total & not b1 is empty & b1 is one-to-one & b1 is onto & b1 is directed & b1 is semi-Dcontinuous & b1 is Dcontinuous )
proof end;
end;

definition
let G1 be _Graph;
let G2 be G1 -Disomorphic _Graph;
mode DIsomorphism of G1,G2 is Disomorphism PGraphMapping of G1,G2;
end;

:: define weight-/label-/ordering-preserving mappings
definition
let G1, G2 be WGraph;
let F be PGraphMapping of G1,G2;
attr F is weight-preserving means :: GLIB_010:def 25
(the_Weight_of G2) * (F _E) = (the_Weight_of G1) | (dom (F _E));
end;

:: deftheorem defines weight-preserving GLIB_010:def 25 :
for G1, G2 being WGraph
for F being PGraphMapping of G1,G2 holds
( F is weight-preserving iff (the_Weight_of G2) * (F _E) = (the_Weight_of G1) | (dom (F _E)) );

definition
let G1, G2 be EGraph;
let F be PGraphMapping of G1,G2;
attr F is elabel-preserving means :: GLIB_010:def 26
(the_ELabel_of G2) * (F _E) = (the_ELabel_of G1) | (dom (F _E));
end;

:: deftheorem defines elabel-preserving GLIB_010:def 26 :
for G1, G2 being EGraph
for F being PGraphMapping of G1,G2 holds
( F is elabel-preserving iff (the_ELabel_of G2) * (F _E) = (the_ELabel_of G1) | (dom (F _E)) );

definition
let G1, G2 be VGraph;
let F be PGraphMapping of G1,G2;
attr F is vlabel-preserving means :: GLIB_010:def 27
(the_VLabel_of G2) * (F _V) = (the_VLabel_of G1) | (dom (F _V));
end;

:: deftheorem defines vlabel-preserving GLIB_010:def 27 :
for G1, G2 being VGraph
for F being PGraphMapping of G1,G2 holds
( F is vlabel-preserving iff (the_VLabel_of G2) * (F _V) = (the_VLabel_of G1) | (dom (F _V)) );

definition
let G1, G2 be [Ordered] _Graph;
let F be PGraphMapping of G1,G2;
attr F is ordering-preserving means :: GLIB_010:def 28
(the_Ordering_of G2) * (F _V) = (the_Ordering_of G1) | (dom (F _V));
end;

:: deftheorem defines ordering-preserving GLIB_010:def 28 :
for G1, G2 being [Ordered] _Graph
for F being PGraphMapping of G1,G2 holds
( F is ordering-preserving iff (the_Ordering_of G2) * (F _V) = (the_Ordering_of G1) | (dom (F _V)) );

registration
let G be WGraph;
cluster id G -> weight-preserving ;
coherence
id G is weight-preserving by RELAT_1:65;
end;

registration
let G be EGraph;
cluster id G -> elabel-preserving ;
coherence
id G is elabel-preserving by RELAT_1:65;
end;

registration
let G be VGraph;
cluster id G -> vlabel-preserving ;
coherence
id G is vlabel-preserving by RELAT_1:65;
end;

registration
let G be [Ordered] _Graph;
cluster id G -> ordering-preserving ;
coherence
id G is ordering-preserving by RELAT_1:65;
end;

:: define domain and range of graph mappings
definition
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
func dom F -> inducedSubgraph of G1, dom (F _V), dom (F _E) equals :: GLIB_010:def 29
 the plain inducedSubgraph of G1, dom (F _V), dom (F _E);
coherence
the plain inducedSubgraph of G1, dom (F _V), dom (F _E) is inducedSubgraph of G1, dom (F _V), dom (F _E) ;
func rng F -> inducedSubgraph of G2, rng (F _V), rng (F _E) equals :: GLIB_010:def 30
 the plain inducedSubgraph of G2, rng (F _V), rng (F _E);
coherence
the plain inducedSubgraph of G2, rng (F _V), rng (F _E) is inducedSubgraph of G2, rng (F _V), rng (F _E) ;
end;

:: deftheorem defines dom GLIB_010:def 29 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds dom F = the plain inducedSubgraph of G1, dom (F _V), dom (F _E);

:: deftheorem defines rng GLIB_010:def 30 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds rng F = the plain inducedSubgraph of G2, rng (F _V), rng (F _E);

registration
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
cluster dom F -> plain ;
coherence
dom F is plain ;
cluster rng F -> plain ;
coherence
rng F is plain ;
end;

theorem Th54: :: GLIB_010:54
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2 holds
( the_Vertices_of (dom F) = dom (F _V) & the_Edges_of (dom F) = dom (F _E) & the_Vertices_of (rng F) = rng (F _V) & the_Edges_of (rng F) = rng (F _E) )
proof end;

theorem Th55: :: GLIB_010:55
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2 holds
( F is total iff dom F == G1 )
proof end;

theorem :: GLIB_010:56
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2 holds
( F is onto iff rng F == G2 )
proof end;

:: define restrictions of graph mappings
definition
let G1, G2 be _Graph;
let H be Subgraph of G1;
let F be PGraphMapping of G1,G2;
func F | H -> PGraphMapping of H,G2 equals :: GLIB_010:def 31
[((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))];
coherence
[((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))] is PGraphMapping of H,G2
proof end;
end;

:: deftheorem defines | GLIB_010:def 31 :
for G1, G2 being _Graph
for H being Subgraph of G1
for F being PGraphMapping of G1,G2 holds F | H = [((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))];

theorem Th57: :: GLIB_010:57
for G1, G2 being _Graph
for H being Subgraph of G1
for F being PGraphMapping of G1,G2 holds
( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )
proof end;

theorem Th58: :: GLIB_010:58
for G1, G2 being _Graph
for V being set
for H being inducedSubgraph of G1,V
for F being PGraphMapping of G1,G2 holds
( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )
proof end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G1;
let F be empty PGraphMapping of G1,G2;
cluster F | H -> empty ;
coherence
F | H is empty ;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G1;
let F be one-to-one PGraphMapping of G1,G2;
cluster F | H -> one-to-one ;
coherence
F | H is one-to-one by Th57;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G1;
let F be semi-continuous PGraphMapping of G1,G2;
cluster F | H -> semi-continuous ;
coherence
F | H is semi-continuous by Th57;
end;

registration
let G1, G2 be _Graph;
let V be set ;
let H be inducedSubgraph of G1,V;
let F be continuous PGraphMapping of G1,G2;
cluster F | H -> continuous ;
coherence
F | H is continuous by Th58;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G1;
let F be directed PGraphMapping of G1,G2;
cluster F | H -> directed ;
coherence
F | H is directed by Th57;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G1;
let F be semi-Dcontinuous PGraphMapping of G1,G2;
cluster F | H -> semi-Dcontinuous ;
coherence
F | H is semi-Dcontinuous by Th57;
end;

registration
let G1, G2 be _Graph;
let V be set ;
let H be inducedSubgraph of G1,V;
let F be Dcontinuous PGraphMapping of G1,G2;
cluster F | H -> Dcontinuous ;
coherence
F | H is Dcontinuous by Th58;
end;

registration
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1,G2;
cluster F | (dom F) -> total ;
coherence
F | (dom F) is total
proof end;
end;

theorem Th59: :: GLIB_010:59
for G1, G2 being _Graph
for H being Subgraph of G1
for F being PGraphMapping of G1,G2 holds
( dom ((F | H) _V) = (dom (F _V)) /\ (the_Vertices_of H) & dom ((F | H) _E) = (dom (F _E)) /\ (the_Edges_of H) ) by RELAT_1:61;

theorem :: GLIB_010:60
for G1, G2 being WGraph
for H being WSubgraph of G1
for F being PGraphMapping of G1,G2 st F is weight-preserving holds
F | H is weight-preserving
proof end;

theorem :: GLIB_010:61
for G1, G2 being EGraph
for H being ESubgraph of G1
for F being PGraphMapping of G1,G2 st F is elabel-preserving holds
F | H is elabel-preserving
proof end;

theorem :: GLIB_010:62
for G1, G2 being VGraph
for H being VSubgraph of G1
for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds
F | H is vlabel-preserving
proof end;

definition
let G1, G2 be _Graph;
let H be Subgraph of G2;
let F be PGraphMapping of G1,G2;
func H |` F -> PGraphMapping of G1,H equals :: GLIB_010:def 32
[((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))];
coherence
[((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))] is PGraphMapping of G1,H
proof end;
end;

:: deftheorem defines |` GLIB_010:def 32 :
for G1, G2 being _Graph
for H being Subgraph of G2
for F being PGraphMapping of G1,G2 holds H |` F = [((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))];

theorem Th63: :: GLIB_010:63
for G1, G2 being _Graph
for H being Subgraph of G2
for F being PGraphMapping of G1,G2 holds
( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
proof end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G2;
let F be empty PGraphMapping of G1,G2;
cluster H |` F -> empty ;
coherence
H |` F is empty by Th63;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G2;
let F be one-to-one PGraphMapping of G1,G2;
cluster H |` F -> one-to-one ;
coherence
H |` F is one-to-one by Th63;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G2;
let F be semi-continuous PGraphMapping of G1,G2;
cluster H |` F -> semi-continuous ;
coherence
H |` F is semi-continuous by Th63;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G2;
let F be continuous PGraphMapping of G1,G2;
cluster H |` F -> continuous ;
coherence
H |` F is continuous by Th63;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G2;
let F be directed PGraphMapping of G1,G2;
cluster H |` F -> directed ;
coherence
H |` F is directed by Th63;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G2;
let F be semi-Dcontinuous PGraphMapping of G1,G2;
cluster H |` F -> semi-Dcontinuous ;
coherence
H |` F is semi-Dcontinuous by Th63;
end;

registration
let G1, G2 be _Graph;
let H be Subgraph of G2;
let F be Dcontinuous PGraphMapping of G1,G2;
cluster H |` F -> Dcontinuous ;
coherence
H |` F is Dcontinuous by Th63;
end;

registration
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1,G2;
cluster (rng F) |` F -> onto ;
coherence
(rng F) |` F is onto
proof end;
end;

theorem :: GLIB_010:64
for G1, G2 being _Graph
for H being Subgraph of G2
for F being PGraphMapping of G1,G2 holds
( rng ((H |` F) _V) = (rng (F _V)) /\ (the_Vertices_of H) & rng ((H |` F) _E) = (rng (F _E)) /\ (the_Edges_of H) ) by RELAT_1:88;

theorem :: GLIB_010:65
for G1, G2 being WGraph
for H being WSubgraph of G2
for F being PGraphMapping of G1,G2 st F is weight-preserving holds
H |` F is weight-preserving
proof end;

theorem :: GLIB_010:66
for G1, G2 being EGraph
for H being ESubgraph of G2
for F being PGraphMapping of G1,G2 st F is elabel-preserving holds
H |` F is elabel-preserving
proof end;

theorem :: GLIB_010:67
for G1, G2 being VGraph
for H being VSubgraph of G2
for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds
H |` F is vlabel-preserving
proof end;

theorem :: GLIB_010:68
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for H1 being Subgraph of G1
for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)
proof end;

:: define inverse of graph mappings
definition
let G1, G2 be _Graph;
let F be one-to-one PGraphMapping of G1,G2;
func F " -> PGraphMapping of G2,G1 equals :: GLIB_010:def 33
[((F _V) "),((F _E) ")];
coherence
[((F _V) "),((F _E) ")] is PGraphMapping of G2,G1
proof end;
end;

:: deftheorem defines " GLIB_010:def 33 :
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds F " = [((F _V) "),((F _E) ")];

registration
let G1, G2 be _Graph;
let F be one-to-one PGraphMapping of G1,G2;
cluster F " -> one-to-one semi-continuous ;
coherence
( F " is one-to-one & F " is semi-continuous )
proof end;
end;

registration
let G1, G2 be _Graph;
let F be empty one-to-one PGraphMapping of G1,G2;
cluster F " -> empty ;
coherence
F " is empty
proof end;
end;

registration
let G1, G2 be _Graph;
let F be non empty one-to-one PGraphMapping of G1,G2;
cluster F " -> non empty ;
coherence
not F " is empty
proof end;
end;

registration
let G1, G2 be _Graph;
let F be one-to-one semi-Dcontinuous PGraphMapping of G1,G2;
cluster F " -> semi-Dcontinuous ;
coherence
F " is semi-Dcontinuous
proof end;
end;

theorem :: GLIB_010:69
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds
( (F ") _V = (F _V) " & (F ") _E = (F _E) " ) ;

theorem Th70: :: GLIB_010:70
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds (F ") " = F
proof end;

theorem Th71: :: GLIB_010:71
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds
( F is total iff F " is onto ) by FUNCT_1:33;

theorem Th72: :: GLIB_010:72
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds
( F is onto iff F " is total ) by FUNCT_1:33;

theorem :: GLIB_010:73
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is total & F is continuous holds
F " is continuous
proof end;

theorem Th74: :: GLIB_010:74
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is total & F is Dcontinuous holds
F " is Dcontinuous
proof end;

theorem Th75: :: GLIB_010:75
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds
( F is isomorphism iff F " is isomorphism ) by Th71, Th72;

theorem :: GLIB_010:76
for G1, G2 being WGraph
for F being one-to-one PGraphMapping of G1,G2 holds
( F is weight-preserving iff F " is weight-preserving )
proof end;

theorem :: GLIB_010:77
for G1, G2 being EGraph
for F being one-to-one PGraphMapping of G1,G2 holds
( F is elabel-preserving iff F " is elabel-preserving )
proof end;

theorem :: GLIB_010:78
for G1, G2 being VGraph
for F being one-to-one PGraphMapping of G1,G2 holds
( F is vlabel-preserving iff F " is vlabel-preserving )
proof end;

theorem Th79: :: GLIB_010:79
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is onto holds
for v being Vertex of G2 holds ((F ") _V) . v is Vertex of G1 by Th34, Th72;

theorem :: GLIB_010:80
for G being _Graph holds (id G) " = id G
proof end;

theorem Th81: :: GLIB_010:81
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2 holds
( dom F = rng (F ") & rng F = dom (F ") )
proof end;

theorem Th82: :: GLIB_010:82
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2
for H being Subgraph of G1 holds (F | H) " = H |` (F ")
proof end;

theorem :: GLIB_010:83
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2
for H being Subgraph of G2 holds (H |` F) " = (F ") | H
proof end;

:: properties derived by use of F"
theorem Th84: :: GLIB_010:84
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 .order() = G2 .order() & G1 .size() = G2 .size() )
proof end;

theorem :: GLIB_010:85
for G1, G2 being _finite _Graph
for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & ex F0 being PGraphMapping of G1,G2 st F0 is isomorphism holds
F is isomorphism
proof end;

theorem :: GLIB_010:86
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds
card (G1 .edgesBetween (X,Y)) = card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))
proof end;

theorem :: GLIB_010:87
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X being Subset of (the_Vertices_of G1) st F is isomorphism holds
card (G1 .edgesBetween X) = card (G2 .edgesBetween ((F _V) .: X))
proof end;

theorem :: GLIB_010:88
for G1, G2 being _Graph
for F being directed PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds
card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))
proof end;

theorem :: GLIB_010:89
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopless implies G2 is loopless ) & ( G2 is loopless implies G1 is loopless ) & ( G1 is edgeless implies G2 is edgeless ) & ( G2 is edgeless implies G1 is edgeless ) & ( G1 is non-multi implies G2 is non-multi ) & ( G2 is non-multi implies G1 is non-multi ) & ( G1 is simple implies G2 is simple ) & ( G2 is simple implies G1 is simple ) & ( G1 is _finite implies G2 is _finite ) & ( G2 is _finite implies G1 is _finite ) & ( G1 is complete implies G2 is complete ) & ( G2 is complete implies G1 is complete ) )
proof end;

theorem :: GLIB_010:90
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Dcontinuous & F is isomorphism holds
( ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G1 is Dsimple implies G2 is Dsimple ) & ( G2 is Dsimple implies G1 is Dsimple ) )
proof end;

Lm4: for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2 holds card ((dom F) .loops()) c= card ((rng F) .loops())
proof end;

theorem :: GLIB_010:91
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2 holds card ((dom F) .loops()) = card ((rng F) .loops())
proof end;

theorem Th92: :: GLIB_010:92
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is total holds
card (G1 .loops()) c= card (G2 .loops())
proof end;

theorem Th93: :: GLIB_010:93
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is onto holds
card (G2 .loops()) c= card (G1 .loops())
proof end;

theorem :: GLIB_010:94
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds
card (G1 .loops()) = card (G2 .loops())
proof end;

theorem :: GLIB_010:95
for G1 being _Graph
for G2 being b1 -isomorphic _Graph holds G1 is G2 -isomorphic
proof end;

theorem :: GLIB_010:96
for G1 being _Graph
for G2 being b1 -Disomorphic _Graph holds G1 is G2 -Disomorphic
proof end;

theorem Th97: :: GLIB_010:97
for G1 being _Graph
for G2 being b1 -isomorphic _Graph
for G3 being b2 -isomorphic _Graph
for F being Isomorphism of G1,G2 st ex E being set st G3 is reverseEdgeDirections of G1,E holds
F " is Isomorphism of G2,G3
proof end;

theorem :: GLIB_010:98
for G1 being _Graph
for G2 being b1 -isomorphic _Graph
for G3 being b2 -isomorphic _Graph
for F being Isomorphism of G1,G2 st G1 == G3 holds
F " is Isomorphism of G2,G3
proof end;

theorem :: GLIB_010:99
for G1 being _Graph
for G2 being b1 -Disomorphic _Graph
for G3 being b2 -Disomorphic _Graph
for F being DIsomorphism of G1,G2 st G1 == G3 holds
F " is DIsomorphism of G2,G3
proof end;

:: define composition of graph mappings
definition
let G1, G2, G3 be _Graph;
let F1 be PGraphMapping of G1,G2;
let F2 be PGraphMapping of G2,G3;
func F2 * F1 -> PGraphMapping of G1,G3 equals :: GLIB_010:def 34
[((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))];
coherence
[((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))] is PGraphMapping of G1,G3
proof end;
end;

:: deftheorem defines * GLIB_010:def 34 :
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 holds F2 * F1 = [((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))];

theorem :: GLIB_010:100
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 holds
( (F2 * F1) _V = (F2 _V) * (F1 _V) & (F2 * F1) _E = (F2 _E) * (F1 _E) ) ;

theorem :: GLIB_010:101
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F2 * F1 is onto holds
F2 is onto
proof end;

theorem :: GLIB_010:102
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F2 * F1 is total holds
F1 is total
proof end;

registration
let G1, G2, G3 be _Graph;
let F1 be one-to-one PGraphMapping of G1,G2;
let F2 be one-to-one PGraphMapping of G2,G3;
cluster F2 * F1 -> one-to-one ;
coherence
F2 * F1 is one-to-one ;
end;

registration
let G1, G2, G3 be _Graph;
let F1 be semi-continuous PGraphMapping of G1,G2;
let F2 be semi-continuous PGraphMapping of G2,G3;
cluster F2 * F1 -> semi-continuous ;
coherence
F2 * F1 is semi-continuous
proof end;
end;

registration
let G1, G2, G3 be _Graph;
let F1 be continuous PGraphMapping of G1,G2;
let F2 be continuous PGraphMapping of G2,G3;
cluster F2 * F1 -> continuous ;
coherence
F2 * F1 is continuous
proof end;
end;

registration
let G1, G2, G3 be _Graph;
let F1 be directed PGraphMapping of G1,G2;
let F2 be directed PGraphMapping of G2,G3;
cluster F2 * F1 -> directed ;
coherence
F2 * F1 is directed
proof end;
end;

registration
let G1, G2, G3 be _Graph;
let F1 be semi-Dcontinuous PGraphMapping of G1,G2;
let F2 be semi-Dcontinuous PGraphMapping of G2,G3;
cluster F2 * F1 -> semi-Dcontinuous ;
coherence
F2 * F1 is semi-Dcontinuous
proof end;
end;

registration
let G1, G2, G3 be _Graph;
let F1 be Dcontinuous PGraphMapping of G1,G2;
let F2 be Dcontinuous PGraphMapping of G2,G3;
cluster F2 * F1 -> Dcontinuous ;
coherence
F2 * F1 is Dcontinuous
proof end;
end;

registration
let G1, G2, G3 be _Graph;
let F1 be empty PGraphMapping of G1,G2;
let F2 be PGraphMapping of G2,G3;
cluster F2 * F1 -> empty ;
coherence
F2 * F1 is empty ;
end;

registration
let G1, G2, G3 be _Graph;
let F1 be PGraphMapping of G1,G2;
let F2 be empty PGraphMapping of G2,G3;
cluster F2 * F1 -> empty ;
coherence
F2 * F1 is empty ;
end;

theorem Th103: :: GLIB_010:103
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is total & rng (F1 _V) c= dom (F2 _V) & rng (F1 _E) c= dom (F2 _E) holds
F2 * F1 is total by RELAT_1:27;

theorem Th104: :: GLIB_010:104
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is total & F2 is total holds
F2 * F1 is total
proof end;

theorem Th105: :: GLIB_010:105
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F2 is onto & dom (F2 _V) c= rng (F1 _V) & dom (F2 _E) c= rng (F1 _E) holds
F2 * F1 is onto by RELAT_1:28;

theorem Th106: :: GLIB_010:106
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is onto & F2 is onto holds
F2 * F1 is onto
proof end;

theorem :: GLIB_010:107
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is weak_SG-embedding & F2 is weak_SG-embedding holds
F2 * F1 is weak_SG-embedding by Th104;

theorem :: GLIB_010:108
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is strong_SG-embedding & F2 is strong_SG-embedding holds
F2 * F1 is strong_SG-embedding by Th104;

theorem Th109: :: GLIB_010:109
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is isomorphism & F2 is isomorphism holds
F2 * F1 is isomorphism by Th104, Th106;

theorem Th110: :: GLIB_010:110
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is Disomorphism & F2 is Disomorphism holds
F2 * F1 is Disomorphism
proof end;

theorem :: GLIB_010:111
for G1, G2, G3 being WGraph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is weight-preserving & F2 is weight-preserving holds
F2 * F1 is weight-preserving
proof end;

theorem :: GLIB_010:112
for G1, G2, G3 being EGraph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is elabel-preserving & F2 is elabel-preserving holds
F2 * F1 is elabel-preserving
proof end;

theorem :: GLIB_010:113
for G1, G2, G3 being VGraph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3 st F1 is vlabel-preserving & F2 is vlabel-preserving holds
F2 * F1 is vlabel-preserving
proof end;

theorem :: GLIB_010:114
for G1, G2, G3, G4 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3
for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1
proof end;

theorem :: GLIB_010:115
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds
( F * (F ") = id G2 & (F ") * F = id G1 )
proof end;

theorem :: GLIB_010:116
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F * (id G1) = F & (id G2) * F = F )
proof end;

theorem :: GLIB_010:117
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3
for H being Subgraph of G1 holds F2 * (F1 | H) = (F2 * F1) | H
proof end;

theorem :: GLIB_010:118
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3
for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)
proof end;

registration
let G1 be _Graph;
let G2 be G1 -isomorphic _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] G2 -isomorphic -> G1 -isomorphic for set ;
coherence
for b1 being _Graph st b1 is G2 -isomorphic holds
b1 is G1 -isomorphic
proof end;
end;

registration
let G1 be _Graph;
let G2 be G1 -Disomorphic _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] G2 -Disomorphic -> G1 -Disomorphic for set ;
coherence
for b1 being _Graph st b1 is G2 -Disomorphic holds
b1 is G1 -Disomorphic
proof end;
end;

definition
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
let W1 be Walk of G1;
attr W1 is F -defined means :Def35: :: GLIB_010:def 35
( W1 .vertices() c= dom (F _V) & W1 .edges() c= dom (F _E) );
end;

:: deftheorem Def35 defines -defined GLIB_010:def 35 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for W1 being Walk of G1 holds
( W1 is F -defined iff ( W1 .vertices() c= dom (F _V) & W1 .edges() c= dom (F _E) ) );

definition
let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;
let W2 be Walk of G2;
attr W2 is F -valued means :Def36: :: GLIB_010:def 36
( W2 .vertices() c= rng (F _V) & W2 .edges() c= rng (F _E) );
end;

:: deftheorem Def36 defines -valued GLIB_010:def 36 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for W2 being Walk of G2 holds
( W2 is F -valued iff ( W2 .vertices() c= rng (F _V) & W2 .edges() c= rng (F _E) ) );

registration
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1,G2;
cluster V5() Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like F -defined for Walk of G1;
existence
ex b1 being Walk of G1 st
( b1 is F -defined & b1 is V5() )
proof end;
cluster V5() Relation-like NAT -defined (the_Vertices_of G2) \/ (the_Edges_of G2) -valued Function-like FinSequence-like F -valued for Walk of G2;
existence
ex b1 being Walk of G2 st
( b1 is F -valued & b1 is V5() )
proof end;
end;

theorem :: GLIB_010:119
for G1, G2 being _Graph
for F being empty PGraphMapping of G1,G2
for W1 being Walk of G1 holds not W1 is F -defined by XBOOLE_1:3;

theorem :: GLIB_010:120
for G1, G2 being _Graph
for F being empty PGraphMapping of G1,G2
for W2 being Walk of G2 holds not W2 is F -valued by XBOOLE_1:3;

theorem Th121: :: GLIB_010:121
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for W1 being Walk of G1 st F is total holds
W1 is F -defined ;

theorem Th122: :: GLIB_010:122
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for W2 being Walk of G2 st F is onto holds
W2 is F -valued ;

registration
let G1, G2 be _Graph;
let F be one-to-one PGraphMapping of G1,G2;
cluster F -defined -> F " -valued for Walk of G1;
coherence
for b1 being Walk of G1 st b1 is F -defined holds
b1 is F " -valued by FUNCT_1:33;
cluster F -valued -> F " -defined for Walk of G2;
coherence
for b1 being Walk of G2 st b1 is F -valued holds
b1 is F " -defined by FUNCT_1:33;
end;

definition
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1,G2;
let W1 be F -defined Walk of G1;
func F .: W1 -> Walk of G2 means :Def37: :: GLIB_010:def 37
( (F _V) * (W1 .vertexSeq()) = it .vertexSeq() & (F _E) * (W1 .edgeSeq()) = it .edgeSeq() );
existence
ex b1 being Walk of G2 st
( (F _V) * (W1 .vertexSeq()) = b1 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b1 .edgeSeq() )
proof end;
uniqueness
for b1, b2 being Walk of G2 st (F _V) * (W1 .vertexSeq()) = b1 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b1 .edgeSeq() & (F _V) * (W1 .vertexSeq()) = b2 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b2 .edgeSeq() holds
b1 = b2 by GLIB_009:26;
end;

:: deftheorem Def37 defines .: GLIB_010:def 37 :
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1
for b5 being Walk of G2 holds
( b5 = F .: W1 iff ( (F _V) * (W1 .vertexSeq()) = b5 .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b5 .edgeSeq() ) );

registration
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1,G2;
let W1 be F -defined Walk of G1;
cluster F .: W1 -> F -valued ;
coherence
F .: W1 is F -valued
proof end;
end;

definition
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1,G2;
let W1 be F -defined Walk of G1;
:: original: .:
redefine func F .: W1 -> F -valued Walk of G2;
correctness
coherence
F .: W1 is F -valued Walk of G2;
;
end;

definition
let G1, G2 be _Graph;
let F be non empty one-to-one PGraphMapping of G1,G2;
let W2 be F -valued Walk of G2;
func F " W2 -> F -defined Walk of G1 equals :: GLIB_010:def 38
(F ") .: W2;
coherence
(F ") .: W2 is F -defined Walk of G1
proof end;
end;

:: deftheorem defines " GLIB_010:def 38 :
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2 holds F " W2 = (F ") .: W2;

Lm5: for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2 holds
( (F _V) * ((F " W2) .vertexSeq()) = W2 .vertexSeq() & (F _E) * ((F " W2) .edgeSeq()) = W2 .edgeSeq() )
proof end;

definition
let G1, G2 be _Graph;
let F be non empty one-to-one PGraphMapping of G1,G2;
let W2 be F -valued Walk of G2;
redefine func F " W2 means :: GLIB_010:def 39
( (F _V) * (it .vertexSeq()) = W2 .vertexSeq() & (F _E) * (it .edgeSeq()) = W2 .edgeSeq() );
compatibility
for b1 being F -defined Walk of G1 holds
( b1 = F " W2 iff ( (F _V) * (b1 .vertexSeq()) = W2 .vertexSeq() & (F _E) * (b1 .edgeSeq()) = W2 .edgeSeq() ) )
proof end;
end;

:: deftheorem defines " GLIB_010:def 39 :
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2
for b5 being b3 -defined Walk of G1 holds
( b5 = F " W2 iff ( (F _V) * (b5 .vertexSeq()) = W2 .vertexSeq() & (F _E) * (b5 .edgeSeq()) = W2 .edgeSeq() ) );

theorem Th123: :: GLIB_010:123
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1 holds F " (F .: W1) = W1
proof end;

theorem :: GLIB_010:124
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2 holds F .: (F " W2) = W2
proof end;

theorem Th125: :: GLIB_010:125
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1 holds
( W1 .length() = (F .: W1) .length() & len W1 = len (F .: W1) )
proof end;

theorem :: GLIB_010:126
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2 holds
( W2 .length() = (F " W2) .length() & len W2 = len (F " W2) ) by Th125;

theorem Th127: :: GLIB_010:127
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1 holds
( (F _V) . (W1 .first()) = (F .: W1) .first() & (F _V) . (W1 .last()) = (F .: W1) .last() )
proof end;

theorem :: GLIB_010:128
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2 holds
( ((F _V) ") . (W2 .first()) = (F " W2) .first() & ((F _V) ") . (W2 .last()) = (F " W2) .last() ) by Th127;

theorem Th129: :: GLIB_010:129
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1
for n being odd Element of NAT st n <= len W1 holds
(F _V) . (W1 . n) = (F .: W1) . n
proof end;

theorem :: GLIB_010:130
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1
for n being even Element of NAT st 1 <= n & n <= len W1 holds
(F _E) . (W1 . n) = (F .: W1) . n
proof end;

theorem Th131: :: GLIB_010:131
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1
for v, w being object st W1 is_Walk_from v,w holds
( v in dom (F _V) & w in dom (F _V) )
proof end;

theorem Th132: :: GLIB_010:132
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1
for v, w being object st W1 is_Walk_from v,w holds
F .: W1 is_Walk_from (F _V) . v,(F _V) . w
proof end;

theorem :: GLIB_010:133
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1
for v, w being object holds
( W1 is_Walk_from v,w iff ( v in dom (F _V) & w in dom (F _V) & F .: W1 is_Walk_from (F _V) . v,(F _V) . w ) )
proof end;

theorem :: GLIB_010:134
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1 st (F _V) . (W1 .first()) = (F _V) . (W1 .last()) holds
W1 .first() = W1 .last()
proof end;

theorem :: GLIB_010:135
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1 holds (F .: W1) .vertices() = (F _V) .: (W1 .vertices())
proof end;

theorem Th136: :: GLIB_010:136
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1 holds (F .: W1) .edges() = (F _E) .: (W1 .edges())
proof end;

theorem Th137: :: GLIB_010:137
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1 holds
( ( W1 is V5() implies F .: W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )
proof end;

theorem Th138: :: GLIB_010:138
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W1 being b3 -defined Walk of G1 holds
( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )
proof end;

:: properties derived using walks
theorem Th139: :: GLIB_010:139
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G2 is acyclic holds
G1 is acyclic
proof end;

theorem :: GLIB_010:140
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )
proof end;

theorem Th141: :: GLIB_010:141
for G1, G2 being _Graph
for E1, E2 being set
for G3 being reverseEdgeDirections of G1,E1
for G4 being reverseEdgeDirections of G2,E2
for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st
( F = F0 & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )
proof end;

theorem Th142: :: GLIB_010:142
for G1, G2 being _Graph
for E1, E2 being set
for G3 being reverseEdgeDirections of G1,E1
for G4 being reverseEdgeDirections of G2,E2
for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st
( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
proof end;

theorem Th143: :: GLIB_010:143
for G1 being _Graph
for G2 being b1 -isomorphic _Graph
for E1, E2 being set
for G3 being reverseEdgeDirections of G1,E1
for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic
proof end;

theorem Th144: :: GLIB_010:144
for G3, G4 being _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2
for F0 being PGraphMapping of G3,G4
for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
proof end;

theorem Th145: :: GLIB_010:145
for G3, G4 being _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2
for F0 being PGraphMapping of G3,G4
for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )
proof end;

theorem Th146: :: GLIB_010:146
for G3 being _Graph
for G4 being b1 -isomorphic _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds
G2 is G1 -isomorphic
proof end;

theorem Th147: :: GLIB_010:147
for G3 being _Graph
for G4 being b1 -Disomorphic _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds
G2 is G1 -Disomorphic
proof end;

theorem Th148: :: GLIB_010:148
for G3, G4 being _Graph
for v1, v2 being object
for G1 being addVertex of G3,v1
for G2 being addVertex of G4,v2
for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
proof end;

theorem :: GLIB_010:149
for G3, G4 being _Graph
for v1, v2 being object
for G1 being addVertex of G3,v1
for G2 being addVertex of G4,v2
for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )
proof end;

theorem :: GLIB_010:150
for G3 being _Graph
for G4 being b1 -isomorphic _Graph
for v1, v2 being object
for G1 being addVertex of G3,v1
for G2 being addVertex of G4,v2 holds
not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )
proof end;

theorem :: GLIB_010:151
for G3 being _Graph
for G4 being b1 -Disomorphic _Graph
for v1, v2 being object
for G1 being addVertex of G3,v1
for G2 being addVertex of G4,v2 holds
not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -Disomorphic )
proof end;

:: for F to be (semi-)continous, it is not enough for F0
:: to be (semi-)continuous. To see this, let G3 be the edgeless graph
:: with 2 vertices, G4 be the trivial edgeless graph, F0 the total PGM
:: from G3 to G4 and v1 <> v3. F0 is (semi-)continuous, but F is not,
:: since that would result in e2 Joins F_V.v1, F_V.v1, G2
:: (because F_V.v1 = F_V.v3), but not e1 Joins v1, v1, G1.
:: If v2 and v4 are additionally not isolated in rng F0, F would be
:: (semi-)continuous, but that theorem isn't proven here.
theorem Th152: :: GLIB_010:152
for G3, G4 being _Graph
for v1, v3 being Vertex of G3
for v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3
for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) )
proof end;

theorem :: GLIB_010:153
for G3, G4 being _Graph
for v1, v3 being Vertex of G3
for v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3
for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
proof end;

:: For (semi-)Dcontinuous, the same remarks as above apply.
theorem Th154: :: GLIB_010:154
for G3, G4 being _Graph
for v1, v3 being Vertex of G3
for v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3
for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )
proof end;

:: Similar to addEdge, the (semi-)(D)continuous properties are not
:: always carried over from F0 to F due to possible isolated vertices.
theorem Th155: :: GLIB_010:155
for G3, G4 being _Graph
for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v1,e1,v3
for G2 being addAdjVertex of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )
proof end;

theorem :: GLIB_010:156
for G3, G4 being _Graph
for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v1,e1,v3
for G2 being addAdjVertex of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )
proof end;

theorem Th157: :: GLIB_010:157
for G3, G4 being _Graph
for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v3,e1,v1
for G2 being addAdjVertex of G4,v4,e2,v2
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )
proof end;

theorem :: GLIB_010:158
for G3, G4 being _Graph
for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v3,e1,v1
for G2 being addAdjVertex of G4,v4,e2,v2
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )
proof end;

theorem :: GLIB_010:159
for G3, G4 being _Graph
for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v1,e1,v3
for G2 being addAdjVertex of G4,v4,e2,v2
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
proof end;

theorem :: GLIB_010:160
for G3, G4 being _Graph
for v3 being Vertex of G3
for v4 being Vertex of G4
for e1, e2, v1, v2 being object
for G1 being addAdjVertex of G3,v3,e1,v1
for G2 being addAdjVertex of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
proof end;

theorem :: GLIB_010:161
for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V holds G2 is G1 -isomorphic
proof end;

theorem Th162: :: GLIB_010:162
for G3, G4 being _Graph
for v1, v2 being object
for V1, V2 being set
for G1 being addAdjVertexAll of G3,v1,V1
for G2 being addAdjVertexAll of G4,v2,V2
for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds
ex F being PGraphMapping of G1,G2 st
( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
proof end;

theorem :: GLIB_010:163
for G3 being _Graph
for G4 being b1 -isomorphic _Graph
for v1, v2 being object
for G1 being addAdjVertexAll of G3,v1
for G2 being addAdjVertexAll of G4,v2 holds
not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )
proof end;

theorem Th164: :: GLIB_010:164
for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2
for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st
( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )
proof end;

theorem Th165: :: GLIB_010:165
for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2
for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st
( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )
proof end;

theorem Th166: :: GLIB_010:166
for G1 being _Graph
for G2 being b1 -isomorphic _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds G4 is G3 -isomorphic
proof end;

theorem Th167: :: GLIB_010:167
for G1 being _Graph
for G2 being b1 -Disomorphic _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic
proof end;

theorem Th168: :: GLIB_010:168
for G1 being _Graph
for G2 being b1 -isomorphic _Graph
for G3 being removeParallelEdges of G1
for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic
proof end;

theorem :: GLIB_010:169
for G1 being _Graph
for G2, G3 being removeParallelEdges of G1 holds G3 is G2 -isomorphic
proof end;

theorem Th170: :: GLIB_010:170
for G1 being _Graph
for G2 being b1 -Disomorphic _Graph
for G3 being removeDParallelEdges of G1
for G4 being removeDParallelEdges of G2 holds G4 is G3 -Disomorphic
proof end;

theorem :: GLIB_010:171
for G1 being _Graph
for G2, G3 being removeDParallelEdges of G1 holds G3 is G2 -Disomorphic
proof end;

theorem Th172: :: GLIB_010:172
for G1 being _Graph
for G2 being b1 -isomorphic _Graph
for G3 being SimpleGraph of G1
for G4 being SimpleGraph of G2 holds G4 is G3 -isomorphic
proof end;

theorem :: GLIB_010:173
for G1 being _Graph
for G2, G3 being SimpleGraph of G1 holds G3 is G2 -isomorphic
proof end;

theorem Th174: :: GLIB_010:174
for G1 being _Graph
for G2 being b1 -Disomorphic _Graph
for G3 being DSimpleGraph of G1
for G4 being DSimpleGraph of G2 holds G4 is G3 -Disomorphic
proof end;

theorem :: GLIB_010:175
for G1 being _Graph
for G2, G3 being DSimpleGraph of G1 holds G3 is G2 -Disomorphic
proof end;

theorem :: GLIB_010:176
for G1, G2 being loopless _trivial _Graph
for F being non empty PGraphMapping of G1,G2 holds
( F is Disomorphism & F = [( the Vertex of G1 .--> the Vertex of G2),{}] )
proof end;

theorem :: GLIB_010:177
for G1, G2 being _trivial _Graph st G1 .size() = G2 .size() holds
ex F being PGraphMapping of G1,G2 st F is Disomorphism
proof end;

:: sadly, the attribute notation is not compatible with the following notation
::registration
:: let G be trivial loopless _Graph;
:: cluster trivial loopless -> G-Disomorphic for _Graph;
:: coherence;
::end;
:: but normal theorems will do
:: Right Now, this is the only class of graphs that can
:: solely be determined by its attributes. More will come in the future.
theorem :: GLIB_010:178
for G1, G2 being loopless _trivial _Graph holds
( G2 is G1 -Disomorphic & G2 is G1 -isomorphic )
proof end;