hereby :: thesis:

assume F1,F2 are_isomorphic ; :: thesis:
then consider p being one-to-one Function such that
A10: ( dom p = dom F1 & rng p = dom F2 ) and
A11: 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 ) ;
A12: ( dom p = I & rng p = I ) by A10, PARTFUN1:def 2;
then reconsider p = p as one-to-one Function of I,I by FUNCT_2:1;
p is onto by A12, 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
A13: ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) by A11;
take G1 = G1; :: thesis:
take G2 = G2; :: thesis:
thus ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) by A13; :: thesis:

end;

given p being Permutation of I such that A14: 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 -isomorphic ) ; :: thesis:
reconsider p = p as one-to-one Function ;
take p ; :: according to GLIB_015:def 15 :: 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 -isomorphic ) by A14; :: thesis: