let I be 2 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for f being Function of (),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
f is being_homeomorphism

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i, j being Element of I
for f being Function of (),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
f is being_homeomorphism

let i, j be Element of I; :: thesis: for f being Function of (),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
f is being_homeomorphism

let f be Function of (),[:(J . i),(J . j):]; :: thesis: ( i <> j & f = <:(proj (J,i)),(proj (J,j)):> implies f is being_homeomorphism )
assume A1: ( i <> j & f = <:(proj (J,i)),(proj (J,j)):> ) ; :: thesis:
A2: dom f = the carrier of () by FUNCT_2:def 1
.= [#] () by STRUCT_0:def 3 ;
A3: ( f is onto & f is open ) by ;
then rng f = the carrier of [:(J . i),(J . j):] by FUNCT_2:def 3;
then A4: rng f = [#] [:(J . i),(J . j):] by STRUCT_0:def 3;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A5: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then a6: ( f . x1 = [((proj (J,i)) . x1),((proj (J,j)) . x1)] & f . x2 = [((proj (J,i)) . x2),((proj (J,j)) . x2)] ) by ;
( x1 in (dom (proj (J,i))) /\ (dom (proj (J,j))) & x2 in (dom (proj (J,i))) /\ (dom (proj (J,j))) ) by ;
then ( x1 in dom (proj (J,i)) & x2 in dom (proj (J,j)) ) by XBOOLE_0:def 4;
then a7: ( x1 in dom (proj ((),i)) & x2 in dom (proj ((),j)) ) by WAYBEL18:def 4;
reconsider g1 = x1, g2 = x2 as Element of () by A5;
( (proj (J,i)) . x1 = g1 . i & (proj (J,i)) . x2 = g2 . i & (proj (J,j)) . x1 = g1 . j & (proj (J,j)) . x2 = g2 . j ) by YELLOW17:8;
then A8: ( g1 . i = g2 . i & g1 . j = g2 . j ) by ;
A9: Carrier J = (i,j) --> ((() . i),(() . j)) by ;
then consider a1, b1 being object such that
( a1 in () . i & b1 in () . j ) and
A10: g1 = (i,j) --> (a1,b1) by A1, a7, Th29;
consider a2, b2 being object such that
( a2 in () . i & b2 in () . j ) and
A11: g2 = (i,j) --> (a2,b2) by A1, a7, A9, Th29;
( g1 . i = a1 & g2 . i = a2 & g1 . j = b1 & g2 . j = b2 ) by ;
hence x1 = x2 by A8, A10, A11; :: thesis: verum
end;
then A12: f is one-to-one by FUNCT_1:def 4;
A13: f is continuous by ;
f " is continuous by ;
hence f is being_homeomorphism by ; :: thesis: verum