reconsider B1 = product b1 as Segre-Coset of A by A2;
set s = permutation_of_indices f;
set i = indx b1;
defpred S1[ object , object ] means for J being ManySortedSet of I st J in f .: (product (b1 +* ((indx b1),{$1}))) holds
$2 = J . ((permutation_of_indices f) . (indx b1));
set B = the carrier of (A . (indx b1));
set t = permutation_of_indices f;
reconsider B2 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A3:
product b2 = B2
and
A4:
b2 . (indx b2) = [#] (A . (indx b2))
by PENCIL_2:def 2;
set j = indx b2;
A5:
f is bijective
by PENCIL_2:def 4;
then A6:
f " B2 c= B1
by FUNCT_1:82;
A7:
Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #)
by PENCIL_1:def 23;
A8:
for x being object st x in the carrier of (A . (indx b1)) holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in the carrier of (A . (indx b1)) implies ex y being object st S1[x,y] )
consider bb being
object such that A9:
bb in B1
by XBOOLE_0:def 1;
A10:
ex
bf being
Function st
(
bf = bb &
dom bf = dom b1 & ( for
o being
object st
o in dom b1 holds
bf . o in b1 . o ) )
by A9, CARD_3:def 5;
A11:
dom b1 = I
by PARTFUN1:def 2;
then reconsider bb =
bb as
ManySortedSet of
I by A10, PARTFUN1:def 2, RELAT_1:def 18;
set bbx =
bb +* (
(indx b1),
x);
A12:
{(bb +* ((indx b1),x))} = product (b1 +* ((indx b1),{x}))
proof
thus
{(bb +* ((indx b1),x))} c= product (b1 +* ((indx b1),{x}))
XBOOLE_0:def 10 product (b1 +* ((indx b1),{x})) c= {(bb +* ((indx b1),x))}proof
let o be
object ;
TARSKI:def 3 ( not o in {(bb +* ((indx b1),x))} or o in product (b1 +* ((indx b1),{x})) )
assume
o in {(bb +* ((indx b1),x))}
;
o in product (b1 +* ((indx b1),{x}))
then A18:
o = bb +* (
(indx b1),
x)
by TARSKI:def 1;
dom (bb +* ((indx b1),x)) =
I
by PARTFUN1:def 2
.=
dom (b1 +* ((indx b1),{x}))
by PARTFUN1:def 2
;
hence
o in product (b1 +* ((indx b1),{x}))
by A18, A13, CARD_3:9;
verum
end;
let o be
object ;
TARSKI:def 3 ( not o in product (b1 +* ((indx b1),{x})) or o in {(bb +* ((indx b1),x))} )
assume
o in product (b1 +* ((indx b1),{x}))
;
o in {(bb +* ((indx b1),x))}
then consider u being
Function such that A19:
u = o
and A20:
dom u = dom (b1 +* ((indx b1),{x}))
and A21:
for
z being
object st
z in dom (b1 +* ((indx b1),{x})) holds
u . z in (b1 +* ((indx b1),{x})) . z
by CARD_3:def 5;
A22:
now for z being object st z in dom u holds
u . z = (bb +* ((indx b1),x)) . zlet z be
object ;
( z in dom u implies u . b1 = (bb +* ((indx b1),x)) . b1 )assume A23:
z in dom u
;
u . b1 = (bb +* ((indx b1),x)) . b1then A24:
z in I
by A20;
reconsider zz =
z as
Element of
I by A20, A23;
A25:
u . z in (b1 +* ((indx b1),{x})) . z
by A20, A21, A23;
per cases
( zz = indx b1 or zz <> indx b1 )
;
suppose A27:
zz <> indx b1
;
u . b1 = (bb +* ((indx b1),x)) . b1then
( not
b1 . zz is
empty &
b1 . zz is
trivial )
by PENCIL_1:def 21;
then
b1 . zz is 1
-element
;
then consider o being
object such that A28:
b1 . z = {o}
by ZFMISC_1:131;
u . z in b1 . z
by A25, A27, FUNCT_7:32;
then A29:
u . z = o
by A28, TARSKI:def 1;
(bb +* ((indx b1),x)) . z = bb . z
by A27, FUNCT_7:32;
then
(bb +* ((indx b1),x)) . z in {o}
by A10, A11, A24, A28;
hence
u . z = (bb +* ((indx b1),x)) . z
by A29, TARSKI:def 1;
verum end; end; end;
dom u =
I
by A20, PARTFUN1:def 2
.=
dom (bb +* ((indx b1),x))
by PARTFUN1:def 2
;
then
u = bb +* (
(indx b1),
x)
by A22;
hence
o in {(bb +* ((indx b1),x))}
by A19, TARSKI:def 1;
verum
end;
assume A30:
x in the
carrier of
(A . (indx b1))
;
ex y being object st S1[x,y]
dom (bb +* ((indx b1),x)) =
I
by PARTFUN1:def 2
.=
dom (Carrier A)
by PARTFUN1:def 2
;
then reconsider bbx1 =
bb +* (
(indx b1),
x) as
Point of
(Segre_Product A) by A7, A31, CARD_3:9;
reconsider fbbx =
f . bbx1 as
ManySortedSet of
I by PENCIL_1:14;
take
fbbx . ((permutation_of_indices f) . (indx b1))
;
S1[x,fbbx . ((permutation_of_indices f) . (indx b1))]
dom f = the
carrier of
(Segre_Product A)
by FUNCT_2:def 1;
then
bbx1 in dom f
;
then A36:
Im (
f,
(bb +* ((indx b1),x)))
= {(f . (bb +* ((indx b1),x)))}
by FUNCT_1:59;
let J be
ManySortedSet of
I;
( J in f .: (product (b1 +* ((indx b1),{x}))) implies fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1)) )
assume
J in f .: (product (b1 +* ((indx b1),{x})))
;
fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1))
hence
fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1))
by A12, A36, TARSKI:def 1;
verum
end;
consider M being Function such that
A37:
( dom M = the carrier of (A . (indx b1)) & ( for x being object st x in the carrier of (A . (indx b1)) holds
S1[x,M . x] ) )
from CLASSES1:sch 1(A8);
A38:
dom f = the carrier of (Segre_Product A)
by FUNCT_2:def 1;
then
B1 c= f " B2
by FUNCT_1:76;
then A39:
f " B2 = B1
by A6;
rng M c= the carrier of (A . ((permutation_of_indices f) . (indx b1)))
proof
let x be
object ;
TARSKI:def 3 ( not x in rng M or x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) )
assume
x in rng M
;
x in the carrier of (A . ((permutation_of_indices f) . (indx b1)))
then consider o being
object such that A40:
o in dom M
and A41:
x = M . o
by FUNCT_1:def 3;
reconsider o =
o as
Point of
(A . (indx b1)) by A37, A40;
consider p being
ManySortedSet of
I such that A42:
p in product b1
and A43:
{(p +* ((indx b1),o))} = product (b1 +* ((indx b1),{o}))
by Th18;
reconsider pio =
p +* (
(indx b1),
o) as
Point of
(Segre_Product A) by A2, A42, PENCIL_1:25;
reconsider J =
f . pio as
ManySortedSet of
I by PENCIL_1:14;
Im (
f,
(p +* ((indx b1),o)))
= {(f . pio)}
by A38, FUNCT_1:59;
then A44:
J in f .: (product (b1 +* ((indx b1),{o})))
by A43, TARSKI:def 1;
(permutation_of_indices f) . (indx b1) in I
;
then
(permutation_of_indices f) . (indx b1) in dom (Carrier A)
by PARTFUN1:def 2;
then
J . ((permutation_of_indices f) . (indx b1)) in (Carrier A) . ((permutation_of_indices f) . (indx b1))
by A7, CARD_3:9;
then
J . ((permutation_of_indices f) . (indx b1)) in [#] (A . ((permutation_of_indices f) . (indx b1)))
by Th7;
hence
x in the
carrier of
(A . ((permutation_of_indices f) . (indx b1)))
by A37, A41, A44;
verum
end;
then reconsider M = M as Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) by A37, FUNCT_2:def 1, RELSET_1:4;
set m = M;
A45:
indx b2 = (permutation_of_indices f) . (indx b1)
by A1, A3, Def3;
A46:
M is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom M or not x2 in dom M or not M . x1 = M . x2 or x1 = x2 )
assume that A47:
(
x1 in dom M &
x2 in dom M )
and A48:
M . x1 = M . x2
;
x1 = x2
reconsider o1 =
x1,
o2 =
x2 as
Point of
(A . (indx b1)) by A47;
consider p1 being
ManySortedSet of
I such that A49:
p1 in product b1
and A50:
{(p1 +* ((indx b1),o1))} = product (b1 +* ((indx b1),{o1}))
by Th18;
reconsider p1io =
p1 +* (
(indx b1),
o1) as
Point of
(Segre_Product A) by A2, A49, PENCIL_1:25;
reconsider J1 =
f . p1io as
ManySortedSet of
I by PENCIL_1:14;
consider p2 being
ManySortedSet of
I such that A51:
p2 in product b1
and A52:
{(p2 +* ((indx b1),o2))} = product (b1 +* ((indx b1),{o2}))
by Th18;
A53:
dom b1 = I
by PARTFUN1:def 2;
A54:
dom p1 = I
by PARTFUN1:def 2;
dom (p1 +* ((indx b1),o1)) = I
by PARTFUN1:def 2;
then
p1io in product b1
by A53, A55, CARD_3:9;
then A58:
J1 in B2
by A38, FUNCT_1:def 6;
reconsider p2io =
p2 +* (
(indx b1),
o2) as
Point of
(Segre_Product A) by A2, A51, PENCIL_1:25;
reconsider J2 =
f . p2io as
ManySortedSet of
I by PENCIL_1:14;
Im (
f,
(p2 +* ((indx b1),o2)))
= {(f . p2io)}
by A38, FUNCT_1:59;
then
J2 in f .: (product (b1 +* ((indx b1),{o2})))
by A52, TARSKI:def 1;
then A59:
M . o2 = J2 . ((permutation_of_indices f) . (indx b1))
by A37;
dom p1 = I
by PARTFUN1:def 2;
then A60:
(p1 +* ((indx b1),o1)) . (indx b1) = o1
by FUNCT_7:31;
A61:
dom b1 = I
by PARTFUN1:def 2;
A62:
dom p2 = I
by PARTFUN1:def 2;
dom (p2 +* ((indx b1),o2)) = I
by PARTFUN1:def 2;
then
p2io in product b1
by A61, A63, CARD_3:9;
then A66:
J2 in B2
by A38, FUNCT_1:def 6;
Im (
f,
(p1 +* ((indx b1),o1)))
= {(f . p1io)}
by A38, FUNCT_1:59;
then A67:
J1 in f .: (product (b1 +* ((indx b1),{o1})))
by A50, TARSKI:def 1;
A68:
now for o being object st o in I holds
J1 . o = J2 . olet o be
object ;
( o in I implies J1 . b1 = J2 . b1 )assume
o in I
;
J1 . b1 = J2 . b1then reconsider l =
o as
Element of
I ;
end;
dom p2 = I
by PARTFUN1:def 2;
then A69:
(p2 +* ((indx b1),o2)) . (indx b1) = o2
by FUNCT_7:31;
J1 = J2
by A68;
hence
x1 = x2
by A38, A5, A60, A69, FUNCT_1:def 4;
verum
end;
f is bijective
by PENCIL_2:def 4;
then A70:
rng f = the carrier of (Segre_Product A)
by FUNCT_2:def 3;
A71:
f " = f "
by A5, TOPS_2:def 4;
the carrier of (A . ((permutation_of_indices f) . (indx b1))) c= rng M
proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) or x in rng M )
assume
x in the
carrier of
(A . ((permutation_of_indices f) . (indx b1)))
;
x in rng M
then reconsider x1 =
x as
Point of
(A . ((permutation_of_indices f) . (indx b1))) ;
consider p0 being
ManySortedSet of
I such that A72:
p0 in product b2
and
{(p0 +* ((indx b2),x1))} = product (b2 +* ((indx b2),{x1}))
by A45, Th18;
reconsider p =
p0 +* (
(indx b2),
x1) as
Point of
(Segre_Product A) by A3, A45, A72, PENCIL_1:25;
reconsider p1 =
p as
ManySortedSet of
I ;
reconsider q =
(f ") . p as
ManySortedSet of
I by PENCIL_1:14;
A73:
p = f . ((f ") . p)
by A70, A5, A71, FUNCT_1:35;
A74:
dom b1 = I
by PARTFUN1:def 2;
A75:
now for o being object st o in I holds
q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . olet o be
object ;
( o in I implies q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1 )assume
o in I
;
q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1then reconsider l =
o as
Element of
I ;
per cases
( l = indx b1 or l <> indx b1 )
;
suppose
l <> indx b1
;
q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1then A76:
(b1 +* ((indx b1),{(q . (indx b1))})) . l = b1 . l
by FUNCT_7:32;
A77:
dom b2 = I
by PARTFUN1:def 2;
A78:
dom p0 = I
by PARTFUN1:def 2;
dom p1 = I
by PARTFUN1:def 2;
then
p in product b2
by A77, A79, CARD_3:9;
then consider q0 being
object such that A82:
q0 in dom f
and A83:
q0 in B1
and A84:
p = f . q0
by A3, FUNCT_1:def 6;
q = q0
by A38, A5, A73, A82, A84, FUNCT_1:def 4;
hence
q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o
by A74, A76, A83, CARD_3:9;
verum end; end; end;
I = dom (Carrier A)
by PARTFUN1:def 2;
then
q . (indx b1) in (Carrier A) . (indx b1)
by A7, CARD_3:9;
then A85:
q . (indx b1) in [#] (A . (indx b1))
by Th7;
(
dom q = I &
dom (b1 +* ((indx b1),{(q . (indx b1))})) = I )
by PARTFUN1:def 2;
then
q in product (b1 +* ((indx b1),{(q . (indx b1))}))
by A75, CARD_3:9;
then
p0 +* (
(indx b2),
x1)
in f .: (product (b1 +* ((indx b1),{(q . (indx b1))})))
by A38, A73, FUNCT_1:def 6;
then
(
dom p0 = I &
M . (q . (indx b1)) = (p0 +* ((indx b2),x1)) . ((permutation_of_indices f) . (indx b1)) )
by A37, A85, PARTFUN1:def 2;
then
(
dom M = the
carrier of
(A . (indx b1)) &
M . (q . (indx b1)) = x )
by A45, FUNCT_2:def 1, FUNCT_7:31;
hence
x in rng M
by A85, FUNCT_1:3;
verum
end;
then A86:
rng M = the carrier of (A . ((permutation_of_indices f) . (indx b1)))
;
then
M is onto
by FUNCT_2:def 3;
then A87:
M " = M "
by A46, TOPS_2:def 4;
A88:
M " is open
proof
let S0 be
Subset of
(A . ((permutation_of_indices f) . (indx b1)));
T_0TOPSP:def 2 ( not S0 is open or (M ") .: S0 is open )
assume
S0 is
open
;
(M ") .: S0 is open
then reconsider S =
S0 as
Block of
(A . ((permutation_of_indices f) . (indx b1))) by PRE_TOPC:def 2;
reconsider L =
product (b2 +* ((indx b2),S)) as
Block of
(Segre_Product A) by A45, Th12;
reconsider K =
f " L as
Block of
(Segre_Product A) ;
consider k being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A89:
K = product k
and A90:
k . (indx k) is
Block of
(A . (indx k))
by PENCIL_1:24;
A91:
dom b2 = I
by PARTFUN1:def 2;
dom (b2 +* ((indx b2),S)) = I
by PARTFUN1:def 2;
then
L c= product b2
by A91, A92, CARD_3:27;
then
(product b1) /\ (product k) = K
by A3, A39, A89, RELAT_1:143, XBOOLE_1:28;
then A94:
2
c= card ((product b1) /\ (product k))
by PENCIL_1:def 6;
then A95:
indx k = indx b1
by PENCIL_1:26;
M " S = k . (indx k)
proof
thus
M " S c= k . (indx k)
XBOOLE_0:def 10 k . (indx k) c= M " Sproof
let o be
object ;
TARSKI:def 3 ( not o in M " S or o in k . (indx k) )
A96:
dom b2 = I
by PARTFUN1:def 2;
assume A97:
o in M " S
;
o in k . (indx k)
then reconsider u =
o as
Point of
(A . (indx b1)) ;
consider p being
ManySortedSet of
I such that A98:
p in product b1
and A99:
{(p +* ((indx b1),u))} = product (b1 +* ((indx b1),{u}))
by Th18;
reconsider q =
p +* (
(indx b1),
u) as
Point of
(Segre_Product A) by A2, A98, PENCIL_1:25;
reconsider fq =
f . q as
ManySortedSet of
I by PENCIL_1:14;
Im (
f,
(p +* ((indx b1),u)))
= {(f . q)}
by A38, FUNCT_1:59;
then A100:
fq in f .: (product (b1 +* ((indx b1),{u})))
by A99, TARSKI:def 1;
product (b1 +* ((indx b1),{u})) c= product b1
then A108:
f .: (product (b1 +* ((indx b1),{u}))) c= product b2
by A3, RELAT_1:123;
M . o in S
by A97, FUNCT_1:def 7;
then A109:
fq . ((permutation_of_indices f) . (indx b1)) in S
by A37, A100;
(
dom fq = I &
dom (b2 +* ((indx b2),S)) = I )
by PARTFUN1:def 2;
then
fq in L
by A110, CARD_3:9;
then
(
dom k = I &
q in K )
by A38, FUNCT_1:def 7, PARTFUN1:def 2;
then
(
dom p = I &
(p +* ((indx b1),u)) . (indx b1) in k . (indx b1) )
by A89, CARD_3:9, PARTFUN1:def 2;
hence
o in k . (indx k)
by A95, FUNCT_7:31;
verum
end;
let o be
object ;
TARSKI:def 3 ( not o in k . (indx k) or o in M " S )
assume A112:
o in k . (indx k)
;
o in M " S
k . (indx k) in the
topology of
(A . (indx b1))
by A90, A95;
then reconsider u =
o as
Point of
(A . (indx b1)) by A112;
consider p0 being
ManySortedSet of
I such that A113:
p0 in product b1
and A114:
{(p0 +* ((indx b1),u))} = product (b1 +* ((indx b1),{u}))
by Th18;
reconsider p =
p0 +* (
(indx b1),
u) as
Point of
(Segre_Product A) by A2, A113, PENCIL_1:25;
reconsider fp =
f . p as
ManySortedSet of
I by PENCIL_1:14;
A115:
dom b1 = I
by PARTFUN1:def 2;
A116:
dom p0 = I
by PARTFUN1:def 2;
(
dom (p0 +* ((indx b1),u)) = I &
dom k = I )
by PARTFUN1:def 2;
then
p in K
by A89, A117, CARD_3:9;
then
(
dom (b2 +* ((indx b2),S)) = I &
fp in L )
by FUNCT_1:def 7, PARTFUN1:def 2;
then
(
dom b2 = I &
fp . (indx b2) in (b2 +* ((indx b2),S)) . (indx b2) )
by CARD_3:9, PARTFUN1:def 2;
then A120:
fp . ((permutation_of_indices f) . (indx b1)) in S
by A45, FUNCT_7:31;
Im (
f,
(p0 +* ((indx b1),u)))
= {(f . p)}
by A38, FUNCT_1:59;
then
fp in f .: (product (b1 +* ((indx b1),{u})))
by A114, TARSKI:def 1;
then
M . u = fp . ((permutation_of_indices f) . (indx b1))
by A37;
hence
o in M " S
by A37, A120, FUNCT_1:def 7;
verum
end;
then
(M ") .: S is
Block of
(A . (indx b1))
by A46, A87, A90, A95, FUNCT_1:85;
hence
(M ") .: S0 is
open
by PRE_TOPC:def 2;
verum
end;
A121:
M is open
proof
let S0 be
Subset of
(A . (indx b1));
T_0TOPSP:def 2 ( not S0 is open or M .: S0 is open )
assume
S0 is
open
;
M .: S0 is open
then reconsider S =
S0 as
Block of
(A . (indx b1)) by PRE_TOPC:def 2;
reconsider L =
product (b1 +* ((indx b1),S)) as
Block of
(Segre_Product A) by Th12;
reconsider K =
f .: L as
Block of
(Segre_Product A) ;
consider k being non
trivial-yielding Segre-like ManySortedSubset of
Carrier A such that A122:
K = product k
and A123:
k . (indx k) is
Block of
(A . (indx k))
by PENCIL_1:24;
A124:
dom b1 = I
by PARTFUN1:def 2;
dom (b1 +* ((indx b1),S)) = I
by PARTFUN1:def 2;
then A127:
L c= product b1
by A124, A125, CARD_3:27;
then
(product b2) /\ (product k) = K
by A3, A122, RELAT_1:123, XBOOLE_1:28;
then
2
c= card ((product b2) /\ (product k))
by PENCIL_1:def 6;
then A128:
indx k = (permutation_of_indices f) . (indx b1)
by A45, PENCIL_1:26;
A129:
dom k = I
by PARTFUN1:def 2;
M .: S = k . (indx k)
proof
thus
M .: S c= k . (indx k)
XBOOLE_0:def 10 k . (indx k) c= M .: Sproof
let o be
object ;
TARSKI:def 3 ( not o in M .: S or o in k . (indx k) )
A130:
dom b1 = I
by PARTFUN1:def 2;
assume
o in M .: S
;
o in k . (indx k)
then consider u being
object such that A131:
u in dom M
and A132:
u in S
and A133:
o = M . u
by FUNCT_1:def 6;
reconsider u =
u as
Point of
(A . (indx b1)) by A131;
consider p0 being
ManySortedSet of
I such that A134:
p0 in product b1
and A135:
{(p0 +* ((indx b1),u))} = product (b1 +* ((indx b1),{u}))
by Th18;
reconsider p =
p0 +* (
(indx b1),
u) as
Point of
(Segre_Product A) by A2, A134, PENCIL_1:25;
reconsider q =
f . p as
ManySortedSet of
I by PENCIL_1:14;
Im (
f,
(p0 +* ((indx b1),u)))
= {(f . p)}
by A38, FUNCT_1:59;
then
q in f .: (product (b1 +* ((indx b1),{u})))
by A135, TARSKI:def 1;
then A136:
M . u = q . ((permutation_of_indices f) . (indx b1))
by A37;
A137:
dom p0 = I
by PARTFUN1:def 2;
(
dom (p0 +* ((indx b1),u)) = I &
dom (b1 +* ((indx b1),S)) = I )
by PARTFUN1:def 2;
then
p in L
by A138, CARD_3:9;
then
q in product k
by A38, A122, FUNCT_1:def 6;
hence
o in k . (indx k)
by A129, A128, A133, A136, CARD_3:9;
verum
end;
let o be
object ;
TARSKI:def 3 ( not o in k . (indx k) or o in M .: S )
assume A142:
o in k . (indx k)
;
o in M .: S
k . (indx k) in the
topology of
(A . ((permutation_of_indices f) . (indx b1)))
by A123, A128;
then reconsider u =
o as
Point of
(A . ((permutation_of_indices f) . (indx b1))) by A142;
consider p0 being
ManySortedSet of
I such that A143:
p0 in product k
and
{(p0 +* (((permutation_of_indices f) . (indx b1)),u))} = product (k +* (((permutation_of_indices f) . (indx b1)),{u}))
by A128, Th18;
K in the
topology of
(Segre_Product A)
;
then reconsider p =
p0 +* (
((permutation_of_indices f) . (indx b1)),
u) as
Point of
(Segre_Product A) by A122, A143, PENCIL_1:25;
reconsider q =
(f ") . p as
ManySortedSet of
I by PENCIL_1:14;
A144:
dom k = I
by PARTFUN1:def 2;
A145:
dom p0 = I
by PARTFUN1:def 2;
A148:
p = f . q
by A70, A5, A71, FUNCT_1:35;
dom (p0 +* (((permutation_of_indices f) . (indx b1)),u)) = I
by PARTFUN1:def 2;
then
p in f .: L
by A122, A144, A146, CARD_3:9;
then
ex
qq being
object st
(
qq in dom f &
qq in L &
p = f . qq )
by FUNCT_1:def 6;
then A149:
q in L
by A38, A5, A148, FUNCT_1:def 4;
dom (b1 +* ((indx b1),S)) = I
by PARTFUN1:def 2;
then
q . (indx b1) in (b1 +* ((indx b1),S)) . (indx b1)
by A149, CARD_3:9;
then A150:
q . (indx b1) in S
by A124, FUNCT_7:31;
then reconsider qi =
q . (indx b1) as
Point of
(A . (indx b1)) ;
consider q0 being
ManySortedSet of
I such that A151:
q0 in product b1
and A152:
{(q0 +* ((indx b1),qi))} = product (b1 +* ((indx b1),{qi}))
by Th18;
A153:
dom q0 = I
by PARTFUN1:def 2;
q0 +* (
(indx b1),
qi)
= q
by A154;
then
Im (
f,
(q0 +* ((indx b1),qi)))
= {(f . q)}
by A38, FUNCT_1:59;
then
p in f .: (product (b1 +* ((indx b1),{qi})))
by A148, A152, TARSKI:def 1;
then
M . (q . (indx b1)) = (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . ((permutation_of_indices f) . (indx b1))
by A37;
then
M . (q . (indx b1)) = o
by A145, FUNCT_7:31;
hence
o in M .: S
by A37, A150, FUNCT_1:def 6;
verum
end;
hence
M .: S0 is
open
by A123, A128, PRE_TOPC:def 2;
verum
end;
take
M
; ( M is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) ) )
A156:
M is onto
by A86, FUNCT_2:def 3;
then
M " is bijective
by A46, PENCIL_2:12;
hence
M is isomorphic
by A46, A156, A121, A88, PENCIL_2:def 4; for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1))
let a be ManySortedSet of I; ( a is Point of (Segre_Product A) & a in product b1 implies for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) )
assume that
A157:
a is Point of (Segre_Product A)
and
A158:
a in product b1
; for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1))
dom (Carrier A) = I
by PARTFUN1:def 2;
then
a . (indx b1) in (Carrier A) . (indx b1)
by A7, A157, CARD_3:9;
then
a . (indx b1) in [#] (A . (indx b1))
by Th7;
then reconsider ai = a . (indx b1) as Point of (A . (indx b1)) ;
A159:
dom b1 = I
by PARTFUN1:def 2;
( dom a = I & dom (b1 +* ((indx b1),{ai})) = I )
by PARTFUN1:def 2;
then A163:
a in product (b1 +* ((indx b1),{ai}))
by A160, CARD_3:9;
let b be ManySortedSet of I; ( b = f . a implies b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) )
assume
b = f . a
; b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1))
then
b in f .: (product (b1 +* ((indx b1),{ai})))
by A38, A157, A163, FUNCT_1:def 6;
hence
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1))
by A37; verum