let F1, F2 be non empty one-to-one Graph-yielding Function; ( F1,F2 are_isomorphic implies rng F1, rng F2 are_isomorphic )
assume
F1,F2 are_isomorphic
; rng F1, rng F2 are_isomorphic
then consider p being one-to-one Function such that
A1:
( dom p = dom F1 & rng p = dom F2 )
and
A2:
for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic )
;
reconsider f = (F2 * p) * (F1 ") as one-to-one Function ;
take
f
; GLIB_015:def 13 ( dom f = rng F1 & rng f = rng F2 & ( for G being _Graph st G in rng F1 holds
f . G is b1 -isomorphic _Graph ) )
A3: dom (F2 * p) =
dom p
by A1, RELAT_1:27
.=
rng (F1 ")
by A1, FUNCT_1:33
;
hence dom f =
dom (F1 ")
by RELAT_1:27
.=
rng F1
by FUNCT_1:33
;
( rng f = rng F2 & ( for G being _Graph st G in rng F1 holds
f . G is b1 -isomorphic _Graph ) )
thus rng f =
rng (F2 * p)
by A3, RELAT_1:28
.=
rng F2
by A1, RELAT_1:28
; for G being _Graph st G in rng F1 holds
f . G is b1 -isomorphic _Graph
let G be _Graph; ( G in rng F1 implies f . G is G -isomorphic _Graph )
assume
G in rng F1
; f . G is G -isomorphic _Graph
then consider x being object such that
A4:
( x in dom F1 & F1 . x = G )
by FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A5:
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic )
by A2, A4;
F1 . x in rng F1
by A4, FUNCT_1:3;
then A6:
G in dom (F1 ")
by A4, FUNCT_1:33;
then
G in dom f
by A3, RELAT_1:27;
then A7:
G in dom (F2 * (p * (F1 ")))
by RELAT_1:36;
G2 =
F2 . (p . ((F1 ") . (F1 . x)))
by A4, A5, FUNCT_1:34
.=
F2 . ((p * (F1 ")) . G)
by A4, A6, FUNCT_1:13
.=
(F2 * (p * (F1 "))) . G
by A7, FUNCT_1:12
.=
f . G
by RELAT_1:36
;
hence
f . G is G -isomorphic _Graph
by A4, A5; verum