let F1, F2 be non empty one-to-one Graph-yielding Function; :: thesis: ( F1,F2 are_Disomorphic implies rng F1, rng F2 are_Disomorphic )
assume F1,F2 are_Disomorphic ; :: thesis: rng F1, rng F2 are_Disomorphic
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 -Disomorphic ) ;
reconsider f = (F2 * p) * (F1 ") as one-to-one Function ;
take f ; :: according to GLIB_015:def 12 :: thesis: ( dom f = rng F1 & rng f = rng F2 & ( for G being _Graph st G in rng F1 holds
f . G is b₁ -Disomorphic _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 ;
:: thesis: ( rng f = rng F2 & ( for G being _Graph st G in rng F1 holds
f . G is b₁ -Disomorphic _Graph ) )
thus rng f = rng (F2 * p) by A3, RELAT_1:28
.= rng F2 by A1, RELAT_1:28 ; :: thesis: for G being _Graph st G in rng F1 holds
f . G is b₁ -Disomorphic _Graph
let G be _Graph; :: thesis: ( G in rng F1 implies f . G is G -Disomorphic _Graph )
assume G in rng F1 ; :: thesis: f . G is G -Disomorphic _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 -Disomorphic ) 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 -Disomorphic _Graph by A4, A5; :: thesis: verum