reconsider f = (F _V) " as PartFunc of (the_Vertices_of G2),(the_Vertices_of G1) ;

reconsider g = (F _E) " as PartFunc of (the_Edges_of G2),(the_Edges_of G1) ;

reconsider g = (F _E) " as PartFunc of (the_Edges_of G2),(the_Edges_of G1) ;

now :: thesis: ( ( for e being object st e in dom g holds

( (the_Source_of G2) . e in dom f & (the_Target_of G2) . 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,G2 holds

g . e Joins f . v,f . w,G1 ) )

assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G2 implies g . e Joins f . v,f . w,G1 )

then A1: ( e in rng (F _E) & v in rng (F _V) & w in rng (F _V) ) by FUNCT_1:33;

then consider e0 being object such that

A2: ( e0 in dom (F _E) & (F _E) . e0 = e ) by FUNCT_1:def 3;

consider v0 being object such that

A3: ( v0 in dom (F _V) & (F _V) . v0 = v ) by A1, FUNCT_1:def 3;

consider w0 being object such that

A4: ( w0 in dom (F _V) & (F _V) . w0 = w ) by A1, FUNCT_1:def 3;

A5: ( g . e = e0 & f . v = v0 & f . w = w0 ) by A2, A3, A4, FUNCT_1:34;

A6: F is semi-continuous ;

assume e Joins v,w,G2 ; :: thesis: g . e Joins f . v,f . w,G1

then (F _E) . e0 Joins (F _V) . v0,(F _V) . w0,G2 by A2, A3, A4;

hence g . e Joins f . v,f . w,G1 by A2, A3, A4, A5, A6; :: thesis: verum

end;

hence
[((F _V) "),((F _E) ")] is PGraphMapping of G2,G1
by Th8; :: thesis: verum( (the_Source_of G2) . e in dom f & (the_Target_of G2) . 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,G2 holds

g . e Joins f . v,f . w,G1 ) )

hereby :: thesis: for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G2 holds

g . e Joins f . v,f . w,G1

let e, v, w be object ; :: thesis: ( e in dom g & v in dom f & w in dom f & e Joins v,w,G2 implies g . e Joins f . v,f . w,G1 )g . e Joins f . v,f . w,G1

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f ) )

assume e in dom g ; :: thesis: ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f )

then e in rng (F _E) by FUNCT_1:33;

then ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) ) by Th6;

hence ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f ) by FUNCT_1:33; :: thesis: verum

end;assume e in dom g ; :: thesis: ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f )

then e in rng (F _E) by FUNCT_1:33;

then ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) ) by Th6;

hence ( (the_Source_of G2) . e in dom f & (the_Target_of G2) . e in dom f ) by FUNCT_1:33; :: thesis: verum

assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G2 implies g . e Joins f . v,f . w,G1 )

then A1: ( e in rng (F _E) & v in rng (F _V) & w in rng (F _V) ) by FUNCT_1:33;

then consider e0 being object such that

A2: ( e0 in dom (F _E) & (F _E) . e0 = e ) by FUNCT_1:def 3;

consider v0 being object such that

A3: ( v0 in dom (F _V) & (F _V) . v0 = v ) by A1, FUNCT_1:def 3;

consider w0 being object such that

A4: ( w0 in dom (F _V) & (F _V) . w0 = w ) by A1, FUNCT_1:def 3;

A5: ( g . e = e0 & f . v = v0 & f . w = w0 ) by A2, A3, A4, FUNCT_1:34;

A6: F is semi-continuous ;

assume e Joins v,w,G2 ; :: thesis: g . e Joins f . v,f . w,G1

then (F _E) . e0 Joins (F _V) . v0,(F _V) . w0,G2 by A2, A3, A4;

hence g . e Joins f . v,f . w,G1 by A2, A3, A4, A5, A6; :: thesis: verum