A1: ex B being Basis of () st
for P being Subset of () st P in B holds
(proj (J,i)) .: P is open
proof
set B = FinMeetCl ();
set T = product J;
reconsider K = product_prebasis J as Subset-Family of () by WAYBEL18:def 3;
FinMeetCl K is Basis of () by ;
then reconsider B = FinMeetCl () as Basis of () by WAYBEL18:def 3;
take B ; :: thesis: for P being Subset of () st P in B holds
(proj (J,i)) .: P is open

let P be Subset of (); :: 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 ;
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 ; :: thesis: verum