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

now :: thesis: for v being Vertex of G2 ex e being object st e Joins v,v,G2

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

end;

hence G2 is loopfull ; :: thesis: verum