let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for A being set st A in product_prebasis J holds
ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for A being set st A in product_prebasis J holds
ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )

let A be set ; :: thesis: ( A in product_prebasis J implies ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A ) )

assume A in product_prebasis J ; :: thesis: ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )

then consider i being set , T being TopStruct , Ai being Subset of T such that
A1: i in I and
A2: Ai is open and
A3: T = J . i and
A4: A = product (() +* (i,Ai)) by WAYBEL18:def 2;
reconsider i = i as Element of I by A1;
reconsider Ai = Ai as Subset of (J . i) by A3;
take i ; :: thesis: ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )

take Ai ; :: thesis: ( Ai is open & (proj (J,i)) " Ai = A )
thus Ai is open by A2, A3; :: thesis: (proj (J,i)) " Ai = A
thus (proj (J,i)) " Ai = A by ; :: thesis: verum