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

for e being object st e in rng (F _E) holds

e in G2 .edgesBetween (rng (F _V))

( 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

hence
dom (F _E) c= G1 .edgesBetween (dom (F _V))
by TARSKI:def 3; :: thesis: rng (F _E) c= G2 .edgesBetween (rng (F _V))
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;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

for e being object st e in rng (F _E) holds

e in G2 .edgesBetween (rng (F _V))

proof

hence
rng (F _E) c= G2 .edgesBetween (rng (F _V))
by TARSKI:def 3; :: thesis: verum
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;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