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