let M be non empty set ; :: thesis:
let J be non-Empty TopStruct-yielding ManySortedSet of M; :: thesis:
assume A1: for i being Element of M holds
( J . i is T_1 & J . i is TopSpace-like ) ; :: thesis:
for p being Point of (product J) holds {p} is closed

proof

let p be Point of (product J); :: thesis:
{p} = Cl {p}

proof

thus {p} c= Cl {p} by PRE_TOPC:18; :: according to XBOOLE_0:def 10 :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: a in Cl {p} ; :: thesis:
then reconsider a = a, p = p as Element of (product J) ;
A3: for i being object st i in M holds
a . i = p . i

proof

let i be object ; :: thesis:
assume i in M ; :: thesis:
then reconsider i = i as Element of M ;
( J . i is TopSpace & J . i is T_1 ) by A1;
then A4: {(p . i)} is closed by URYSOHN1:19;
a . i in Cl {(p . i)} by A2, Th29;
then a . i in {(p . i)} by A4, PRE_TOPC:22;
hence a . i = p . i by TARSKI:def 1; :: thesis:

end;

p in the carrier of (product J) ;
then p in product (Carrier J) by WAYBEL18:def 3;
then dom p = dom (Carrier J) by CARD_3:9;
then A5: dom p = M by PARTFUN1:def 2;
a in the carrier of (product J) ;
then a in product (Carrier J) by WAYBEL18:def 3;
then dom a = dom (Carrier J) by CARD_3:9;
then dom a = M by PARTFUN1:def 2;
then a = p by A5, A3, FUNCT_1:2;
hence a in {p} by TARSKI:def 1; :: thesis:

end;

hence {p} is closed ; :: thesis:

end;

hence product J is T_1 by URYSOHN1:19; :: thesis: