let G1, G2 be _trivial _Graph; :: thesis: ( G1 .size() = G2 .size() implies ex F being PGraphMapping of G1,G2 st F is Disomorphism )
assume G1 .size() = G2 .size() ; :: thesis: ex F being PGraphMapping of G1,G2 st F is Disomorphism
then G1 .size() = card () by GLIB_000:def 25;
then card () = card () by GLIB_000:def 25;
then consider g being Function such that
A1: ( g is one-to-one & dom g = the_Edges_of G1 & rng g = the_Edges_of G2 ) by ;
reconsider g = g as Function of (),() by ;
consider v being Vertex of G1 such that
A2: the_Vertices_of G1 = {v} by GLIB_000:22;
consider w being Vertex of G2 such that
A3: the_Vertices_of G2 = {w} by GLIB_000:22;
reconsider V = {v} as Subset of () ;
reconsider f = V --> w as PartFunc of (),() ;
now :: thesis: ( ( for e being object st e in dom g holds
( () . e in dom f & () . e in dom f ) ) & ( for e, v1, w1 being object st e in dom g & v1 in dom f & w1 in dom f holds
( e Joins v1,w1,G1 iff g . e Joins f . v1,f . w1,G2 ) ) )
A4: for e being object st e in dom g holds
( () . e in dom f & () . e in dom f ) by ;
hence for e being object st e in dom g holds
( () . e in dom f & () . e in dom f ) ; :: thesis: for e, v1, w1 being object st e in dom g & v1 in dom f & w1 in dom f holds
( e Joins v1,w1,G1 iff g . e Joins f . v1,f . w1,G2 )

let e, v1, w1 be object ; :: thesis: ( e in dom g & v1 in dom f & w1 in dom f implies ( e Joins v1,w1,G1 iff g . e Joins f . v1,f . w1,G2 ) )
assume A5: ( e in dom g & v1 in dom f & w1 in dom f ) ; :: thesis: ( e Joins v1,w1,G1 iff g . e Joins f . v1,f . w1,G2 )
then A6: ( v1 = v & w1 = v ) by TARSKI:def 1;
A7: ( f . v1 = w & f . w1 = w ) by ;
( (the_Source_of G1) . e in dom f & () . e in dom f ) by A5, A4;
then ( (the_Source_of G1) . e = v1 & () . e = w1 ) by ;
then A8: e Joins v1,w1,G1 by ;
A9: g . e in the_Edges_of G2 by ;
then ( (the_Source_of G2) . (g . e) in the_Vertices_of G2 & () . (g . e) in the_Vertices_of G2 ) by FUNCT_2:5;
then ( (the_Source_of G2) . (g . e) = w & () . (g . e) = w ) by ;
then g . e Joins f . v1,f . w1,G2 by ;
hence ( e Joins v1,w1,G1 iff g . e Joins f . v1,f . w1,G2 ) by A8; :: thesis: verum
end;
then reconsider F = [f,g] as semi-continuous PGraphMapping of G1,G2 by Th31;
take F ; :: thesis: F is Disomorphism
A10: F is total by A1, A2;
A11: f = v .--> w by FUNCOP_1:def 9;
then A12: F is onto by ;
F is one-to-one by ;
hence F is Disomorphism by ; :: thesis: verum