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 (the_Edges_of G2) by GLIB_000:def 25;
then card (the_Edges_of G1) = card (the_Edges_of G2) 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 CARD_1:5, WELLORD2:def 4;
reconsider g = g as Function of (the_Edges_of G1),(the_Edges_of G2) by A1, FUNCT_2:1;
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 (the_Vertices_of G1) ;
reconsider f = V --> w as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) ;

now :: thesis: ( ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . 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
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A2, FUNCT_2:5;
hence for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . 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 A5, FUNCOP_1:7;
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A5, A4;
then ( (the_Source_of G1) . e = v1 & (the_Target_of G1) . e = w1 ) by A6, TARSKI:def 1;
then A8: e Joins v1,w1,G1 by A5, GLIB_000:def 13;
A9: g . e in the_Edges_of G2 by A1, A5, FUNCT_1:3;
then ( (the_Source_of G2) . (g . e) in the_Vertices_of G2 & (the_Target_of G2) . (g . e) in the_Vertices_of G2 ) by FUNCT_2:5;
then ( (the_Source_of G2) . (g . e) = w & (the_Target_of G2) . (g . e) = w ) by A3, TARSKI:def 1;
then g . e Joins f . v1,f . w1,G2 by A7, A9, GLIB_000:def 13;
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 A1, A3, FUNCOP_1:88;
F is one-to-one by A1, A11;
hence F is Disomorphism by A10, A12; :: thesis: verum