let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 holds
( dom (F _E) c= G1 .edgesBetween (dom (F _V)) & rng (F _E) c= G2 .edgesBetween (rng (F _V)) )
let F be PGraphMapping of G1,G2; :: thesis: ( dom (F _E) c= G1 .edgesBetween (dom (F _V)) & rng (F _E) c= G2 .edgesBetween (rng (F _V)) )
for e being object st e in dom (F _E) holds
e in G1 .edgesBetween (dom (F _V))
proof
let e be object ; :: thesis: ( e in dom (F _E) implies e in G1 .edgesBetween (dom (F _V)) )
assume A1: e in dom (F _E) ; :: thesis: e in G1 .edgesBetween (dom (F _V))
then ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by Th5;
hence e in G1 .edgesBetween (dom (F _V)) by A1, GLIB_000:31; :: thesis: verum
end;
hence dom (F _E) c= G1 .edgesBetween (dom (F _V)) by TARSKI:def 3; :: thesis: rng (F _E) c= G2 .edgesBetween (rng (F _V))
for e being object st e in rng (F _E) holds
e in G2 .edgesBetween (rng (F _V))
proof
let e be object ; :: thesis: ( e in rng (F _E) implies e in G2 .edgesBetween (rng (F _V)) )
assume A2: e in rng (F _E) ; :: thesis: e in G2 .edgesBetween (rng (F _V))
then ( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) ) by Th6;
hence e in G2 .edgesBetween (rng (F _V)) by A2, GLIB_000:31; :: thesis: verum
end;
hence rng (F _E) c= G2 .edgesBetween (rng (F _V)) by TARSKI:def 3; :: thesis: verum