let G1, G2 be _Graph; :: thesis: for F being continuous PGraphMapping of G1,G2 st rng (F _V) = the_Vertices_of G2 & G1 is loopless holds

G2 is loopless

let F be continuous PGraphMapping of G1,G2; :: thesis: ( rng (F _V) = the_Vertices_of G2 & G1 is loopless implies G2 is loopless )

assume A1: rng (F _V) = the_Vertices_of G2 ; :: thesis: ( not G1 is loopless or G2 is loopless )

assume A2: G1 is loopless ; :: thesis: G2 is loopless

for v, e being object holds not e Joins v,v,G2

G2 is loopless

let F be continuous PGraphMapping of G1,G2; :: thesis: ( rng (F _V) = the_Vertices_of G2 & G1 is loopless implies G2 is loopless )

assume A1: rng (F _V) = the_Vertices_of G2 ; :: thesis: ( not G1 is loopless or G2 is loopless )

assume A2: G1 is loopless ; :: thesis: G2 is loopless

for v, e being object holds not e Joins v,v,G2

proof

hence
G2 is loopless
by GLIB_000:18; :: thesis: verum
let v be object ; :: thesis: for e being object holds not e Joins v,v,G2

given e9 being object such that A3: e9 Joins v,v,G2 ; :: thesis: contradiction

v in rng (F _V) by A1, A3, GLIB_000:13;

then consider v0 being object such that

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

consider e being object such that

A5: ( e Joins v0,v0,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A3, A4, Def16;

thus contradiction by A2, A5, GLIB_000:18; :: thesis: verum

end;given e9 being object such that A3: e9 Joins v,v,G2 ; :: thesis: contradiction

v in rng (F _V) by A1, A3, GLIB_000:13;

then consider v0 being object such that

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

consider e being object such that

A5: ( e Joins v0,v0,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A3, A4, Def16;

thus contradiction by A2, A5, GLIB_000:18; :: thesis: verum