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 ((Carrier J) +* (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 A4, WAYBEL18:4; :: thesis: verum