let F1, F2 be Graph-yielding ManySortedSet of I; :: thesis: ( ex p being Permutation of I st
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 ) implies ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (p . x) & G2 is G1 -isomorphic ) )
assume ex p being Permutation of I st
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: ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (p . x) & G2 is G1 -isomorphic )
then consider p being Permutation of I such that
A16: 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 ) ;
reconsider q = p " as Permutation of I ;
take q ; :: thesis: for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (q . x) & G2 is G1 -isomorphic )
let y be object ; :: thesis: ( y in I implies ex G1, G2 being _Graph st
( G1 = F2 . y & G2 = F1 . (q . y) & G2 is G1 -isomorphic ) )
assume y in I ; :: thesis: ex G1, G2 being _Graph st
( G1 = F2 . y & G2 = F1 . (q . y) & G2 is G1 -isomorphic )
then A17: y in dom q by FUNCT_2:def 1;
then q . y in rng q by FUNCT_1:3;
then consider G1, G2 being _Graph such that
A18: ( G1 = F1 . (q . y) & G2 = F2 . (p . (q . y)) & G2 is G1 -isomorphic ) by A16;
take G2 ; :: thesis: ex G2 being _Graph st
( G2 = F2 . y & G2 = F1 . (q . y) & G2 is G2 -isomorphic )
take G1 ; :: thesis: ( G2 = F2 . y & G1 = F1 . (q . y) & G1 is G2 -isomorphic )
y in rng p by A17, FUNCT_1:33;
hence G2 = F2 . y by A18, FUNCT_1:35; :: thesis: ( G1 = F1 . (q . y) & G1 is G2 -isomorphic )
thus ( G1 = F1 . (q . y) & G1 is G2 -isomorphic ) by A18, GLIB_010:95; :: thesis: verum