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

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