let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2 holds
( F is total iff dom F == G1 )
let F be non empty PGraphMapping of G1,G2; :: thesis: ( F is total iff dom F == G1 )

hereby :: thesis: ( dom F == G1 implies F is total )

A1: G1 is Subgraph of G1 by GLIB_000:40;
assume A2: F is total ; :: thesis: dom F == G1
A3: the_Vertices_of (dom F) = the_Vertices_of G1 by A2, Th54;
the_Edges_of (dom F) = the_Edges_of G1 by A2, Th54;
hence dom F == G1 by A1, A3, GLIB_000:86; :: thesis: verum

end;

assume A4: dom F == G1 ; :: thesis: F is total
A5: dom (F _V) = the_Vertices_of (dom F) by Th54
.= the_Vertices_of G1 by A4, GLIB_000:def 34 ;
dom (F _E) = the_Edges_of (dom F) by Th54
.= the_Edges_of G1 by A4, GLIB_000:def 34 ;
hence F is total by A5; :: thesis: verum