A1: ex B being Basis of (product J) st
for P being Subset of (product J) st P in B holds
(proj (J,i)) .: P is open
proof
set B = FinMeetCl (product_prebasis J);
set T = product J;
reconsider K = product_prebasis J as Subset-Family of (product J) by WAYBEL18:def 3;
FinMeetCl K is Basis of (product J) by WAYBEL18:def 3, YELLOW_9:23;
then reconsider B = FinMeetCl (product_prebasis J) as Basis of (product J) by WAYBEL18:def 3;
take B ; :: thesis: for P being Subset of (product J) st P in B holds
(proj (J,i)) .: P is open
let P be Subset of (product J); :: thesis: ( P in B implies (proj (J,i)) .: P is open )
assume A2: P in B ; :: thesis: (proj (J,i)) .: P is open
per cases ( P <> {} or P = {} ) ;
suppose P <> {} ; :: thesis: (proj (J,i)) .: P is open
then ex I0 being finite Subset of I st
for j being Element of I holds
( (proj (J,j)) .: P is open & ( not j in I0 implies (proj (J,j)) .: P = [#] (J . j) ) ) by A2, Th63;
hence (proj (J,i)) .: P is open ; :: thesis: verum
end;
suppose P = {} ; :: thesis: (proj (J,i)) .: P is open
then ( (proj (J,i)) .: P is empty & (proj (J,i)) .: P is Subset of (J . i) ) ;
hence (proj (J,i)) .: P is open ; :: thesis: verum
end;
end;
end;
( product J is TopSpace & J . i is TopSpace ) ;
hence proj (J,i) is open by A1, Th45; :: thesis: verum