let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I

for P being non empty Subset of (product (Carrier J)) st P in product_prebasis J holds

( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for P being non empty Subset of (product (Carrier J)) st P in product_prebasis J holds

( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) )

let P be non empty Subset of (product (Carrier J)); :: thesis: ( P in product_prebasis J implies ( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) ) )

assume P in product_prebasis J ; :: thesis: ( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) )

then consider i being Element of I such that

A1: (proj (J,i)) .: P is open and

A2: for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) by Th57;

(proj (J,j)) .: P = [#] (J . j)

thus for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) by A2; :: thesis: verum

for P being non empty Subset of (product (Carrier J)) st P in product_prebasis J holds

( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for P being non empty Subset of (product (Carrier J)) st P in product_prebasis J holds

( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) )

let P be non empty Subset of (product (Carrier J)); :: thesis: ( P in product_prebasis J implies ( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) ) )

assume P in product_prebasis J ; :: thesis: ( ( for j being Element of I holds (proj (J,j)) .: P is open ) & ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) )

then consider i being Element of I such that

A1: (proj (J,i)) .: P is open and

A2: for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) by Th57;

hereby :: thesis: ex i being Element of I st

for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j)

take
i
; :: thesis: for j being Element of I st j <> i holds for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j)

let j be Element of I; :: thesis: (proj (J,j)) .: P is open

( j <> i implies (proj (J,j)) .: P = [#] (J . j) ) by A2;

hence (proj (J,j)) .: P is open by A1; :: thesis: verum

end;( j <> i implies (proj (J,j)) .: P = [#] (J . j) ) by A2;

hence (proj (J,j)) .: P is open by A1; :: thesis: verum

(proj (J,j)) .: P = [#] (J . j)

thus for j being Element of I st j <> i holds

(proj (J,j)) .: P = [#] (J . j) by A2; :: thesis: verum