let F1, F2 be non empty Graph-yielding Function; :: thesis: ( dom F1 = dom F2 & ( for x1 being Element of dom F1
for x2 being Element of dom F2 st x1 = x2 holds
F2 . x2 is F1 . x1 -Disomorphic ) implies F1,F2 are_Disomorphic )
assume A1: dom F1 = dom F2 ; :: thesis: ( ex x1 being Element of dom F1 ex x2 being Element of dom F2 st
( x1 = x2 & not F2 . x2 is F1 . x1 -Disomorphic ) or F1,F2 are_Disomorphic )
assume A2: for x1 being Element of dom F1
for x2 being Element of dom F2 st x1 = x2 holds
F2 . x2 is F1 . x1 -Disomorphic ; :: thesis: F1,F2 are_Disomorphic
reconsider p = id (dom F1) as one-to-one Function ;
take p ; :: according to GLIB_015:def 14 :: 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 -Disomorphic ) ) )
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 -Disomorphic )
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 -Disomorphic ) )
assume A3: x in dom F1 ; :: thesis: ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic )
then reconsider G1 = F1 . x as _Graph ;
reconsider G2 = F2 . x as _Graph by A1, A3;
take G1 ; :: thesis: ex G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic )
take G2 ; :: thesis: ( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic )
thus ( G1 = F1 . x & G2 = F2 . (p . x) ) by A3, FUNCT_1:18; :: thesis: G2 is G1 -Disomorphic
thus G2 is G1 -Disomorphic by A1, A2, A3; :: thesis: verum