reconsider B1 = product b1 as Segre-Coset of A by A2;
set s = permutation_of_indices f;
set i = indx b1;
defpred S1[ set , set ] 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 set st x in the carrier of (A . (indx b1)) holds
ex y being set st S1[x,y]
proof
let x be
set ;
( x in the carrier of (A . (indx b1)) implies ex y being set st S1[x,y] )
consider bb being
set 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
set 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:
dom (Carrier A) = I
by PARTFUN1:def 2;
A13:
{(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
set ;
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 A19:
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 A19, A14, CARD_3:9;
verum
end;
let o be
set ;
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 A20:
u = o
and A21:
dom u = dom (b1 +* ((indx b1),{x}))
and A22:
for
z being
set st
z in dom (b1 +* ((indx b1),{x})) holds
u . z in (b1 +* ((indx b1),{x})) . z
by CARD_3:def 5;
A23:
now let z be
set ;
( z in dom u implies u . b1 = (bb +* ((indx b1),x)) . b1 )assume A24:
z in dom u
;
u . b1 = (bb +* ((indx b1),x)) . b1then A25:
z in I
by A21, PARTFUN1:def 2;
reconsider zz =
z as
Element of
I by A21, A24, PARTFUN1:def 2;
A26:
u . z in (b1 +* ((indx b1),{x})) . z
by A21, A22, A24;
per cases
( zz = indx b1 or zz <> indx b1 )
;
suppose A28:
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
set such that A29:
b1 . z = {o}
by ZFMISC_1:131;
u . z in b1 . z
by A26, A28, FUNCT_7:32;
then A30:
u . z = o
by A29, TARSKI:def 1;
(bb +* ((indx b1),x)) . z = bb . z
by A28, FUNCT_7:32;
then
(bb +* ((indx b1),x)) . z in {o}
by A10, A11, A25, A29;
hence
u . z = (bb +* ((indx b1),x)) . z
by A30, TARSKI:def 1;
verum end; end;
dom u =
I
by A21, PARTFUN1:def 2
.=
dom (bb +* ((indx b1),x))
by PARTFUN1:def 2
;
then
u = bb +* (
(indx b1),
x)
by A23, FUNCT_1:2;
hence
o in {(bb +* ((indx b1),x))}
by A20, TARSKI:def 1;
verum
end;
assume A31:
x in the
carrier of
(A . (indx b1))
;
ex y being set 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, A32, 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 A37:
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 A13, A37, TARSKI:def 1;
verum
end;
consider M being Function such that
A38:
( dom M = the carrier of (A . (indx b1)) & ( for x being set st x in the carrier of (A . (indx b1)) holds
S1[x,M . x] ) )
from CLASSES1:sch 1(A8);
A39:
dom f = the carrier of (Segre_Product A)
by FUNCT_2:def 1;
then
B1 c= f " B2
by FUNCT_1:76;
then A40:
f " B2 = B1
by A6, XBOOLE_0:def 10;
rng M c= the carrier of (A . ((permutation_of_indices f) . (indx b1)))
proof
let x be
set ;
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
set such that A41:
o in dom M
and A42:
x = M . o
by FUNCT_1:def 3;
reconsider o =
o as
Point of
(A . (indx b1)) by A38, A41;
consider p being
ManySortedSet of
I such that A43:
p in product b1
and A44:
{(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, A43, PENCIL_1:25;
reconsider J =
f . pio as
ManySortedSet of
I by PENCIL_1:14;
Im (
f,
(p +* ((indx b1),o)))
= {(f . pio)}
by A39, FUNCT_1:59;
then A45:
J in f .: (product (b1 +* ((indx b1),{o})))
by A44, 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 A38, A42, A45;
verum
end;
then reconsider M = M as Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) by A38, FUNCT_2:def 1, RELSET_1:4;
set m = M;
A46:
indx b2 = (permutation_of_indices f) . (indx b1)
by A1, A3, Def3;
A47:
M is one-to-one
proof
let x1,
x2 be
set ;
FUNCT_1:def 4 ( not x1 in proj1 M or not x2 in proj1 M or not M . x1 = M . x2 or x1 = x2 )
assume that A48:
(
x1 in dom M &
x2 in dom M )
and A49:
M . x1 = M . x2
;
x1 = x2
reconsider o1 =
x1,
o2 =
x2 as
Point of
(A . (indx b1)) by A48;
consider p1 being
ManySortedSet of
I such that A50:
p1 in product b1
and A51:
{(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, A50, PENCIL_1:25;
reconsider J1 =
f . p1io as
ManySortedSet of
I by PENCIL_1:14;
consider p2 being
ManySortedSet of
I such that A52:
p2 in product b1
and A53:
{(p2 +* ((indx b1),o2))} = product (b1 +* ((indx b1),{o2}))
by Th18;
A54:
dom b1 = I
by PARTFUN1:def 2;
A55:
dom p1 = I
by PARTFUN1:def 2;
dom (p1 +* ((indx b1),o1)) = I
by PARTFUN1:def 2;
then
p1io in product b1
by A54, A56, CARD_3:9;
then A59:
J1 in B2
by A39, FUNCT_1:def 6;
reconsider p2io =
p2 +* (
(indx b1),
o2) as
Point of
(Segre_Product A) by A2, A52, PENCIL_1:25;
reconsider J2 =
f . p2io as
ManySortedSet of
I by PENCIL_1:14;
Im (
f,
(p2 +* ((indx b1),o2)))
= {(f . p2io)}
by A39, FUNCT_1:59;
then
J2 in f .: (product (b1 +* ((indx b1),{o2})))
by A53, TARSKI:def 1;
then A60:
M . o2 = J2 . ((permutation_of_indices f) . (indx b1))
by A38;
dom p1 = I
by PARTFUN1:def 2;
then A61:
(p1 +* ((indx b1),o1)) . (indx b1) = o1
by FUNCT_7:31;
A62:
dom b1 = I
by PARTFUN1:def 2;
A63:
dom p2 = I
by PARTFUN1:def 2;
dom (p2 +* ((indx b1),o2)) = I
by PARTFUN1:def 2;
then
p2io in product b1
by A62, A64, CARD_3:9;
then A67:
J2 in B2
by A39, FUNCT_1:def 6;
Im (
f,
(p1 +* ((indx b1),o1)))
= {(f . p1io)}
by A39, FUNCT_1:59;
then A68:
J1 in f .: (product (b1 +* ((indx b1),{o1})))
by A51, TARSKI:def 1;
A69:
now let o be
set ;
( 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 A70:
(p2 +* ((indx b1),o2)) . (indx b1) = o2
by FUNCT_7:31;
(
dom J1 = I &
dom J2 = I )
by PARTFUN1:def 2;
then
J1 = J2
by A69, FUNCT_1:2;
hence
x1 = x2
by A39, A5, A61, A70, FUNCT_1:def 4;
verum
end;
f is bijective
by PENCIL_2:def 4;
then A71:
rng f = the carrier of (Segre_Product A)
by FUNCT_2:def 3;
A72:
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
set ;
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 A73:
p0 in product b2
and
{(p0 +* ((indx b2),x1))} = product (b2 +* ((indx b2),{x1}))
by A46, Th18;
reconsider p =
p0 +* (
(indx b2),
x1) as
Point of
(Segre_Product A) by A3, A46, A73, PENCIL_1:25;
reconsider p1 =
p as
ManySortedSet of
I ;
reconsider q =
(f ") . p as
ManySortedSet of
I by PENCIL_1:14;
A74:
p = f . ((f ") . p)
by A71, A5, A72, FUNCT_1:35;
A75:
dom b1 = I
by PARTFUN1:def 2;
A76:
now let o be
set ;
( 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 A77:
(b1 +* ((indx b1),{(q . (indx b1))})) . l = b1 . l
by FUNCT_7:32;
A78:
dom b2 = I
by PARTFUN1:def 2;
A79:
dom p0 = I
by PARTFUN1:def 2;
A80:
now let o be
set ;
( o in I implies p1 . b1 in b2 . b1 )assume A81:
o in I
;
p1 . b1 in b2 . b1 end;
dom p1 = I
by PARTFUN1:def 2;
then
p in product b2
by A78, A80, CARD_3:9;
then consider q0 being
set such that A83:
q0 in dom f
and A84:
q0 in B1
and A85:
p = f . q0
by A3, FUNCT_1:def 6;
q = q0
by A39, A5, A74, A83, A85, FUNCT_1:def 4;
hence
q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o
by A75, A77, A84, CARD_3:9;
verum 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 A86:
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 A76, CARD_3:9;
then
p0 +* (
(indx b2),
x1)
in f .: (product (b1 +* ((indx b1),{(q . (indx b1))})))
by A39, A74, FUNCT_1:def 6;
then
(
dom p0 = I &
M . (q . (indx b1)) = (p0 +* ((indx b2),x1)) . ((permutation_of_indices f) . (indx b1)) )
by A38, A86, PARTFUN1:def 2;
then
(
dom M = the
carrier of
(A . (indx b1)) &
M . (q . (indx b1)) = x )
by A46, FUNCT_2:def 1, FUNCT_7:31;
hence
x in rng M
by A86, FUNCT_1:3;
verum
end;
then A87:
rng M = the carrier of (A . ((permutation_of_indices f) . (indx b1)))
by XBOOLE_0:def 10;
then
M is onto
by FUNCT_2:def 3;
then A88:
M " = M "
by A47, TOPS_2:def 4;
A89:
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 A46, 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 A90:
K = product k
and A91:
k . (indx k) is
Block of
(A . (indx k))
by PENCIL_1:24;
A92:
dom b2 = I
by PARTFUN1:def 2;
dom (b2 +* ((indx b2),S)) = I
by PARTFUN1:def 2;
then
L c= product b2
by A92, A93, CARD_3:27;
then
(product b1) /\ (product k) = K
by A3, A40, A90, RELAT_1:143, XBOOLE_1:28;
then A95:
2
c= card ((product b1) /\ (product k))
by PENCIL_1:def 6;
then A96:
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
set ;
TARSKI:def 3 ( not o in M " S or o in k . (indx k) )
A97:
dom b2 = I
by PARTFUN1:def 2;
assume A98:
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 A99:
p in product b1
and A100:
{(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, A99, PENCIL_1:25;
reconsider fq =
f . q as
ManySortedSet of
I by PENCIL_1:14;
Im (
f,
(p +* ((indx b1),u)))
= {(f . q)}
by A39, FUNCT_1:59;
then A101:
fq in f .: (product (b1 +* ((indx b1),{u})))
by A100, TARSKI:def 1;
product (b1 +* ((indx b1),{u})) c= product b1
then A109:
f .: (product (b1 +* ((indx b1),{u}))) c= product b2
by A3, RELAT_1:123;
M . o in S
by A98, FUNCT_1:def 7;
then A110:
fq . ((permutation_of_indices f) . (indx b1)) in S
by A38, A101;
(
dom fq = I &
dom (b2 +* ((indx b2),S)) = I )
by PARTFUN1:def 2;
then
fq in L
by A111, CARD_3:9;
then
(
dom k = I &
q in K )
by A39, FUNCT_1:def 7, PARTFUN1:def 2;
then
(
dom p = I &
(p +* ((indx b1),u)) . (indx b1) in k . (indx b1) )
by A90, CARD_3:9, PARTFUN1:def 2;
hence
o in k . (indx k)
by A96, FUNCT_7:31;
verum
end;
let o be
set ;
TARSKI:def 3 ( not o in k . (indx k) or o in M " S )
assume A113:
o in k . (indx k)
;
o in M " S
k . (indx k) in the
topology of
(A . (indx b1))
by A91, A96;
then reconsider u =
o as
Point of
(A . (indx b1)) by A113;
consider p0 being
ManySortedSet of
I such that A114:
p0 in product b1
and A115:
{(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, A114, PENCIL_1:25;
reconsider fp =
f . p as
ManySortedSet of
I by PENCIL_1:14;
A116:
dom b1 = I
by PARTFUN1:def 2;
A117:
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 A90, A118, 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 A121:
fp . ((permutation_of_indices f) . (indx b1)) in S
by A46, FUNCT_7:31;
Im (
f,
(p0 +* ((indx b1),u)))
= {(f . p)}
by A39, FUNCT_1:59;
then
fp in f .: (product (b1 +* ((indx b1),{u})))
by A115, TARSKI:def 1;
then
M . u = fp . ((permutation_of_indices f) . (indx b1))
by A38;
hence
o in M " S
by A38, A121, FUNCT_1:def 7;
verum
end;
then
(M ") .: S is
Block of
(A . (indx b1))
by A47, A88, A91, A96, FUNCT_1:85;
hence
(M ") .: S0 is
open
by PRE_TOPC:def 2;
verum
end;
A122:
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 A123:
K = product k
and A124:
k . (indx k) is
Block of
(A . (indx k))
by PENCIL_1:24;
A125:
dom b1 = I
by PARTFUN1:def 2;
dom (b1 +* ((indx b1),S)) = I
by PARTFUN1:def 2;
then A128:
L c= product b1
by A125, A126, CARD_3:27;
then
(product b2) /\ (product k) = K
by A3, A123, RELAT_1:123, XBOOLE_1:28;
then
2
c= card ((product b2) /\ (product k))
by PENCIL_1:def 6;
then A129:
indx k = (permutation_of_indices f) . (indx b1)
by A46, PENCIL_1:26;
A130:
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
set ;
TARSKI:def 3 ( not o in M .: S or o in k . (indx k) )
A131:
dom b1 = I
by PARTFUN1:def 2;
assume
o in M .: S
;
o in k . (indx k)
then consider u being
set such that A132:
u in dom M
and A133:
u in S
and A134:
o = M . u
by FUNCT_1:def 6;
reconsider u =
u as
Point of
(A . (indx b1)) by A132;
consider p0 being
ManySortedSet of
I such that A135:
p0 in product b1
and A136:
{(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, A135, PENCIL_1:25;
reconsider q =
f . p as
ManySortedSet of
I by PENCIL_1:14;
Im (
f,
(p0 +* ((indx b1),u)))
= {(f . p)}
by A39, FUNCT_1:59;
then
q in f .: (product (b1 +* ((indx b1),{u})))
by A136, TARSKI:def 1;
then A137:
M . u = q . ((permutation_of_indices f) . (indx b1))
by A38;
A138:
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 A139, CARD_3:9;
then
q in product k
by A39, A123, FUNCT_1:def 6;
hence
o in k . (indx k)
by A130, A129, A134, A137, CARD_3:9;
verum
end;
let o be
set ;
TARSKI:def 3 ( not o in k . (indx k) or o in M .: S )
assume A143:
o in k . (indx k)
;
o in M .: S
k . (indx k) in the
topology of
(A . ((permutation_of_indices f) . (indx b1)))
by A124, A129;
then reconsider u =
o as
Point of
(A . ((permutation_of_indices f) . (indx b1))) by A143;
consider p0 being
ManySortedSet of
I such that A144:
p0 in product k
and
{(p0 +* (((permutation_of_indices f) . (indx b1)),u))} = product (k +* (((permutation_of_indices f) . (indx b1)),{u}))
by A129, 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 A123, A144, PENCIL_1:25;
reconsider q =
(f ") . p as
ManySortedSet of
I by PENCIL_1:14;
A145:
dom k = I
by PARTFUN1:def 2;
A146:
dom p0 = I
by PARTFUN1:def 2;
A149:
p = f . q
by A71, A5, A72, FUNCT_1:35;
dom (p0 +* (((permutation_of_indices f) . (indx b1)),u)) = I
by PARTFUN1:def 2;
then
p in f .: L
by A123, A145, A147, CARD_3:9;
then
ex
qq being
set st
(
qq in dom f &
qq in L &
p = f . qq )
by FUNCT_1:def 6;
then A150:
q in L
by A39, A5, A149, 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 A150, CARD_3:9;
then A151:
q . (indx b1) in S
by A125, FUNCT_7:31;
then reconsider qi =
q . (indx b1) as
Point of
(A . (indx b1)) ;
consider q0 being
ManySortedSet of
I such that A152:
q0 in product b1
and A153:
{(q0 +* ((indx b1),qi))} = product (b1 +* ((indx b1),{qi}))
by Th18;
A154:
dom q0 = I
by PARTFUN1:def 2;
(
dom q = I &
dom (q0 +* ((indx b1),qi)) = I )
by PARTFUN1:def 2;
then
q0 +* (
(indx b1),
qi)
= q
by A155, FUNCT_1:2;
then
Im (
f,
(q0 +* ((indx b1),qi)))
= {(f . q)}
by A39, FUNCT_1:59;
then
p in f .: (product (b1 +* ((indx b1),{qi})))
by A149, A153, TARSKI:def 1;
then
M . (q . (indx b1)) = (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . ((permutation_of_indices f) . (indx b1))
by A38;
then
M . (q . (indx b1)) = o
by A146, FUNCT_7:31;
hence
o in M .: S
by A38, A151, FUNCT_1:def 6;
verum
end;
hence
M .: S0 is
open
by A124, A129, 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)) ) )
A157:
M is onto
by A87, FUNCT_2:def 3;
then
M " is bijective
by A47, PENCIL_2:12;
hence
M is isomorphic
by A47, A157, A122, A89, 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
A158:
a is Point of (Segre_Product A)
and
A159:
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, A158, 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)) ;
A160:
dom b1 = I
by PARTFUN1:def 2;
( dom a = I & dom (b1 +* ((indx b1),{ai})) = I )
by PARTFUN1:def 2;
then A164:
a in product (b1 +* ((indx b1),{ai}))
by A161, 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 A39, A158, A164, FUNCT_1:def 6;
hence
b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1))
by A38; verum