let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I holds {} in product_prebasis J

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: {} in product_prebasis J

set P = the empty Subset of (product (Carrier J));

ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* (i,V)) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: {} in product_prebasis J

set P = the empty Subset of (product (Carrier J));

ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* (i,V)) )

proof

hence
{} in product_prebasis J
by WAYBEL18:def 2; :: thesis: verum
set i = the Element of I;

set V = the empty Subset of (J . the Element of I);

take the Element of I ; :: thesis: ex T being TopStruct ex V being Subset of T st

( the Element of I in I & V is open & T = J . the Element of I & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* ( the Element of I,V)) )

take J . the Element of I ; :: thesis: ex V being Subset of (J . the Element of I) st

( the Element of I in I & V is open & J . the Element of I = J . the Element of I & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* ( the Element of I,V)) )

take the empty Subset of (J . the Element of I) ; :: thesis: ( the Element of I in I & the empty Subset of (J . the Element of I) is open & J . the Element of I = J . the Element of I & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) )

dom (Carrier J) = I by PARTFUN1:def 2;

hence ( the Element of I in I & the empty Subset of (J . the Element of I) is open & J . the Element of I = J . the Element of I & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) ) by Th36; :: thesis: verum

end;set V = the empty Subset of (J . the Element of I);

take the Element of I ; :: thesis: ex T being TopStruct ex V being Subset of T st

( the Element of I in I & V is open & T = J . the Element of I & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* ( the Element of I,V)) )

take J . the Element of I ; :: thesis: ex V being Subset of (J . the Element of I) st

( the Element of I in I & V is open & J . the Element of I = J . the Element of I & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* ( the Element of I,V)) )

take the empty Subset of (J . the Element of I) ; :: thesis: ( the Element of I in I & the empty Subset of (J . the Element of I) is open & J . the Element of I = J . the Element of I & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) )

dom (Carrier J) = I by PARTFUN1:def 2;

hence ( the Element of I in I & the empty Subset of (J . the Element of I) is open & J . the Element of I = J . the Element of I & the empty Subset of (product (Carrier J)) = product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) ) by Th36; :: thesis: verum