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 -Disomorphic ) ) ) 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 -Disomorphic ) ) ) )
given p being one-to-one Function such that A2: ( dom p = dom F1 & rng p = dom F2 ) and
A3: 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 ) ; :: 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 -Disomorphic ) ) )
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 -Disomorphic ) ) )
thus ( dom (p ") = dom F2 & rng (p ") = dom F1 ) by A2, 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 -Disomorphic )
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 -Disomorphic ) )
assume y in dom F2 ; :: thesis: ex G1, G2 being _Graph st
( G1 = F2 . y & G2 = F1 . ((p ") . y) & G2 is G1 -Disomorphic )
then consider x being object such that
A4: ( x in dom p & p . x = y ) by A2, FUNCT_1:def 3;
consider G1, G2 being _Graph such that
A5: ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) by A2, A3, A4;
take G2 ; :: thesis: ex G2 being _Graph st
( G2 = F2 . y & G2 = F1 . ((p ") . y) & G2 is G2 -Disomorphic )
take G1 ; :: thesis: ( G2 = F2 . y & G1 = F1 . ((p ") . y) & G1 is G2 -Disomorphic )
thus G2 = F2 . y by A4, A5; :: thesis: ( G1 = F1 . ((p ") . y) & G1 is G2 -Disomorphic )
thus G1 = F1 . ((p ") . y) by A4, A5, FUNCT_1:34; :: thesis: G1 is G2 -Disomorphic
thus G1 is G2 -Disomorphic by A5, GLIB_010:96; :: thesis: verum