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 )

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

( 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 )

assume A4:
dom F == G1
; :: thesis: 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 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

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