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

let F be PGraphMapping of G1,G2; :: thesis: 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) )

let e be object ; :: thesis: ( e in rng (F _E) implies ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) ) )

assume e in rng (F _E) ; :: thesis: ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )

then consider e0 being object such that

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

A2: ( (the_Source_of G1) . e0 in dom (F _V) & (the_Target_of G1) . e0 in dom (F _V) ) by A1, Th5;

e0 Joins (the_Source_of G1) . e0,(the_Target_of G1) . e0,G1 by A1, GLIB_000:def 13;

then (F _E) . e0 Joins (F _V) . ((the_Source_of G1) . e0),(F _V) . ((the_Target_of G1) . e0),G2 by A1, A2, Th4;

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) )

let F be PGraphMapping of G1,G2; :: thesis: 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) )

let e be object ; :: thesis: ( e in rng (F _E) implies ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) ) )

assume e in rng (F _E) ; :: thesis: ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )

then consider e0 being object such that

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

A2: ( (the_Source_of G1) . e0 in dom (F _V) & (the_Target_of G1) . e0 in dom (F _V) ) by A1, Th5;

e0 Joins (the_Source_of G1) . e0,(the_Target_of G1) . e0,G1 by A1, GLIB_000:def 13;

then (F _E) . e0 Joins (F _V) . ((the_Source_of G1) . e0),(F _V) . ((the_Target_of G1) . e0),G2 by A1, A2, Th4;

per cases then
( ( (the_Source_of G2) . e = (F _V) . ((the_Source_of G1) . e0) & (the_Target_of G2) . e = (F _V) . ((the_Target_of G1) . e0) ) or ( (the_Target_of G2) . e = (F _V) . ((the_Source_of G1) . e0) & (the_Source_of G2) . e = (F _V) . ((the_Target_of G1) . e0) ) )
by A1, GLIB_000:def 13;

end;

suppose
( (the_Source_of G2) . e = (F _V) . ((the_Source_of G1) . e0) & (the_Target_of G2) . e = (F _V) . ((the_Target_of G1) . e0) )
; :: thesis: ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )

hence
( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )
by A2, FUNCT_1:def 3; :: thesis: verum

end;suppose
( (the_Target_of G2) . e = (F _V) . ((the_Source_of G1) . e0) & (the_Source_of G2) . e = (F _V) . ((the_Target_of G1) . e0) )
; :: thesis: ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )

hence
( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )
by A2, FUNCT_1:def 3; :: thesis: verum

end;