let G1, G2 be _trivial _Graph; ( G1 .size() = G2 .size() implies ex F being PGraphMapping of G1,G2 st F is Disomorphism )
assume
G1 .size() = G2 .size()
; 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 ( ( 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 )
;
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 ;
( 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 )
;
( 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;
verum end;
then reconsider F = [f,g] as semi-continuous PGraphMapping of G1,G2 by Th31;
take
F
; 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; verum