let F1, F2 be Graph-yielding Function; :: thesis: ( F1,F2 are_Disomorphic implies F1,F2 are_isomorphic )
assume F1,F2 are_Disomorphic ; :: thesis: F1,F2 are_isomorphic
then consider p being one-to-one Function such that
A1: ( dom p = dom F1 & rng p = dom F2 ) and
A2: 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 ) ;
take p ; :: according to GLIB_015:def 15 :: thesis: ( 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 ) ) )
thus ( dom p = dom F1 & rng p = dom F2 ) by A1; :: thesis: 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 )
let x be object ; :: thesis: ( x in dom F1 implies ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) )
assume x in dom F1 ; :: thesis: ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic )
then consider G1, G2 being _Graph such that
A3: ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) by A2;
take G1 ; :: thesis: ex G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic )
take G2 ; :: thesis: ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic )
thus ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) by A3; :: thesis: verum