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₂ -isomorphic _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₂ -isomorphic _Graph ) ) )
given f being one-to-one Function such that A4: ( dom f = S1 & rng f = S2 ) and
A5: for G being _Graph st G in S1 holds
f . G is b₁ -isomorphic _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₂ -isomorphic _Graph ) )
take f " ; :: thesis: ( dom (f ") = S2 & rng (f ") = S1 & ( for G being _Graph st G in S2 holds
(f ") . G is b₁ -isomorphic _Graph ) )
thus ( dom (f ") = S2 & rng (f ") = S1 ) by A4, FUNCT_1:33; :: thesis: for G being _Graph st G in S2 holds
(f ") . G is b₁ -isomorphic _Graph
let G be _Graph; :: thesis: ( G in S2 implies (f ") . G is G -isomorphic _Graph )
assume G in S2 ; :: thesis: (f ") . G is G -isomorphic _Graph
then consider G0 being object such that
A6: ( G0 in dom f & f . G0 = G ) by A4, FUNCT_1:def 3;
reconsider G0 = G0 as _Graph by A4, A6;
G is G0 -isomorphic by A4, A5, A6;
then G0 is G -isomorphic by GLIB_010:95;
hence (f ") . G is G -isomorphic _Graph by A6, FUNCT_1:34; :: thesis: verum