let S1, S2, S3 be Graph-membered set ; :: thesis: ( S1,S2 are_Disomorphic & S2,S3 are_Disomorphic implies S1,S3 are_Disomorphic )
assume S1,S2 are_Disomorphic ; :: thesis: ( not S2,S3 are_Disomorphic or S1,S3 are_Disomorphic )
then consider f being one-to-one Function such that
A1: ( dom f = S1 & rng f = S2 ) and
A2: for G being _Graph st G in S1 holds
f . G is b₁ -Disomorphic _Graph ;
assume S2,S3 are_Disomorphic ; :: thesis: S1,S3 are_Disomorphic
then consider g being one-to-one Function such that
A3: ( dom g = S2 & rng g = S3 ) and
A4: for G being _Graph st G in S2 holds
g . G is b₁ -Disomorphic _Graph ;
take g * f ; :: according to GLIB_015:def 12 :: thesis: ( dom (g * f) = S1 & rng (g * f) = S3 & ( for G being _Graph st G in S1 holds
(g * f) . G is b₁ -Disomorphic _Graph ) )
thus dom (g * f) = S1 by A1, A3, RELAT_1:27; :: thesis: ( rng (g * f) = S3 & ( for G being _Graph st G in S1 holds
(g * f) . G is b₁ -Disomorphic _Graph ) )
thus rng (g * f) = S3 by A1, A3, RELAT_1:28; :: thesis: for G being _Graph st G in S1 holds
(g * f) . G is b₁ -Disomorphic _Graph
let G be _Graph; :: thesis: ( G in S1 implies (g * f) . G is G -Disomorphic _Graph )
assume A5: G in S1 ; :: thesis: (g * f) . G is G -Disomorphic _Graph
then reconsider G9 = f . G as G -Disomorphic _Graph by A2;
G9 in rng f by A1, A5, FUNCT_1:def 3;
then g . G9 is G9 -Disomorphic _Graph by A1, A4;
hence (g * f) . G is G -Disomorphic _Graph by A1, A5, FUNCT_1:13; :: thesis: verum