let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of st ( for i being Element of I holds J . i is injective ) holds
product J is injective
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of I holds J . i is injective ) implies product J is injective )
assume A1:
for i being Element of I holds J . i is injective
; :: thesis: product J is injective
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis: for f being Function of X,(product J) st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f )
let f be Function of X,(product J); :: thesis: ( f is continuous implies for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f ) )
assume A2:
f is continuous
; :: thesis: for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f )
let Y be non empty TopSpace; :: thesis: ( X is SubSpace of Y implies ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f ) )
assume A3:
X is SubSpace of Y
; :: thesis: ex g being Function of Y,(product J) st
( g is continuous & g | the carrier of X = f )
defpred S1[ set , set ] means ex i1 being Element of I st
( i1 = $1 & ex g being Function of Y,(J . i1) st
( g is continuous & g | the carrier of X = (proj J,i1) * f & $2 = g ) );
A4:
for i being set st i in I holds
ex u being set st S1[i,u]
proof
let i be
set ;
:: thesis: ( i in I implies ex u being set st S1[i,u] )
assume
i in I
;
:: thesis: ex u being set st S1[i,u]
then reconsider i1 =
i as
Element of
I ;
A5:
J . i1 is
injective
by A1;
(proj J,i1) * f is
continuous
by A2, Th7;
then consider g being
Function of
Y,
(J . i1) such that A6:
g is
continuous
and A7:
g | the
carrier of
X = (proj J,i1) * f
by A3, A5, Def5;
take
g
;
:: thesis: S1[i,g]
take
i1
;
:: thesis: ( i1 = i & ex g being Function of Y,(J . i1) st
( g is continuous & g | the carrier of X = (proj J,i1) * f & g = g ) )
thus
(
i1 = i & ex
g being
Function of
Y,
(J . i1) st
(
g is
continuous &
g | the
carrier of
X = (proj J,i1) * f &
g = g ) )
by A6, A7;
:: thesis: verum
end;
consider G being Function such that
A8:
dom G = I
and
A9:
for i being set st i in I holds
S1[i,G . i]
from CLASSES1:sch 1(A4);
A10:
dom <:G:> c= the carrier of Y
the carrier of Y c= dom <:G:>
then A24:
dom <:G:> = the carrier of Y
by A10, XBOOLE_0:def 10;
A25:
G is Function-yielding
A28:
product (rngs G) c= product (Carrier J)
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in product (rngs G) or y in product (Carrier J) )
assume
y in product (rngs G)
;
:: thesis: y in product (Carrier J)
then consider h being
Function such that A29:
y = h
and A30:
dom h = dom (rngs G)
and A31:
for
x being
set st
x in dom (rngs G) holds
h . x in (rngs G) . x
by CARD_3:def 5;
A32:
dom h =
I
by A8, A25, A30, FUNCT_6:90
.=
dom (Carrier J)
by PARTFUN1:def 4
;
for
x being
set st
x in dom (Carrier J) holds
h . x in (Carrier J) . x
proof
let x be
set ;
:: thesis: ( x in dom (Carrier J) implies h . x in (Carrier J) . x )
assume A33:
x in dom (Carrier J)
;
:: thesis: h . x in (Carrier J) . x
then A34:
h . x in (rngs G) . x
by A30, A31, A32;
A35:
x in I
by A33, PARTFUN1:def 4;
then consider i being
Element of
I such that A36:
i = x
and A37:
ex
g being
Function of
Y,
(J . i) st
(
g is
continuous &
g | the
carrier of
X = (proj J,i) * f &
G . x = g )
by A9;
consider g being
Function of
Y,
(J . i) such that
(
g is
continuous &
g | the
carrier of
X = (proj J,i) * f )
and A38:
G . x = g
by A37;
x in dom G
by A8, A33, PARTFUN1:def 4;
then A39:
(rngs G) . x = rng g
by A38, FUNCT_6:31;
consider R being
1-sorted such that A40:
R = J . x
and A41:
(Carrier J) . x = the
carrier of
R
by A35, PRALG_1:def 13;
thus
h . x in (Carrier J) . x
by A34, A36, A39, A40, A41;
:: thesis: verum
end;
hence
y in product (Carrier J)
by A29, A32, CARD_3:def 5;
:: thesis: verum
end;
rng <:G:> c= product (rngs G)
by FUNCT_6:49;
then A42:
rng <:G:> c= product (Carrier J)
by A28, XBOOLE_1:1;
then
rng <:G:> c= the carrier of (product J)
by Def3;
then reconsider h = <:G:> as Function of the carrier of Y,the carrier of (product J) by A24, FUNCT_2:def 1, RELSET_1:11;
A43: dom (h | the carrier of X) =
(dom h) /\ the carrier of X
by RELAT_1:90
.=
the carrier of Y /\ the carrier of X
by FUNCT_2:def 1
.=
the carrier of X
by A3, BORSUK_1:35, XBOOLE_1:28
.=
dom f
by FUNCT_2:def 1
;
A44:
for x being set st x in dom (h | the carrier of X) holds
(h | the carrier of X) . x = f . x
proof
let x be
set ;
:: thesis: ( x in dom (h | the carrier of X) implies (h | the carrier of X) . x = f . x )
assume A45:
x in dom (h | the carrier of X)
;
:: thesis: (h | the carrier of X) . x = f . x
then A46:
x in the
carrier of
Y
;
f . x in rng f
by A43, A45, FUNCT_1:def 5;
then
f . x in the
carrier of
(product J)
;
then A47:
f . x in product (Carrier J)
by Def3;
then consider y being
Function such that A48:
f . x = y
and A49:
dom y = dom (Carrier J)
and
for
i being
set st
i in dom (Carrier J) holds
y . i in (Carrier J) . i
by CARD_3:def 5;
(h | the carrier of X) . x in rng (h | the carrier of X)
by A45, FUNCT_1:def 5;
then
(h | the carrier of X) . x in the
carrier of
(product J)
;
then
(h | the carrier of X) . x in product (Carrier J)
by Def3;
then consider z being
Function such that A50:
(h | the carrier of X) . x = z
and A51:
dom z = dom (Carrier J)
and
for
i being
set st
i in dom (Carrier J) holds
z . i in (Carrier J) . i
by CARD_3:def 5;
for
j being
set st
j in dom y holds
y . j = z . j
proof
let j be
set ;
:: thesis: ( j in dom y implies y . j = z . j )
assume
j in dom y
;
:: thesis: y . j = z . j
then A52:
j in I
by A49, PARTFUN1:def 4;
then consider i being
Element of
I such that A53:
i = j
and A54:
ex
g being
Function of
Y,
(J . i) st
(
g is
continuous &
g | the
carrier of
X = (proj J,i) * f &
G . j = g )
by A9;
consider g being
Function of
Y,
(J . i) such that
g is
continuous
and A55:
g | the
carrier of
X = (proj J,i) * f
and A56:
G . j = g
by A54;
A57:
x in dom h
by A46, FUNCT_2:def 1;
A58:
y in dom (proj (Carrier J),i)
by A47, A48, PRALG_3:def 2;
z = <:G:> . x
by A43, A45, A50, FUNCT_1:72;
hence z . j =
g . x
by A8, A52, A56, A57, FUNCT_6:54
.=
((proj J,i) * f) . x
by A43, A45, A55, FUNCT_1:72
.=
(proj (Carrier J),i) . y
by A43, A45, A48, FUNCT_2:21
.=
y . j
by A53, A58, PRALG_3:def 2
;
:: thesis: verum
end;
hence
(h | the carrier of X) . x = f . x
by A48, A49, A50, A51, FUNCT_1:9;
:: thesis: verum
end;
reconsider h = h as Function of Y,(product J) ;
take
h
; :: thesis: ( h is continuous & h | the carrier of X = f )
set B = product_prebasis J;
A59:
product_prebasis J is prebasis of product J
by Def3;
for P being Subset of (product J) st P in product_prebasis J holds
h " P is open
proof
let P be
Subset of
(product J);
:: thesis: ( P in product_prebasis J implies h " P is open )
assume A60:
P in product_prebasis J
;
:: thesis: h " 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 A61:
i in I
and A62:
V is
open
and A63:
T = J . i
and A64:
p = product ((Carrier J) +* i,V)
by A60, Def2;
consider j being
Element of
I such that A65:
j = i
and A66:
ex
g being
Function of
Y,
(J . j) st
(
g is
continuous &
g | the
carrier of
X = (proj J,j) * f &
G . i = g )
by A9, A61;
consider g being
Function of
Y,
(J . j) such that A67:
g is
continuous
and
g | the
carrier of
X = (proj J,j) * f
and A68:
G . i = g
by A66;
reconsider V =
V as
Subset of
(J . j) by A63, A65;
A69:
(proj J,j) " V = p
by A64, A65, Th5;
[#] (J . j) <> {}
;
then A70:
g " V is
open
by A62, A63, A65, A67, TOPS_2:55;
A71:
dom g =
the
carrier of
Y
by FUNCT_2:def 1
.=
dom h
by FUNCT_2:def 1
;
A72:
dom (proj J,j) = product (Carrier J)
by PRALG_3:def 2;
A73:
h " P c= g " V
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in h " P or x in g " V )
assume A74:
x in h " P
;
:: thesis: x in g " V
then A75:
(
x in dom h &
h . x in P )
by FUNCT_1:def 13;
A76:
x in dom g
by A71, A74, FUNCT_1:def 13;
A77:
h . x in (proj J,j) " V
by A69, A74, FUNCT_1:def 13;
then A78:
h . x in dom (proj J,j)
by FUNCT_1:def 13;
h . x in product (Carrier J)
by A72, A77, FUNCT_1:def 13;
then consider y being
Function such that A79:
h . x = y
and
dom y = dom (Carrier J)
and
for
i being
set st
i in dom (Carrier J) holds
y . i in (Carrier J) . i
by CARD_3:def 5;
(proj J,j) . (h . x) = y . j
by A78, A79, PRALG_3:def 2;
then A80:
y . j in V
by A77, FUNCT_1:def 13;
g . x = y . j
by A8, A65, A68, A75, A79, FUNCT_6:54;
hence
x in g " V
by A76, A80, FUNCT_1:def 13;
:: thesis: verum
end;
g " V c= h " P
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in g " V or x in h " P )
assume A81:
x in g " V
;
:: thesis: x in h " P
then A82:
x in dom h
by A71, FUNCT_1:def 13;
then A83:
h . x in rng h
by FUNCT_1:def 5;
then A84:
h . x in product (Carrier J)
by A42;
consider y being
Function such that A85:
h . x = y
and
dom y = dom (Carrier J)
and
for
i being
set st
i in dom (Carrier J) holds
y . i in (Carrier J) . i
by A42, A83, CARD_3:def 5;
y in dom (proj (Carrier J),j)
by A84, A85, PRALG_3:def 2;
then A86:
(proj J,j) . (h . x) = y . j
by A85, PRALG_3:def 2;
g . x = y . j
by A8, A65, A68, A82, A85, FUNCT_6:54;
then
(proj J,j) . (h . x) in V
by A81, A86, FUNCT_1:def 13;
then
h . x in (proj J,j) " V
by A42, A72, A83, FUNCT_1:def 13;
hence
x in h " P
by A69, A82, FUNCT_1:def 13;
:: thesis: verum
end;
hence
h " P is
open
by A70, A73, XBOOLE_0:def 10;
:: thesis: verum
end;
hence
h is continuous
by A59, YELLOW_9:36; :: thesis: h | the carrier of X = f
thus
h | the carrier of X = f
by A43, A44, FUNCT_1:9; :: thesis: verum