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

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 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;

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