let X be non empty TopSpace; :: thesis: for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of
for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj J,i) * f is continuous )
let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj J,i) * f is continuous )
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: for f being Function of X,(product J) holds
( f is continuous iff for i being Element of I holds (proj J,i) * f is continuous )
let f be Function of X,(product J); :: thesis: ( f is continuous iff for i being Element of I holds (proj J,i) * f is continuous )
assume A2:
for i being Element of I holds (proj J,i) * f is continuous
; :: thesis: f is continuous
set B = product_prebasis J;
A3:
product_prebasis J is prebasis of product J
by Def3;
for P being Subset of (product J) st P in product_prebasis J holds
f " P is open
proof
let P be
Subset of
(product J);
:: thesis: ( P in product_prebasis J implies f " P is open )
assume A4:
P in product_prebasis J
;
:: thesis: f " P is open
reconsider p =
P as
Subset of
(product (Carrier J)) by Def3;
consider i being
set ,
T being
TopStruct ,
V being
Subset of
T such that A5:
i in I
and A6:
V is
open
and A7:
T = J . i
and A8:
p = product ((Carrier J) +* i,V)
by A4, Def2;
reconsider j =
i as
Element of
I by A5;
A9:
(proj J,j) * f is
continuous
by A2;
reconsider V =
V as
Subset of
(J . j) by A7;
A10:
(proj J,j) " V = p
by A8, Th5;
[#] (J . j) <> {}
;
then
((proj J,j) * f) " V is
open
by A6, A7, A9, TOPS_2:55;
hence
f " P is
open
by A10, RELAT_1:181;
:: thesis: verum
end;
hence
f is continuous
by A3, YELLOW_9:36; :: thesis: verum