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) ;

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

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 ) ) )

then reconsider F = [f,g] as semi-continuous PGraphMapping of G1,G2 by Th31;( (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;( (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

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