let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) is continuous
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: 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: 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 object ; :: 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 7;
hence x in product (Carrier J) ; :: thesis: verum

end;

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

end;

[#] (J . i) <> {} ;
hence proj (J,i) is continuous by A1, TOPS_2:43; :: thesis: verum