let I be 1 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I holds the topology of (product J) = product_prebasis J
let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: the topology of (product J) = product_prebasis J
reconsider T = product J as TopSpace ;
reconsider K = product_prebasis J as Subset-Family of T by WAYBEL18:def 3;
K is prebasis of T by WAYBEL18:def 3;
then A1: UniCl (FinMeetCl K) = the topology of T by YELLOW_9:22, YELLOW_9:23;
FinMeetCl K = FinMeetCl (product_prebasis J) by WAYBEL18:def 3;
then UniCl (FinMeetCl K) = UniCl (FinMeetCl (product_prebasis J)) by WAYBEL18:def 3;
hence the topology of (product J) = product_prebasis J by A1, Lm7; :: thesis: verum