let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is injective ) holds
product J is injective
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: 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
set B = product_prebasis J;
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 ) )
defpred S1[ object , object ] 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 ) );
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 )
A4: for i being object st i in I holds
ex u being object st S1[i,u]
proof
let i be object ; :: thesis: ( i in I implies ex u being object st S1[i,u] )
assume i in I ; :: thesis: ex u being object st S1[i,u]
then reconsider i1 = i as Element of I ;
( J . i1 is injective & (proj (J,i1)) * f is continuous ) by A1, A2, Th6;
then consider g being Function of Y,(J . i1) such that
A5: ( g is continuous & g | the carrier of X = (proj (J,i1)) * f ) by A3;
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 A5; :: thesis: verum
end;
consider G being Function such that
A6: dom G = I and
A7: for i being object st i in I holds
S1[i,G . i] from CLASSES1:sch 1(A4);
 G is Function-yielding
proof
let j be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not j in dom G or G . j is set )
assume j in dom G ; :: thesis: G . j is set
then ex i being Element of I st
( i = j & 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 A6, A7;
hence G . j is set ; :: thesis: verum
end;
then reconsider G = G as Function-yielding Function ;
A8: the carrier of Y c= dom <:G:>
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of Y or x in dom <:G:> )
consider i being object such that
A9: i in I by XBOOLE_0:def 1;
assume A10: x in the carrier of Y ; :: thesis: x in dom <:G:>
A11: for f9 being Function st f9 in rng G holds
x in dom f9
proof
let f9 be Function; :: thesis: ( f9 in rng G implies x in dom f9 )
assume f9 in rng G ; :: thesis: x in dom f9
then consider k being object such that
A12: k in dom G and
A13: f9 = G . k by FUNCT_1:def 3;
ex i1 being Element of I st
( i1 = k & ex ff being Function of Y,(J . i1) st
( ff is continuous & ff | the carrier of X = (proj (J,i1)) * f & G . k = ff ) ) by A6, A7, A12;
hence x in dom f9 by A10, A13, FUNCT_2:def 1; :: thesis: verum
end;
consider j being Element of I such that
j = i and
A14: 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 A7, A9;
consider g being Function of Y,(J . j) such that
g is continuous and
g | the carrier of X = (proj (J,j)) * f and
A15: G . i = g by A14;
g in rng G by A6, A9, A15, FUNCT_1:def 3;
hence x in dom <:G:> by A11, FUNCT_6:33; :: thesis: verum
end;
A16: product (rngs G) c= product (Carrier J)
proof
let y be object ; :: 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
A17: y = h and
A18: dom h = dom (rngs G) and
A19: for x being object st x in dom (rngs G) holds
h . x in (rngs G) . x by CARD_3:def 5;
A20: dom h = I by A6, A18, FUNCT_6:60
.= dom (Carrier J) by PARTFUN1:def 2 ;
for x being object st x in dom (Carrier J) holds
h . x in (Carrier J) . x
proof
let x be object ; :: thesis: ( x in dom (Carrier J) implies h . x in (Carrier J) . x )
assume A21: x in dom (Carrier J) ; :: thesis: h . x in (Carrier J) . x
then A22: x in I ;
then consider i being Element of I such that
A23: i = x and
A24: 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 A7;
A25: ex R being 1-sorted st
( R = J . x & (Carrier J) . x = the carrier of R ) by A22, PRALG_1:def 15;
consider g being Function of Y,(J . i) such that
g is continuous and
g | the carrier of X = (proj (J,i)) * f and
A26: G . x = g by A24;
x in dom G by A6, A21;
then A27: (rngs G) . x = rng g by A26, FUNCT_6:22;
h . x in (rngs G) . x by A18, A19, A20, A21;
hence h . x in (Carrier J) . x by A23, A27, A25; :: thesis: verum
end;
hence y in product (Carrier J) by A17, A20, CARD_3:def 5; :: thesis: verum
end;
dom <:G:> c= the carrier of Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom <:G:> or x in the carrier of Y )
assume A28: x in dom <:G:> ; :: thesis: x in the carrier of Y
consider j being object such that
A29: j in I by XBOOLE_0:def 1;
consider i being Element of I such that
i = j and
A30: 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 A7, A29;
consider g being Function of Y,(J . i) such that
g is continuous and
g | the carrier of X = (proj (J,i)) * f and
A31: G . j = g by A30;
g in rng G by A6, A29, A31, FUNCT_1:def 3;
then x in dom g by A28, FUNCT_6:32;
hence x in the carrier of Y ; :: thesis: verum
end;
then A32: dom <:G:> = the carrier of Y by A8;
rng <:G:> c= product (rngs G) by FUNCT_6:29;
then A33: rng <:G:> c= product (Carrier J) by A16;
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 A32, FUNCT_2:def 1, RELSET_1:4;
A34: dom (h | the carrier of X) = (dom h) /\ the carrier of X by RELAT_1:61
.= the carrier of Y /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X by A3, BORSUK_1:1, XBOOLE_1:28
.= dom f by FUNCT_2:def 1 ;
A35: for x being object st x in dom (h | the carrier of X) holds
(h | the carrier of X) . x = f . x
proof
let x be object ; :: thesis: ( x in dom (h | the carrier of X) implies (h | the carrier of X) . x = f . x )
assume A36: x in dom (h | the carrier of X) ; :: thesis: (h | the carrier of X) . x = f . x
then A37: x in dom h by RELAT_1:57;
(h | the carrier of X) . x in rng (h | the carrier of X) by A36, FUNCT_1:def 3;
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
A38: (h | the carrier of X) . x = z and
A39: dom z = dom (Carrier J) and
for i being object st i in dom (Carrier J) holds
z . i in (Carrier J) . i by CARD_3:def 5;
f . x in rng f by A34, A36, FUNCT_1:def 3;
then f . x in the carrier of (product J) ;
then A40: f . x in product (Carrier J) by Def3;
then consider y being Function such that
A41: f . x = y and
A42: dom y = dom (Carrier J) and
for i being object st i in dom (Carrier J) holds
y . i in (Carrier J) . i by CARD_3:def 5;
A43: x in the carrier of Y by A37;
for j being object st j in dom y holds
y . j = z . j
proof
let j be object ; :: thesis: ( j in dom y implies y . j = z . j )
assume j in dom y ; :: thesis: y . j = z . j
then A44: j in I by A42;
then consider i being Element of I such that
A45: i = j and
A46: 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 A7;
A47: y in dom (proj ((Carrier J),i)) by A40, A41, CARD_3:def 16;
consider g being Function of Y,(J . i) such that
g is continuous and
A48: g | the carrier of X = (proj (J,i)) * f and
A49: G . j = g by A46;
( x in dom h & z = <:G:> . x ) by A36, A43, A38, FUNCT_1:49, FUNCT_2:def 1;
hence z . j = g . x by A6, A44, A49, FUNCT_6:34
.= ((proj (J,i)) * f) . x by A36, A48, FUNCT_1:49
.= (proj ((Carrier J),i)) . y by A36, A41, FUNCT_2:15
.= y . j by A45, A47, CARD_3:def 16 ;
:: thesis: verum
end;
hence (h | the carrier of X) . x = f . x by A41, A42, A38, A39, FUNCT_1:2; :: thesis: verum
end;
reconsider h = h as Function of Y,(product J) ;
A50: 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 )
reconsider p = P as Subset of (product (Carrier J)) by Def3;
assume P in product_prebasis J ; :: thesis: h " P is open
then consider i being set , T being TopStruct , V being Subset of T such that
A51: i in I and
A52: V is open and
A53: T = J . i and
A54: p = product ((Carrier J) +* (i,V)) by Def2;
consider j being Element of I such that
A55: j = i and
A56: 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 A7, A51;
reconsider V = V as Subset of (J . j) by A53, A55;
A57: dom (proj (J,j)) = product (Carrier J) by CARD_3:def 16;
consider g being Function of Y,(J . j) such that
A58: g is continuous and
g | the carrier of X = (proj (J,j)) * f and
A59: G . i = g by A56;
A60: dom g = the carrier of Y by FUNCT_2:def 1
.= dom h by FUNCT_2:def 1 ;
A61: (proj (J,j)) " V = p by A54, A55, Th4;
A62: h " P c= g " V
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in h " P or x in g " V )
assume A63: x in h " P ; :: thesis: x in g " V
then A64: h . x in (proj (J,j)) " V by A61, FUNCT_1:def 7;
then h . x in product (Carrier J) by A57, FUNCT_1:def 7;
then consider y being Function such that
A65: h . x = y and
dom y = dom (Carrier J) and
for i being object st i in dom (Carrier J) holds
y . i in (Carrier J) . i by CARD_3:def 5;
h . x in dom (proj (J,j)) by A64, FUNCT_1:def 7;
then (proj (J,j)) . (h . x) = y . j by A65, CARD_3:def 16;
then A66: y . j in V by A64, FUNCT_1:def 7;
x in dom h by A63, FUNCT_1:def 7;
then A67: g . x = y . j by A6, A55, A59, A65, FUNCT_6:34;
x in dom g by A60, A63, FUNCT_1:def 7;
hence x in g " V by A66, A67, FUNCT_1:def 7; :: thesis: verum
end;
A68: g " V c= h " P
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g " V or x in h " P )
assume A69: x in g " V ; :: thesis: x in h " P
then A70: x in dom h by A60, FUNCT_1:def 7;
then A71: h . x in rng h by FUNCT_1:def 3;
then consider y being Function such that
A72: h . x = y and
dom y = dom (Carrier J) and
for i being object st i in dom (Carrier J) holds
y . i in (Carrier J) . i by A33, CARD_3:def 5;
h . x in product (Carrier J) by A33, A71;
then y in dom (proj ((Carrier J),j)) by A72, CARD_3:def 16;
then A73: (proj (J,j)) . (h . x) = y . j by A72, CARD_3:def 16;
g . x = y . j by A6, A55, A59, A70, A72, FUNCT_6:34;
then (proj (J,j)) . (h . x) in V by A69, A73, FUNCT_1:def 7;
then h . x in (proj (J,j)) " V by A33, A57, A71, FUNCT_1:def 7;
hence x in h " P by A61, A70, FUNCT_1:def 7; :: thesis: verum
end;
[#] (J . j) <> {} ;
then g " V is open by A52, A53, A55, A58, TOPS_2:43;
hence h " P is open by A62, A68, XBOOLE_0:def 10; :: thesis: verum
end;
take h ; :: thesis: ( h is continuous & h | the carrier of X = f )
product_prebasis J is prebasis of (product J) by Def3;
hence h is continuous by A50, YELLOW_9:36; :: thesis: h | the carrier of X = f
thus h | the carrier of X = f by A34, A35, FUNCT_1:2; :: thesis: verum