let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
for i being Element of I holds proj J,i is continuous
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: for i being Element of I holds proj J,i is continuous
let i be Element of I; :: thesis: proj J,i is continuous
A1: [#] (J . i) <> {} ;
for P being Subset of (J . i) st P is open holds
(proj J,i) " P is open

proof

let P be Subset of (J . i); :: thesis: ( P is open implies (proj J,i) " P is open )
assume A2: P is open ; :: thesis: (proj J,i) " P is open
(proj J,i) " P c= product (Carrier J)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj J,i) " P or x in product (Carrier J) )
assume x in (proj J,i) " P ; :: thesis: x in product (Carrier J)
then x in dom (proj (Carrier J),i) by FUNCT_1:def 13;
hence x in product (Carrier J) by PRALG_3:def 2; :: thesis: verum

end;

then reconsider x = (proj J,i) " P as Subset of (product (Carrier J)) ;
x = product ((Carrier J) +* i,P) by Th5;
then A3: (proj J,i) " P in product_prebasis J by A2, Def2;
product_prebasis J is prebasis of product J by Def3;
then product_prebasis J c= the topology of (product J) by CANTOR_1:def 5;
hence (proj J,i) " P is open by A3, PRE_TOPC:def 5; :: thesis: verum

end;

hence proj J,i is continuous by A1, TOPS_2:55; :: thesis: verum