let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is semi-continuous & dom (F _V) = the_Vertices_of G1 & G2 .loops() c= rng (F _E) & G2 is loopfull holds
G1 is loopfull
let F be PGraphMapping of G1,G2; :: thesis: ( F is semi-continuous & dom (F _V) = the_Vertices_of G1 & G2 .loops() c= rng (F _E) & G2 is loopfull implies G1 is loopfull )
assume that
A1: F is semi-continuous and
A2: ( dom (F _V) = the_Vertices_of G1 & G2 .loops() c= rng (F _E) ) and
A3: G2 is loopfull ; :: thesis: G1 is loopfull

now :: thesis: for v being Vertex of G1 ex e0 being object st e0 Joins v,v,G1

let v be Vertex of G1; :: thesis: ex e0 being object st e0 Joins v,v,G1
(F _V) . v in rng (F _V) by A2, FUNCT_1:3;
then consider e being object such that
A4: e Joins (F _V) . v,(F _V) . v,G2 by A3;
e in G2 .loops() by A4, GLIB_009:def 2;
then consider e0 being object such that
A5: ( e0 in dom (F _E) & (F _E) . e0 = e ) by A2, FUNCT_1:def 3;
take e0 = e0; :: thesis: e0 Joins v,v,G1
thus e0 Joins v,v,G1 by A1, A2, A4, A5, GLIB_010:def 15; :: thesis: verum

end;

hence G1 is loopfull ; :: thesis: verum