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_0 TopSpace ) holds
product J is T_0
let J be non-Empty TopStruct-yielding ManySortedSet of M; :: thesis: ( ( for i being Element of M holds J . i is T_0 TopSpace ) implies product J is T_0 )
assume A1: for i being Element of M holds J . i is T_0 TopSpace ; :: thesis: product J is T_0
for x, y being Point of (product J) st x <> y holds
Cl {x} <> Cl {y}

proof

let x, y be Point of (product J); :: thesis: ( x <> y implies Cl {x} <> Cl {y} )
assume that
A2: x <> y and
A3: Cl {x} = Cl {y} ; :: thesis: contradiction
y in the carrier of (product J) ;
then y in product (Carrier J) by WAYBEL18:def 3;
then dom y = dom (Carrier J) by CARD_3:9;
then A4: dom y = M by PARTFUN1:def 2;
x in the carrier of (product J) ;
then x in product (Carrier J) by WAYBEL18:def 3;
then dom x = dom (Carrier J) by CARD_3:9;
then dom x = M by PARTFUN1:def 2;
then consider i being object such that
A5: i in M and
A6: x . i <> y . i by A2, A4, FUNCT_1:2;
reconsider i = i as Element of M by A5;
A7: pi ((Cl {y}),i) = Cl {(y . i)} by Th31;
( J . i is T_0 TopSpace & pi ((Cl {x}),i) = Cl {(x . i)} ) by A1, Th31;
hence contradiction by A3, A6, A7, TSP_1:def 5; :: thesis: verum

end;

hence product J is T_0 by TSP_1:def 5; :: thesis: verum