let I be 1 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) is being_homeomorphism
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I holds proj (J,i) is being_homeomorphism
let i be Element of I; :: thesis: proj (J,i) is being_homeomorphism
card I = 1 by CARD_1:def 7;
then A1: I = {i} by ORDERS_5:2;
set f = proj (J,i);
A2: dom (proj (J,i)) = the carrier of (product J) by FUNCT_2:def 1
.= [#] (product J) by STRUCT_0:def 3 ;
the carrier of (J . i) = [#] (J . i) by STRUCT_0:def 3
.= (Carrier J) . i by PENCIL_3:7 ;
then A3: Carrier J = {i} --> the carrier of (J . i) by A1, Th7;
A4: rng (proj (J,i)) = the carrier of (J . i) by FUNCT_2:def 3
.= [#] (J . i) by STRUCT_0:def 3 ;
a5: proj (J,i) = proj ((Carrier J),i) by WAYBEL18:def 4
.= proj ((i .--> the carrier of (J . i)),i) by A3, FUNCOP_1:def 9 ;
(proj (J,i)) " is continuous by a5, TOPREALA:14;
hence proj (J,i) is being_homeomorphism by A2, A4, a5, TOPS_2:def 5; :: thesis: verum