let F 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 = F . x & G2 = F . (p . x) & G2 is G1 -Disomorphic )
reconsider p = id I as Permutation of I ;
take p ; :: thesis: for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F . x & G2 = F . (p . x) & G2 is G1 -Disomorphic )
let x be object ; :: thesis: ( x in I implies ex G1, G2 being _Graph st
( G1 = F . x & G2 = F . (p . x) & G2 is G1 -Disomorphic ) )
assume A6: x in I ; :: thesis: ex G1, G2 being _Graph st
( G1 = F . x & G2 = F . (p . x) & G2 is G1 -Disomorphic )
then x in dom F by PARTFUN1:def 2;
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take G ; :: thesis: ex G2 being _Graph st
( G = F . x & G2 = F . (p . x) & G2 is G -Disomorphic )
take G ; :: thesis: ( G = F . x & G = F . (p . x) & G is G -Disomorphic )
thus ( G = F . x & G = F . (p . x) & G is G -Disomorphic ) by A6, FUNCT_1:18, GLIB_010:53; :: thesis: verum