let G1, G2 be _Graph; :: thesis: for x, y being object holds
( x .--> G1,y .--> G2 are_Disomorphic iff G2 is G1 -Disomorphic )
let x, y be object ; :: thesis: ( x .--> G1,y .--> G2 are_Disomorphic iff G2 is G1 -Disomorphic )

hereby :: thesis: ( G2 is G1 -Disomorphic implies x .--> G1,y .--> G2 are_Disomorphic )

assume x .--> G1,y .--> G2 are_Disomorphic ; :: thesis: G2 is G1 -Disomorphic
then consider p being one-to-one Function such that
A1: ( dom p = dom (x .--> G1) & rng p = dom (y .--> G2) ) and
A2: for z being object st z in dom (x .--> G1) holds
ex G3, G4 being _Graph st
( G3 = (x .--> G1) . z & G4 = (y .--> G2) . (p . z) & G4 is G3 -Disomorphic ) ;
( dom p = dom {[x,G1]} & rng p = dom {[y,G2]} ) by A1, FUNCT_4:82;
then ( dom p = {x} & rng p = {y} ) by RELAT_1:9;
then A3: p = x .--> y by FUNCT_4:112;
dom (x .--> G1) = dom {[x,G1]} by FUNCT_4:82
.= {x} by RELAT_1:9 ;
then x in dom (x .--> G1) by TARSKI:def 1;
then consider G3, G4 being _Graph such that
A4: ( G3 = (x .--> G1) . x & G4 = (y .--> G2) . (p . x) & G4 is G3 -Disomorphic ) by A2;
A5: G3 = G1 by A4, FUNCOP_1:72;
G4 = (y .--> G2) . y by A3, A4, FUNCOP_1:72
.= G2 by FUNCOP_1:72 ;
hence G2 is G1 -Disomorphic by A4, A5; :: thesis: verum

end;

assume A6: G2 is G1 -Disomorphic ; :: thesis: x .--> G1,y .--> G2 are_Disomorphic
take p = x .--> y; :: according to GLIB_015:def 14 :: thesis: ( dom p = dom (x .--> G1) & rng p = dom (y .--> G2) & ( for x being object st x in dom (x .--> G1) holds
ex G1, G2 being _Graph st
( G1 = (x .--> G1) . x & G2 = (y .--> G2) . (p . x) & G2 is G1 -Disomorphic ) ) )
thus dom p = dom {[x,y]} by FUNCT_4:82
.= {x} by RELAT_1:9
.= dom {[x,G1]} by RELAT_1:9
.= dom (x .--> G1) by FUNCT_4:82 ; :: thesis: ( rng p = dom (y .--> G2) & ( for x being object st x in dom (x .--> G1) holds
ex G1, G2 being _Graph st
( G1 = (x .--> G1) . x & G2 = (y .--> G2) . (p . x) & G2 is G1 -Disomorphic ) ) )
p = {x} --> y by FUNCOP_1:def 9;
hence rng p = {y} by FUNCOP_1:8
.= dom {[y,G2]} by RELAT_1:9
.= dom (y .--> G2) by FUNCT_4:82 ;
:: thesis: for x being object st x in dom (x .--> G1) holds
ex G1, G2 being _Graph st
( G1 = (x .--> G1) . x & G2 = (y .--> G2) . (p . x) & G2 is G1 -Disomorphic )
let z be object ; :: thesis: ( z in dom (x .--> G1) implies ex G1, G2 being _Graph st
( G1 = (x .--> G1) . z & G2 = (y .--> G2) . (p . z) & G2 is G1 -Disomorphic ) )
assume z in dom (x .--> G1) ; :: thesis: ex G1, G2 being _Graph st
( G1 = (x .--> G1) . z & G2 = (y .--> G2) . (p . z) & G2 is G1 -Disomorphic )
then A7: z = x by TARSKI:def 1;
take G1 ; :: thesis: ex G2 being _Graph st
( G1 = (x .--> G1) . z & G2 = (y .--> G2) . (p . z) & G2 is G1 -Disomorphic )
take G2 ; :: thesis: ( G1 = (x .--> G1) . z & G2 = (y .--> G2) . (p . z) & G2 is G1 -Disomorphic )
thus G1 = (x .--> G1) . z by A7, FUNCOP_1:72; :: thesis: ( G2 = (y .--> G2) . (p . z) & G2 is G1 -Disomorphic )
thus G2 = (y .--> G2) . y by FUNCOP_1:72
.= (y .--> G2) . (p . z) by A7, FUNCOP_1:72 ; :: thesis: G2 is G1 -Disomorphic
thus G2 is G1 -Disomorphic by A6; :: thesis: verum