let G1, G2 be loopless _trivial _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2 holds

( F is Disomorphism & F = [( the Vertex of G1 .--> the Vertex of G2),{}] )

let F be non empty PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism & F = [( the Vertex of G1 .--> the Vertex of G2),{}] )

thus F is Disomorphism ; :: thesis: F = [( the Vertex of G1 .--> the Vertex of G2),{}]

A1: F _E = {} ;

( F is total & F is onto ) ;

then A2: ( dom (F _V) = the_Vertices_of G1 & rng (F _V) = the_Vertices_of G2 ) ;

consider v1 being Vertex of G1 such that

A3: the_Vertices_of G1 = {v1} by GLIB_000:22;

consider v2 being Vertex of G2 such that

A4: the_Vertices_of G2 = {v2} by GLIB_000:22;

( dom (F _V) = { the Vertex of G1} & rng (F _V) = { the Vertex of G2} ) by A2, A3, A4, TARSKI:def 1;

then F _V = the Vertex of G1 .--> the Vertex of G2 by FUNCT_4:112;

hence F = [( the Vertex of G1 .--> the Vertex of G2),{}] by A1; :: thesis: verum

( F is Disomorphism & F = [( the Vertex of G1 .--> the Vertex of G2),{}] )

let F be non empty PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism & F = [( the Vertex of G1 .--> the Vertex of G2),{}] )

thus F is Disomorphism ; :: thesis: F = [( the Vertex of G1 .--> the Vertex of G2),{}]

A1: F _E = {} ;

( F is total & F is onto ) ;

then A2: ( dom (F _V) = the_Vertices_of G1 & rng (F _V) = the_Vertices_of G2 ) ;

consider v1 being Vertex of G1 such that

A3: the_Vertices_of G1 = {v1} by GLIB_000:22;

consider v2 being Vertex of G2 such that

A4: the_Vertices_of G2 = {v2} by GLIB_000:22;

( dom (F _V) = { the Vertex of G1} & rng (F _V) = { the Vertex of G2} ) by A2, A3, A4, TARSKI:def 1;

then F _V = the Vertex of G1 .--> the Vertex of G2 by FUNCT_4:112;

hence F = [( the Vertex of G1 .--> the Vertex of G2),{}] by A1; :: thesis: verum