let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2 holds

( dom F = rng (F ") & rng F = dom (F ") )

let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: ( dom F = rng (F ") & rng F = dom (F ") )

A1: the_Vertices_of (dom F) = dom (F _V) by Th54

.= rng ((F _V) ") by FUNCT_1:33

.= the_Vertices_of (rng (F ")) by Th54 ;

the_Edges_of (dom F) = dom (F _E) by Th54

.= rng ((F _E) ") by FUNCT_1:33

.= the_Edges_of (rng (F ")) by Th54 ;

hence dom F = rng (F ") by A1, GLIB_000:86, GLIB_009:44; :: thesis: rng F = dom (F ")

A2: the_Vertices_of (rng F) = rng (F _V) by Th54

.= dom ((F _V) ") by FUNCT_1:33

.= the_Vertices_of (dom (F ")) by Th54 ;

the_Edges_of (rng F) = rng (F _E) by Th54

.= dom ((F _E) ") by FUNCT_1:33

.= the_Edges_of (dom (F ")) by Th54 ;

hence rng F = dom (F ") by A2, GLIB_000:86, GLIB_009:44; :: thesis: verum

( dom F = rng (F ") & rng F = dom (F ") )

let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: ( dom F = rng (F ") & rng F = dom (F ") )

A1: the_Vertices_of (dom F) = dom (F _V) by Th54

.= rng ((F _V) ") by FUNCT_1:33

.= the_Vertices_of (rng (F ")) by Th54 ;

the_Edges_of (dom F) = dom (F _E) by Th54

.= rng ((F _E) ") by FUNCT_1:33

.= the_Edges_of (rng (F ")) by Th54 ;

hence dom F = rng (F ") by A1, GLIB_000:86, GLIB_009:44; :: thesis: rng F = dom (F ")

A2: the_Vertices_of (rng F) = rng (F _V) by Th54

.= dom ((F _V) ") by FUNCT_1:33

.= the_Vertices_of (dom (F ")) by Th54 ;

the_Edges_of (rng F) = rng (F _E) by Th54

.= dom ((F _E) ") by FUNCT_1:33

.= the_Edges_of (dom (F ")) by Th54 ;

hence rng F = dom (F ") by A2, GLIB_000:86, GLIB_009:44; :: thesis: verum