let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for e being object st e in rng (F _E) holds
( () . e in rng (F _V) & () . e in rng (F _V) )

let F be PGraphMapping of G1,G2; :: thesis: for e being object st e in rng (F _E) holds
( () . e in rng (F _V) & () . e in rng (F _V) )

let e be object ; :: thesis: ( e in rng (F _E) implies ( () . e in rng (F _V) & () . e in rng (F _V) ) )
assume e in rng (F _E) ; :: thesis: ( () . e in rng (F _V) & () . 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) & () . e0 in dom (F _V) ) by ;
e0 Joins () . e0,() . e0,G1 by ;
then (F _E) . e0 Joins (F _V) . (() . e0),(F _V) . (() . e0),G2 by A1, A2, Th4;
per cases ) . e = (F _V) . (() . e0) & () . e = (F _V) . (() . e0) ) or ( () . e = (F _V) . (() . e0) & () . e = (F _V) . (() . e0) ) ) by ;
suppose ( (the_Source_of G2) . e = (F _V) . (() . e0) & () . e = (F _V) . (() . e0) ) ; :: thesis: ( () . e in rng (F _V) & () . e in rng (F _V) )
hence ( (the_Source_of G2) . e in rng (F _V) & () . e in rng (F _V) ) by ; :: thesis: verum
end;
suppose ( (the_Target_of G2) . e = (F _V) . (() . e0) & () . e = (F _V) . (() . e0) ) ; :: thesis: ( () . e in rng (F _V) & () . e in rng (F _V) )
hence ( (the_Source_of G2) . e in rng (F _V) & () . e in rng (F _V) ) by ; :: thesis: verum
end;
end;