let S1, S2 be Graph-membered set ; :: thesis: ( ex f being one-to-one Function st
( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b₂ -Disomorphic _Graph ) ) implies ex f being one-to-one Function st
( dom f = S2 & rng f = S1 & ( for G being _Graph st G in S2 holds
f . G is b₂ -Disomorphic _Graph ) ) )
given 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 ; :: thesis: ex f being one-to-one Function st
( dom f = S2 & rng f = S1 & ( for G being _Graph st G in S2 holds
f . G is b₂ -Disomorphic _Graph ) )
take f " ; :: thesis: ( dom (f ") = S2 & rng (f ") = S1 & ( for G being _Graph st G in S2 holds
(f ") . G is b₁ -Disomorphic _Graph ) )
thus ( dom (f ") = S2 & rng (f ") = S1 ) by A1, FUNCT_1:33; :: thesis: for G being _Graph st G in S2 holds
(f ") . G is b₁ -Disomorphic _Graph
let G be _Graph; :: thesis: ( G in S2 implies (f ") . G is G -Disomorphic _Graph )
assume G in S2 ; :: thesis: (f ") . G is G -Disomorphic _Graph
then consider G0 being object such that
A3: ( G0 in dom f & f . G0 = G ) by A1, FUNCT_1:def 3;
reconsider G0 = G0 as _Graph by A1, A3;
G is G0 -Disomorphic by A1, A2, A3;
then G0 is G -Disomorphic by GLIB_010:96;
hence (f ") . G is G -Disomorphic _Graph by A3, FUNCT_1:34; :: thesis: verum