let M be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of 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 TopSpace-yielding ManySortedSet of ; :: 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
( x in the carrier of (product J) & y in the carrier of (product J) ) ;
then ( x in product (Carrier J) & y in product (Carrier J) ) by WAYBEL18:def 3;
then ( dom x = dom (Carrier J) & dom y = dom (Carrier J) ) by CARD_3:18;
then ( dom x = M & dom y = M ) by PARTFUN1:def 4;
then consider i being set such that
A4: i in M and
A5: x . i <> y . i by A2, FUNCT_1:9;
reconsider i = i as Element of M by A4;
A6: J . i is T_0 TopSpace by A1;
( pi (Cl {x}),i = Cl {(x . i)} & pi (Cl {y}),i = Cl {(y . i)} ) by Th32;
hence contradiction by A3, A5, A6, TSP_1:def 5; :: thesis: verum

end;

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