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 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
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 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
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 holds
( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) ) implies [f,g] is semi-continuous 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 holds
( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) ; :: thesis: [f,g] is semi-continuous PGraphMapping of G1,G2
A3: 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 A2;
reconsider F = [f,g] as PGraphMapping of G1,G2 by A1, A3, Th8;
F is semi-continuous by A2;
hence [f,g] is semi-continuous PGraphMapping of G1,G2 ; :: thesis: verum