let F1, F2 be Graph-yielding Function; :: thesis: ( ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F2 & ( 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 ) ) ) implies ex p being one-to-one Function st
( dom p = dom F2 & rng p = dom F1 & ( for x being object st x in dom F2 holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (p . x) & G2 is G1 -isomorphic ) ) ) )
given p being one-to-one Function such that A7: ( dom p = dom F1 & rng p = dom F2 ) and
A8: 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 ) ; :: thesis: ex p being one-to-one Function st
( dom p = dom F2 & rng p = dom F1 & ( for x being object st x in dom F2 holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (p . x) & G2 is G1 -isomorphic ) ) )
take p " ; :: thesis: ( dom (p ") = dom F2 & rng (p ") = dom F1 & ( for x being object st x in dom F2 holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . ((p ") . x) & G2 is G1 -isomorphic ) ) )
thus ( dom (p ") = dom F2 & rng (p ") = dom F1 ) by A7, FUNCT_1:33; :: thesis: for x being object st x in dom F2 holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . ((p ") . x) & G2 is G1 -isomorphic )
let y be object ; :: thesis: ( y in dom F2 implies ex G1, G2 being _Graph st
( G1 = F2 . y & G2 = F1 . ((p ") . y) & G2 is G1 -isomorphic ) )
assume y in dom F2 ; :: thesis: ex G1, G2 being _Graph st
( G1 = F2 . y & G2 = F1 . ((p ") . y) & G2 is G1 -isomorphic )
then consider x being object such that
A9: ( x in dom p & p . x = y ) by A7, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A10: ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) by A7, A8, A9;
take G2 ; :: thesis: ex G2 being _Graph st
( G2 = F2 . y & G2 = F1 . ((p ") . y) & G2 is G2 -isomorphic )
take G1 ; :: thesis: ( G2 = F2 . y & G1 = F1 . ((p ") . y) & G1 is G2 -isomorphic )
thus G2 = F2 . y by A9, A10; :: thesis: ( G1 = F1 . ((p ") . y) & G1 is G2 -isomorphic )
thus G1 = F1 . ((p ") . y) by A9, A10, FUNCT_1:34; :: thesis: G1 is G2 -isomorphic
thus G1 is G2 -isomorphic by A10, GLIB_010:95; :: thesis: verum