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)) )

proof

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;

hence {} in product_prebasis J by WAYBEL18:def 2; :: thesis: verum