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