let F1, F2, F3 be Graph-yielding Function; :: thesis: ( F1,F2 are_Disomorphic & F2,F3 are_Disomorphic implies F1,F3 are_Disomorphic )
assume F1,F2 are_Disomorphic ; :: thesis: ( not F2,F3 are_Disomorphic or F1,F3 are_Disomorphic )
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 ) ;
assume F2,F3 are_Disomorphic ; :: thesis: F1,F3 are_Disomorphic
then consider q being one-to-one Function such that
A3: ( dom q = dom F2 & rng q = dom F3 ) and
A4: for x being object st x in dom F2 holds
ex G2, G3 being _Graph st
( G2 = F2 . x & G3 = F3 . (q . x) & G3 is G2 -Disomorphic ) ;
take q * p ; :: according to GLIB_015:def 14 :: thesis: ( dom (q * p) = dom F1 & rng (q * p) = dom F3 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F3 . ((q * p) . x) & G2 is G1 -Disomorphic ) ) )
( dom (q * p) = dom p & rng (q * p) = rng q ) by A1, A3, RELAT_1:27, RELAT_1:28;
hence A5: ( dom (q * p) = dom F1 & rng (q * p) = dom F3 ) by A1, A3; :: thesis: for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F3 . ((q * p) . x) & G2 is G1 -Disomorphic )
let x be object ; :: thesis: ( x in dom F1 implies ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F3 . ((q * p) . x) & G2 is G1 -Disomorphic ) )
assume x in dom F1 ; :: thesis: ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F3 . ((q * p) . x) & G2 is G1 -Disomorphic )
then A6: ( x in dom p & p . x in dom q ) by A5, FUNCT_1:11;
then consider G1, G2 being _Graph such that
A7: ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) by A1, A2;
consider G9, G3 being _Graph such that
A8: ( G9 = F2 . (p . x) & G3 = F3 . (q . (p . x)) & G3 is G9 -Disomorphic ) by A3, A4, A6;
take G1 ; :: thesis: ex G2 being _Graph st
( G1 = F1 . x & G2 = F3 . ((q * p) . x) & G2 is G1 -Disomorphic )
take G3 ; :: thesis: ( G1 = F1 . x & G3 = F3 . ((q * p) . x) & G3 is G1 -Disomorphic )
thus G1 = F1 . x by A7; :: thesis: ( G3 = F3 . ((q * p) . x) & G3 is G1 -Disomorphic )
thus G3 = F3 . ((q * p) . x) by A6, A8, FUNCT_1:13; :: thesis: G3 is G1 -Disomorphic
thus G3 is G1 -Disomorphic by A7, A8; :: thesis: verum