let I1, I2 be non empty set ; for J1 being non-Empty TopSpace-yielding ManySortedSet of I1
for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
let J1 be non-Empty TopSpace-yielding ManySortedSet of I1; for J2 being non-Empty TopSpace-yielding ManySortedSet of I2
for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
let J2 be non-Empty TopSpace-yielding ManySortedSet of I2; for p being Function of I1,I2
for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
let p be Function of I1,I2; for H being ProductHomeo of J1,J2,p
for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
let H be ProductHomeo of J1,J2,p; for F being ManySortedFunction of I1 st p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) holds
for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
let F be ManySortedFunction of I1; ( p is bijective & ( for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism ) ) & ( for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i) ) implies for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U))) )
assume that
A1:
p is bijective
and
A2:
for i being Element of I1 ex f being Function of (J1 . i),((J2 * p) . i) st
( F . i = f & f is being_homeomorphism )
and
A3:
for g being Element of (product J1)
for i being Element of I1 holds (H . g) . (p . i) = (F . i) . (g . i)
; for i being Element of I1
for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
let i be Element of I1; for U being Subset of (J1 . i) holds H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
let U be Subset of (J1 . i); H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
reconsider j = p . i as Element of I2 ;
i in I1
;
then A4:
i in dom p
by FUNCT_2:def 1;
consider f being Function of (J1 . i),((J2 * p) . i) such that
A5:
( F . i = f & f is being_homeomorphism )
by A2;
A6: rng f =
[#] ((J2 * p) . i)
by A5, TOPS_2:def 5
.=
[#] (J2 . j)
by A4, FUNCT_1:13
.=
the carrier of (J2 . j)
by STRUCT_0:def 3
;
for y being object holds
( y in H .: (product ((Carrier J1) +* (i,U))) iff y in product ((Carrier J2) +* (j,((F . i) .: U))) )
proof
let y be
object ;
( y in H .: (product ((Carrier J1) +* (i,U))) iff y in product ((Carrier J2) +* (j,((F . i) .: U))) )
thus
(
y in H .: (product ((Carrier J1) +* (i,U))) implies
y in product ((Carrier J2) +* (j,((F . i) .: U))) )
( y in product ((Carrier J2) +* (j,((F . i) .: U))) implies y in H .: (product ((Carrier J1) +* (i,U))) )proof
assume
y in H .: (product ((Carrier J1) +* (i,U)))
;
y in product ((Carrier J2) +* (j,((F . i) .: U)))
then consider x being
object such that A8:
(
x in dom H &
x in product ((Carrier J1) +* (i,U)) &
y = H . x )
by FUNCT_1:def 6;
reconsider g =
x as
Element of
(product J1) by A8;
y in rng H
by A8, FUNCT_1:3;
then reconsider h =
y as
Element of
(product J2) ;
h in the
carrier of
(product J2)
;
then A9:
h in product (Carrier J2)
by WAYBEL18:def 3;
then A10:
dom h =
dom (Carrier J2)
by CARD_3:9
.=
dom ((Carrier J2) +* (j,((F . i) .: U)))
by FUNCT_7:30
;
for
z being
object st
z in dom ((Carrier J2) +* (j,((F . i) .: U))) holds
h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z
proof
let z be
object ;
( z in dom ((Carrier J2) +* (j,((F . i) .: U))) implies h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z )
assume a11:
z in dom ((Carrier J2) +* (j,((F . i) .: U)))
;
h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z
then A11:
z in dom (Carrier J2)
by FUNCT_7:30;
reconsider j0 =
z as
Element of
I2 by a11;
I2 = rng p
by A1, FUNCT_2:def 3;
then consider i0 being
object such that A12:
(
i0 in I1 &
p . i0 = j0 )
by FUNCT_2:11;
reconsider i0 =
i0 as
Element of
I1 by A12;
consider f0 being
Function of
(J1 . i0),
((J2 * p) . i0) such that A13:
(
F . i0 = f0 &
f0 is
being_homeomorphism )
by A2;
A14:
h . j0 = f0 . (g . i0)
by A3, A8, A12, A13;
per cases
( j0 = j or j0 <> j )
;
suppose A15:
j0 = j
;
h . z in ((Carrier J2) +* (j,((F . i) .: U))) . zthen A16:
((Carrier J2) +* (j,((F . i) .: U))) . z = (F . i) .: U
by A11, FUNCT_7:31;
A17:
i0 = i
by A1, A12, A15, FUNCT_2:19;
a18:
I1 = dom (Carrier J1)
by PARTFUN1:def 2;
then
i in dom (Carrier J1)
;
then
i in dom ((Carrier J1) +* (i,U))
by FUNCT_7:30;
then
g . i in ((Carrier J1) +* (i,U)) . i
by A8, CARD_3:9;
then
g . i in U
by a18, FUNCT_7:31;
hence
h . z in ((Carrier J2) +* (j,((F . i) .: U))) . z
by A14, A16, A17, A13, FUNCT_2:35;
verum end; end;
end;
hence
y in product ((Carrier J2) +* (j,((F . i) .: U)))
by A10, CARD_3:9;
verum
end;
assume A20:
y in product ((Carrier J2) +* (j,((F . i) .: U)))
;
y in H .: (product ((Carrier J1) +* (i,U)))
then reconsider h =
y as
Element of
product ((Carrier J2) +* (j,((F . i) .: U))) ;
A21: the
carrier of
(J1 . i) =
[#] (J1 . i)
by STRUCT_0:def 3
.=
(Carrier J1) . i
by PENCIL_3:7
;
i in I1
;
then A22:
i in dom (Carrier J1)
by PARTFUN1:def 2;
then A23:
product ((Carrier J1) +* (i,U)) c= product (Carrier J1)
by A21, Th39;
A24:
(Carrier J2) . j =
[#] (J2 . j)
by PENCIL_3:7
.=
the
carrier of
(J2 . j)
by STRUCT_0:def 3
;
a25:
(
j in I2 &
(F . i) .: U c= the
carrier of
(J2 . j) )
by A6, A5, RELAT_1:111;
then A25:
(
j in dom (Carrier J2) &
(F . i) .: U c= (Carrier J2) . j )
by A24, PARTFUN1:def 2;
then A26:
product ((Carrier J2) +* (j,((F . i) .: U))) c= product (Carrier J2)
by Th39;
ex
x being
object st
(
x in dom H &
x in product ((Carrier J1) +* (i,U)) &
H . x = y )
proof
defpred S1[
object ,
object ]
means ex
f being
one-to-one Function st
(
F . $1
= f & $2
= (f ") . (h . (p . $1)) );
A28:
for
i0 being
Element of
I1 ex
y being
object st
S1[
i0,
y]
consider g being
ManySortedSet of
I1 such that A30:
for
i being
Element of
I1 holds
S1[
i,
g . i]
from PBOOLE:sch 6(A28);
take
g
;
( g in dom H & g in product ((Carrier J1) +* (i,U)) & H . g = y )
A31:
dom g =
I1
by PARTFUN1:def 2
.=
dom ((Carrier J1) +* (i,U))
by PARTFUN1:def 2
;
a36:
for
z being
object st
z in dom ((Carrier J1) +* (i,U)) holds
g . z in ((Carrier J1) +* (i,U)) . z
proof
let z be
object ;
( z in dom ((Carrier J1) +* (i,U)) implies g . z in ((Carrier J1) +* (i,U)) . z )
assume
z in dom ((Carrier J1) +* (i,U))
;
g . z in ((Carrier J1) +* (i,U)) . z
then reconsider i0 =
z as
Element of
I1 ;
consider f0 being
one-to-one Function such that A32:
(
F . i0 = f0 &
g . i0 = (f0 ") . (h . (p . i0)) )
by A30;
p . i0 in I2
;
then
p . i0 in dom (Carrier J2)
by PARTFUN1:def 2;
then
h . (p . i0) in (Carrier J2) . (p . i0)
by A20, A26, CARD_3:9;
then
h . (p . i0) in [#] (J2 . (p . i0))
by PENCIL_3:7;
then A33:
h . (p . i0) in [#] ((J2 * p) . i0)
by FUNCT_2:15;
per cases
( i = i0 or i <> i0 )
;
suppose A35:
i = i0
;
g . z in ((Carrier J1) +* (i,U)) . zthen A36:
((Carrier J1) +* (i,U)) . z = U
by A22, FUNCT_7:31;
j in dom ((Carrier J2) +* (j,((F . i) .: U)))
by a25, PARTFUN1:def 2;
then
h . j in ((Carrier J2) +* (j,((F . i) .: U))) . j
by A20, CARD_3:9;
then A37:
h . j in (F . i) .: U
by A25, FUNCT_7:31;
A38:
f " = f0 "
by A5, A32, A35, TOPS_2:def 4;
[#] ((J2 * p) . i0) =
rng f
by A5, A35, TOPS_2:def 5
.=
dom (f0 ")
by A5, A32, A35, FUNCT_1:33
;
then
g . i0 in rng (f0 ")
by A32, A33, FUNCT_1:3;
then A39:
g . i0 in dom f
by A5, A32, A35, FUNCT_1:33;
h . j in (Carrier J2) . j
by A20, A26, A25, CARD_3:9;
then
h . j in [#] (J2 . j)
by PENCIL_3:7;
then a40:
h . j in [#] ((J2 * p) . i)
by A4, FUNCT_1:13;
a41:
dom f = the
carrier of
(J1 . i)
by FUNCT_2:def 1;
reconsider f1 =
f as
one-to-one Function by A5;
A43:
h . j in rng f1
by a40, A5, TOPS_2:def 5;
f . ((f ") . (h . j)) =
f1 . ((f1 ") . (h . j))
by A5, TOPS_2:def 4
.=
h . j
by A43, FUNCT_1:35
;
then
g . i0 in f0 " (f0 .: U)
by A5, A32, A35, A38, A39, A37, FUNCT_1:def 7;
hence
g . z in ((Carrier J1) +* (i,U)) . z
by A36, a41, A5, A32, A35, FUNCT_1:94;
verum end; suppose
i <> i0
;
g . z in ((Carrier J1) +* (i,U)) . zthen A44:
((Carrier J1) +* (i,U)) . z = (Carrier J1) . z
by FUNCT_7:32;
consider f9 being
Function of
(J1 . i0),
((J2 * p) . i0) such that A45:
(
F . i0 = f9 &
f9 is
being_homeomorphism )
by A2;
dom (f0 ") =
rng f0
by FUNCT_1:33
.=
[#] ((J2 * p) . i0)
by A32, A45, TOPS_2:def 5
.=
the
carrier of
((J2 * p) . i0)
by STRUCT_0:def 3
;
then
(f0 ") . (h . (p . i0)) in rng (f0 ")
by A33, FUNCT_1:3;
then
g . i0 in dom f0
by A32, FUNCT_1:33;
then
g . i0 in [#] (J1 . i0)
by A32, A45, TOPS_2:def 5;
hence
g . z in ((Carrier J1) +* (i,U)) . z
by A44, PENCIL_3:7;
verum end; end;
end;
then
g in product ((Carrier J1) +* (i,U))
by A31, CARD_3:9;
then
g in product (Carrier J1)
by A23;
then A47:
g in the
carrier of
(product J1)
by WAYBEL18:def 3;
hence
(
g in dom H &
g in product ((Carrier J1) +* (i,U)) )
by a36, A31, CARD_3:9, FUNCT_2:def 1;
H . g = y
reconsider h0 =
H . g as
Element of
(product J2) by A47, FUNCT_2:5;
h0 in the
carrier of
(product J2)
;
then
h0 in product (Carrier J2)
by WAYBEL18:def 3;
then A48:
dom h0 =
dom (Carrier J2)
by CARD_3:9
.=
dom h
by A20, A26, CARD_3:9
;
for
z being
object st
z in dom h holds
h . z = h0 . z
proof
let z be
object ;
( z in dom h implies h . z = h0 . z )
assume
z in dom h
;
h . z = h0 . z
then
z in dom (Carrier J2)
by A20, A26, CARD_3:9;
then reconsider j0 =
z as
Element of
I2 ;
reconsider p9 =
p as
one-to-one Function by A1;
j0 in I2
;
then A49:
j0 in rng p9
by A1, FUNCT_2:def 3;
then
j0 in dom (p9 ")
by FUNCT_1:33;
then
(p9 ") . j0 in rng (p9 ")
by FUNCT_1:3;
then A50:
(p9 ") . j0 in dom p9
by FUNCT_1:33;
then reconsider i0 =
(p9 ") . j0 as
Element of
I1 by FUNCT_2:def 1;
consider f9 being
one-to-one Function such that A51:
(
F . i0 = f9 &
g . i0 = (f9 ") . (h . (p . i0)) )
by A30;
consider f0 being
Function of
(J1 . i0),
((J2 * p) . i0) such that A52:
(
F . i0 = f0 &
f0 is
being_homeomorphism )
by A2;
A53:
rng f9 =
[#] ((J2 * p) . i0)
by A51, A52, TOPS_2:def 5
.=
the
carrier of
((J2 * p) . i0)
by STRUCT_0:def 3
;
A54:
p . i0 = j0
by A49, FUNCT_1:35;
A55:
(Carrier J2) . (p . i0) =
[#] (J2 . (p . i0))
by PENCIL_3:7
.=
[#] ((J2 * p) . i0)
by A50, FUNCT_1:13
.=
the
carrier of
((J2 * p) . i0)
by STRUCT_0:def 3
;
p . i0 in I2
;
then
p . i0 in dom (Carrier J2)
by PARTFUN1:def 2;
then A56:
h . (p . i0) in (Carrier J2) . (p . i0)
by A20, A26, CARD_3:9;
h . j0 =
f9 . ((f9 ") . (h . (p . i0)))
by A53, A54, A55, A56, FUNCT_1:35
.=
h0 . j0
by A3, A47, A51, A54
;
hence
h . z = h0 . z
;
verum
end;
hence
H . g = y
by A48, FUNCT_1:2;
verum
end;
hence
y in H .: (product ((Carrier J1) +* (i,U)))
by FUNCT_1:def 6;
verum
end;
hence
H .: (product ((Carrier J1) +* (i,U))) = product ((Carrier J2) +* ((p . i),((F . i) .: U)))
by TARSKI:2; verum