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

proof

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

proof

thus {p} c= Cl {p} by PRE_TOPC:18; :: according to XBOOLE_0:def 10 :: thesis: Cl {p} c= {p}
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Cl {p} or a in {p} )
assume A2: a in Cl {p} ; :: thesis: a in {p}
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: ( i in M implies a . i = p . i )
assume i in M ; :: thesis: a . i = p . i
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: verum

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: verum

end;

hence {p} is closed ; :: thesis: verum

end;

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