let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is total holds

( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )

let F be PGraphMapping of G1,G2; :: thesis: ( F is total implies ( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) ) )

assume A1: F is total ; :: thesis: ( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )

( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )

let F be PGraphMapping of G1,G2; :: thesis: ( F is total implies ( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) ) )

assume A1: F is total ; :: thesis: ( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )

hereby :: thesis: ( G2 is edgeless implies G1 is edgeless )

thus
( G2 is edgeless implies G1 is edgeless )
by A1; :: thesis: verumassume A2:
G2 is loopless
; :: thesis: G1 is loopless

for e being object holds

( not e in the_Edges_of G1 or not (the_Source_of G1) . e = (the_Target_of G1) . e )

end;for e being object holds

( not e in the_Edges_of G1 or not (the_Source_of G1) . e = (the_Target_of G1) . e )

proof

hence
G1 is loopless
by GLIB_000:def 18; :: thesis: verum
given e being object such that A3:
e in the_Edges_of G1
and

A4: (the_Source_of G1) . e = (the_Target_of G1) . e ; :: thesis: contradiction

set v = (the_Source_of G1) . e;

A5: e Joins (the_Source_of G1) . e,(the_Source_of G1) . e,G1 by A3, A4, GLIB_000:def 13;

then (the_Source_of G1) . e in dom (F _V) by A1, GLIB_000:13;

then (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Source_of G1) . e),G2 by A1, A3, A5, Th4;

hence contradiction by A2, GLIB_000:18; :: thesis: verum

end;A4: (the_Source_of G1) . e = (the_Target_of G1) . e ; :: thesis: contradiction

set v = (the_Source_of G1) . e;

A5: e Joins (the_Source_of G1) . e,(the_Source_of G1) . e,G1 by A3, A4, GLIB_000:def 13;

then (the_Source_of G1) . e in dom (F _V) by A1, GLIB_000:13;

then (F _E) . e Joins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Source_of G1) . e),G2 by A1, A3, A5, Th4;

hence contradiction by A2, GLIB_000:18; :: thesis: verum