let G1, G2 be _Graph; :: thesis: 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

let f be PartFunc of (the_Vertices_of G1),(the_Vertices_of G2); :: thesis: 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

let g be PartFunc of (the_Edges_of G1),(the_Edges_of G2); :: thesis: ( ( 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 ) implies [f,g] is PGraphMapping of G1,G2 )

assume that

A1: for e being object st e in dom g holds

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

A2: 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 ; :: thesis: [f,g] is PGraphMapping of G1,G2

A3: ( dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 ) ;

A4: ( dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 ) ;

take f ; :: according to GLIB_010:def 8 :: thesis: ex g being Function st

( [f,g] = [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 ) )

take g ; :: thesis: ( [f,g] = [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 ) )

thus ( [f,g] = [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 ) ) by A1, A2, A3, A4; :: thesis: verum

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

let f be PartFunc of (the_Vertices_of G1),(the_Vertices_of G2); :: thesis: 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

let g be PartFunc of (the_Edges_of G1),(the_Edges_of G2); :: thesis: ( ( 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 ) implies [f,g] is PGraphMapping of G1,G2 )

assume that

A1: for e being object st e in dom g holds

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

A2: 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 ; :: thesis: [f,g] is PGraphMapping of G1,G2

A3: ( dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 ) ;

A4: ( dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 ) ;

take f ; :: according to GLIB_010:def 8 :: thesis: ex g being Function st

( [f,g] = [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 ) )

take g ; :: thesis: ( [f,g] = [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 ) )

thus ( [f,g] = [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 ) ) by A1, A2, A3, A4; :: thesis: verum