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

proof

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;

hence G2 is loopless by GLIB_000:18; :: thesis: verum