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 (product J),[:(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 (product J),[:(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 (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

f is being_homeomorphism

let f be Function of (product J),[:(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: f is being_homeomorphism

A2: dom f = the carrier of (product J) by FUNCT_2:def 1

.= [#] (product J) by STRUCT_0:def 3 ;

A3: ( f is onto & f is open ) by A1, Th73;

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

A13: f is continuous by A1, YELLOW12:41;

f " is continuous by A3, A12, TOPREALA:14;

hence f is being_homeomorphism by A2, A4, A12, A13, TOPS_2:def 5; :: thesis: verum

for i, j being Element of I

for f being Function of (product J),[:(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 (product J),[:(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 (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds

f is being_homeomorphism

let f be Function of (product J),[:(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: f is being_homeomorphism

A2: dom f = the carrier of (product J) by FUNCT_2:def 1

.= [#] (product J) by STRUCT_0:def 3 ;

A3: ( f is onto & f is open ) by A1, Th73;

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

then A12:
f is one-to-one
by FUNCT_1:def 4;
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 A1, FUNCT_3:def 7;

( x1 in (dom (proj (J,i))) /\ (dom (proj (J,j))) & x2 in (dom (proj (J,i))) /\ (dom (proj (J,j))) ) by A1, A5, FUNCT_3:def 7;

then ( x1 in dom (proj (J,i)) & x2 in dom (proj (J,j)) ) by XBOOLE_0:def 4;

then a7: ( x1 in dom (proj ((Carrier J),i)) & x2 in dom (proj ((Carrier J),j)) ) by WAYBEL18:def 4;

reconsider g1 = x1, g2 = x2 as Element of (product J) 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 a6, A5, XTUPLE_0:1;

A9: Carrier J = (i,j) --> (((Carrier J) . i),((Carrier J) . j)) by A1, Th9;

then consider a1, b1 being object such that

( a1 in (Carrier J) . i & b1 in (Carrier J) . j ) and

A10: g1 = (i,j) --> (a1,b1) by A1, a7, Th29;

consider a2, b2 being object such that

( a2 in (Carrier J) . i & b2 in (Carrier J) . 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 A1, A10, A11, FUNCT_4:63;

hence x1 = x2 by A8, A10, A11; :: thesis: verum

end;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 A1, FUNCT_3:def 7;

( x1 in (dom (proj (J,i))) /\ (dom (proj (J,j))) & x2 in (dom (proj (J,i))) /\ (dom (proj (J,j))) ) by A1, A5, FUNCT_3:def 7;

then ( x1 in dom (proj (J,i)) & x2 in dom (proj (J,j)) ) by XBOOLE_0:def 4;

then a7: ( x1 in dom (proj ((Carrier J),i)) & x2 in dom (proj ((Carrier J),j)) ) by WAYBEL18:def 4;

reconsider g1 = x1, g2 = x2 as Element of (product J) 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 a6, A5, XTUPLE_0:1;

A9: Carrier J = (i,j) --> (((Carrier J) . i),((Carrier J) . j)) by A1, Th9;

then consider a1, b1 being object such that

( a1 in (Carrier J) . i & b1 in (Carrier J) . j ) and

A10: g1 = (i,j) --> (a1,b1) by A1, a7, Th29;

consider a2, b2 being object such that

( a2 in (Carrier J) . i & b2 in (Carrier J) . 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 A1, A10, A11, FUNCT_4:63;

hence x1 = x2 by A8, A10, A11; :: thesis: verum

A13: f is continuous by A1, YELLOW12:41;

f " is continuous by A3, A12, TOPREALA:14;

hence f is being_homeomorphism by A2, A4, A12, A13, TOPS_2:def 5; :: thesis: verum