hereby :: thesis:

assume F1,F2 are_Disomorphic ; :: thesis:
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 ) ;
A3: ( dom p = I & rng p = I ) by A1, PARTFUN1:def 2;
then reconsider p = p as one-to-one Function of I,I by FUNCT_2:1;
p is onto by A3, FUNCT_2:def 3;
then reconsider p = p as Permutation of I ;
take p = p; :: thesis:
let x be object ; :: thesis:
assume x in I ; :: thesis:
then x in dom F1 by PARTFUN1:def 2;
then consider G1, G2 being _Graph such that
A4: ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) by A2;
take G1 = G1; :: thesis:
take G2 = G2; :: thesis:
thus ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) by A4; :: thesis:

end;

given p being Permutation of I such that A5: for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) ; :: thesis:
reconsider p = p as one-to-one Function ;
take p ; :: according to GLIB_015:def 14 :: thesis:
thus dom p = I by PARTFUN1:def 2
.= dom F1 by PARTFUN1:def 2 ; :: thesis:
thus rng p = I by FUNCT_2:def 3
.= dom F2 by PARTFUN1:def 2 ; :: thesis:
let x be object ; :: thesis:
assume x in dom F1 ; :: thesis:
hence ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) by A5; :: thesis: