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

hence proj (J,i) is open by A1, Th45; :: thesis: verum

for P being Subset of (product J) st P in B holds

(proj (J,i)) .: P is open

proof

( product J is TopSpace & J . i is TopSpace )
;
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

end;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 = {} )
;

end;

hence proj (J,i) is open by A1, Th45; :: thesis: verum