reconsider B1 = product b1 as Segre-Coset of A by B2;
set s = permutation_of_indices f;
set i = indx b1;
defpred S₁[ 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 B1, PENCIL_2:24;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A1: product b2 = B2 and
A2: b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def 2;
set j = indx b2;
A3: f is bijective by PENCIL_2:def 4;
then A4: f " B2 c= B1 by FUNCT_1:82;
A5: Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def 23;
A6: for x being set st x in the carrier of (A . (indx b1)) holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis:
consider bb being set such that
A7: bb in B1 by XBOOLE_0:def 1;
A8: 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 A7, CARD_3:def 5;
A9: dom b1 = I by PARTFUN1:def 2;
then reconsider bb = bb as ManySortedSet of I by A8, PARTFUN1:def 2, RELAT_1:def 18;
set bbx = bb +* ((indx b1),x);
A10: {(bb +* ((indx b1),x))} = product (b1 +* ((indx b1),{x}))

proof

thus {(bb +* ((indx b1),x))} c= product (b1 +* ((indx b1),{x})) :: according to XBOOLE_0:def 10 :: thesis:

proof

A11: now :: thesis:

let z be set ; :: thesis:
assume z in dom (b1 +* ((indx b1),{x})) ; :: thesis:
then A12: z in I ;
then A13: z in dom bb by PARTFUN1:def 2;

per cases ;

suppose A14: z = indx b1 ; :: thesis:

then (bb +* ((indx b1),x)) . z = x by A13, FUNCT_7:31;
then (bb +* ((indx b1),x)) . z in {x} by TARSKI:def 1;
hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A9, A14, FUNCT_7:31; :: thesis:

end;

suppose A15: z <> indx b1 ; :: thesis:

then (bb +* ((indx b1),x)) . z = bb . z by FUNCT_7:32;
then (bb +* ((indx b1),x)) . z in b1 . z by A7, A9, A12, CARD_3:9;
hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A15, FUNCT_7:32; :: thesis:

end;

let o be set ; :: according to TARSKI:def 3 :: thesis:
assume o in {(bb +* ((indx b1),x))} ; :: thesis:
then A16: 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 A16, A11, CARD_3:9; :: thesis:

end;

let o be set ; :: according to TARSKI:def 3 :: thesis:
assume o in product (b1 +* ((indx b1),{x})) ; :: thesis:
then consider u being Function such that
A17: u = o and
A18: dom u = dom (b1 +* ((indx b1),{x})) and
A19: 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;

A20: now :: thesis:

let z be set ; :: thesis:
assume A21: z in dom u ; :: thesis:
then A22: z in I by A18;
reconsider zz = z as Element of I by A18, A21;
A23: u . z in (b1 +* ((indx b1),{x})) . z by A18, A19, A21;

per cases ;

suppose A24: zz = indx b1 ; :: thesis:

then u . z in {x} by A9, A23, FUNCT_7:31;
then u . z = x by TARSKI:def 1;
hence u . z = (bb +* ((indx b1),x)) . z by A8, A9, A24, FUNCT_7:31; :: thesis:

end;

suppose A25: zz <> indx b1 ; :: thesis:

then ( 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
A26: b1 . z = {o} by ZFMISC_1:131;
u . z in b1 . z by A23, A25, FUNCT_7:32;
then A27: u . z = o by A26, TARSKI:def 1;
(bb +* ((indx b1),x)) . z = bb . z by A25, FUNCT_7:32;
then (bb +* ((indx b1),x)) . z in {o} by A8, A9, A22, A26;
hence u . z = (bb +* ((indx b1),x)) . z by A27, TARSKI:def 1; :: thesis:

end;

dom u = I by A18, PARTFUN1:def 2
.= dom (bb +* ((indx b1),x)) by PARTFUN1:def 2 ;
then u = bb +* ((indx b1),x) by A20, FUNCT_1:2;
hence o in {(bb +* ((indx b1),x))} by A17, TARSKI:def 1; :: thesis:

end;

assume A28: x in the carrier of (A . (indx b1)) ; :: thesis:

A29: now :: thesis:

let o be set ; :: thesis:
assume A30: o in dom (Carrier A) ; :: thesis:
then reconsider u = o as Element of I ;

per cases ;

suppose A31: u = indx b1 ; :: thesis:

then (bb +* ((indx b1),x)) . u in [#] (A . (indx b1)) by A28, A8, A9, FUNCT_7:31;
hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A31, Th7; :: thesis:

end;

suppose A32: u <> indx b1 ; :: thesis:

b1 c= Carrier A by PBOOLE:def 18;
then A33: b1 . o c= (Carrier A) . o by A30, PBOOLE:def 2;
(bb +* ((indx b1),x)) . u = bb . u by A32, FUNCT_7:32;
then (bb +* ((indx b1),x)) . u in b1 . u by A7, A9, CARD_3:9;
hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A33; :: thesis:

end;

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 A5, A29, CARD_3:9;
reconsider fbbx = f . bbx1 as ManySortedSet of I by PENCIL_1:14;
take fbbx . ((permutation_of_indices f) . (indx b1)) ; :: thesis:
dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;
then bbx1 in dom f ;
then A34: Im (f,(bb +* ((indx b1),x))) = {(f . (bb +* ((indx b1),x)))} by FUNCT_1:59;
let J be ManySortedSet of I; :: thesis:
assume J in f .: (product (b1 +* ((indx b1),{x}))) ; :: thesis:
hence fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1)) by A10, A34, TARSKI:def 1; :: thesis:

end;

consider M being Function such that
A35: ( dom M = the carrier of (A . (indx b1)) & ( for x being set st x in the carrier of (A . (indx b1)) holds
S₁[x,M . x] ) ) from CLASSES1:sch 1(A6);
A36: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;
then B1 c= f " B2 by FUNCT_1:76;
then A37: f " B2 = B1 by A4, XBOOLE_0:def 10;
rng M c= the carrier of (A . ((permutation_of_indices f) . (indx b1)))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng M ; :: thesis:
then consider o being set such that
A38: o in dom M and
A39: x = M . o by FUNCT_1:def 3;
reconsider o = o as Point of (A . (indx b1)) by A35, A38;
consider p being ManySortedSet of I such that
A40: p in product b1 and
A41: {(p +* ((indx b1),o))} = product (b1 +* ((indx b1),{o})) by Th18;
reconsider pio = p +* ((indx b1),o) as Point of (Segre_Product A) by B2, A40, PENCIL_1:25;
reconsider J = f . pio as ManySortedSet of I by PENCIL_1:14;
Im (f,(p +* ((indx b1),o))) = {(f . pio)} by A36, FUNCT_1:59;
then A42: J in f .: (product (b1 +* ((indx b1),{o}))) by A41, 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 A5, 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 A35, A39, A42; :: thesis:

end;

then reconsider M = M as Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) by A35, FUNCT_2:def 1, RELSET_1:4;
set m = M;
A43: indx b2 = (permutation_of_indices f) . (indx b1) by B1, A1, Def3;
A44: M is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A45: ( x1 in dom M & x2 in dom M ) and
A46: M . x1 = M . x2 ; :: thesis:
reconsider o1 = x1, o2 = x2 as Point of (A . (indx b1)) by A45;
consider p1 being ManySortedSet of I such that
A47: p1 in product b1 and
A48: {(p1 +* ((indx b1),o1))} = product (b1 +* ((indx b1),{o1})) by Th18;
reconsider p1io = p1 +* ((indx b1),o1) as Point of (Segre_Product A) by B2, A47, PENCIL_1:25;
reconsider J1 = f . p1io as ManySortedSet of I by PENCIL_1:14;
consider p2 being ManySortedSet of I such that
A49: p2 in product b1 and
A50: {(p2 +* ((indx b1),o2))} = product (b1 +* ((indx b1),{o2})) by Th18;
A51: dom b1 = I by PARTFUN1:def 2;
A52: dom p1 = I by PARTFUN1:def 2;

A53: now :: thesis:

let o be set ; :: thesis:
assume A54: o in I ; :: thesis:

per cases ;

suppose A55: o = indx b1 ; :: thesis:

then (p1 +* ((indx b1),o1)) . o = o1 by A52, FUNCT_7:31;
then (p1 +* ((indx b1),o1)) . o in [#] (A . (indx b1)) ;
hence (p1 +* ((indx b1),o1)) . o in b1 . o by B2, A55, Th10; :: thesis:

end;

suppose o <> indx b1 ; :: thesis:

then (p1 +* ((indx b1),o1)) . o = p1 . o by FUNCT_7:32;
hence (p1 +* ((indx b1),o1)) . o in b1 . o by A47, A51, A54, CARD_3:9; :: thesis:

end;

dom (p1 +* ((indx b1),o1)) = I by PARTFUN1:def 2;
then p1io in product b1 by A51, A53, CARD_3:9;
then A56: J1 in B2 by A36, FUNCT_1:def 6;
reconsider p2io = p2 +* ((indx b1),o2) as Point of (Segre_Product A) by B2, A49, PENCIL_1:25;
reconsider J2 = f . p2io as ManySortedSet of I by PENCIL_1:14;
Im (f,(p2 +* ((indx b1),o2))) = {(f . p2io)} by A36, FUNCT_1:59;
then J2 in f .: (product (b1 +* ((indx b1),{o2}))) by A50, TARSKI:def 1;
then A57: M . o2 = J2 . ((permutation_of_indices f) . (indx b1)) by A35;
dom p1 = I by PARTFUN1:def 2;
then A58: (p1 +* ((indx b1),o1)) . (indx b1) = o1 by FUNCT_7:31;
A59: dom b1 = I by PARTFUN1:def 2;
A60: dom p2 = I by PARTFUN1:def 2;

A61: now :: thesis:

let o be set ; :: thesis:
assume A62: o in I ; :: thesis:

per cases ;

suppose A63: o = indx b1 ; :: thesis:

then (p2 +* ((indx b1),o2)) . o = o2 by A60, FUNCT_7:31;
then (p2 +* ((indx b1),o2)) . o in [#] (A . (indx b1)) ;
hence (p2 +* ((indx b1),o2)) . o in b1 . o by B2, A63, Th10; :: thesis:

end;

suppose o <> indx b1 ; :: thesis:

then (p2 +* ((indx b1),o2)) . o = p2 . o by FUNCT_7:32;
hence (p2 +* ((indx b1),o2)) . o in b1 . o by A49, A59, A62, CARD_3:9; :: thesis:

end;

dom (p2 +* ((indx b1),o2)) = I by PARTFUN1:def 2;
then p2io in product b1 by A59, A61, CARD_3:9;
then A64: J2 in B2 by A36, FUNCT_1:def 6;
Im (f,(p1 +* ((indx b1),o1))) = {(f . p1io)} by A36, FUNCT_1:59;
then A65: J1 in f .: (product (b1 +* ((indx b1),{o1}))) by A48, TARSKI:def 1;

A66: now :: thesis:

let o be set ; :: thesis:
assume o in I ; :: thesis:
then reconsider l = o as Element of I ;

per cases ;

suppose l = indx b2 ; :: thesis:

hence J1 . o = J2 . o by A43, A35, A46, A65, A57; :: thesis:

end;

suppose l <> indx b2 ; :: thesis:

hence J1 . o = J2 . o by A1, A56, A64, PENCIL_1:23; :: thesis:

end;

dom p2 = I by PARTFUN1:def 2;
then A67: (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 A66, FUNCT_1:2;
hence x1 = x2 by A36, A3, A58, A67, FUNCT_1:def 4; :: thesis:

end;

f is bijective by PENCIL_2:def 4;
then A68: rng f = the carrier of (Segre_Product A) by FUNCT_2:def 3;
A69: f " = f " by A3, TOPS_2:def 4;
the carrier of (A . ((permutation_of_indices f) . (indx b1))) c= rng M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ; :: thesis:
then reconsider x1 = x as Point of (A . ((permutation_of_indices f) . (indx b1))) ;
consider p0 being ManySortedSet of I such that
A70: p0 in product b2 and
{(p0 +* ((indx b2),x1))} = product (b2 +* ((indx b2),{x1})) by A43, Th18;
reconsider p = p0 +* ((indx b2),x1) as Point of (Segre_Product A) by A1, A43, A70, PENCIL_1:25;
reconsider p1 = p as ManySortedSet of I ;
reconsider q = (f ") . p as ManySortedSet of I by PENCIL_1:14;
A71: p = f . ((f ") . p) by A68, A3, A69, FUNCT_1:35;
A72: dom b1 = I by PARTFUN1:def 2;

A73: now :: thesis:

let o be set ; :: thesis:
assume o in I ; :: thesis:
then reconsider l = o as Element of I ;

per cases ;

suppose l = indx b1 ; :: thesis:

then (b1 +* ((indx b1),{(q . (indx b1))})) . l = {(q . o)} by A72, FUNCT_7:31;
hence q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o by TARSKI:def 1; :: thesis:

end;

suppose l <> indx b1 ; :: thesis:

then A74: (b1 +* ((indx b1),{(q . (indx b1))})) . l = b1 . l by FUNCT_7:32;
A75: dom b2 = I by PARTFUN1:def 2;
A76: dom p0 = I by PARTFUN1:def 2;

A77: now :: thesis:

let o be set ; :: thesis:
assume A78: o in I ; :: thesis:

per cases ;

suppose A79: o = indx b2 ; :: thesis:

then p1 . o = x1 by A76, FUNCT_7:31;
then p1 . o in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ;
hence p1 . o in b2 . o by B1, A1, A2, A79, Def3; :: thesis:

end;

suppose o <> indx b2 ; :: thesis:

then p1 . o = p0 . o by FUNCT_7:32;
hence p1 . o in b2 . o by A70, A75, A78, CARD_3:9; :: thesis:

end;

dom p1 = I by PARTFUN1:def 2;
then p in product b2 by A75, A77, CARD_3:9;
then consider q0 being set such that
A80: q0 in dom f and
A81: q0 in B1 and
A82: p = f . q0 by A1, FUNCT_1:def 6;
q = q0 by A36, A3, A71, A80, A82, FUNCT_1:def 4;
hence q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o by A72, A74, A81, CARD_3:9; :: thesis:

end;

I = dom (Carrier A) by PARTFUN1:def 2;
then q . (indx b1) in (Carrier A) . (indx b1) by A5, CARD_3:9;
then A83: 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 A73, CARD_3:9;
then p0 +* ((indx b2),x1) in f .: (product (b1 +* ((indx b1),{(q . (indx b1))}))) by A36, A71, FUNCT_1:def 6;
then ( dom p0 = I & M . (q . (indx b1)) = (p0 +* ((indx b2),x1)) . ((permutation_of_indices f) . (indx b1)) ) by A35, A83, PARTFUN1:def 2;
then ( dom M = the carrier of (A . (indx b1)) & M . (q . (indx b1)) = x ) by A43, FUNCT_2:def 1, FUNCT_7:31;
hence x in rng M by A83, FUNCT_1:3; :: thesis:

end;

then A84: 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 A85: M " = M " by A44, TOPS_2:def 4;
A86: M " is open

proof

let S0 be Subset of (A . ((permutation_of_indices f) . (indx b1))); :: according to T_0TOPSP:def 2 :: thesis:
assume S0 is open ; :: thesis:
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 A43, 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
A87: K = product k and
A88: k . (indx k) is Block of (A . (indx k)) by PENCIL_1:24;
A89: dom b2 = I by PARTFUN1:def 2;

A90: now :: thesis:

let x be set ; :: thesis:
assume x in I ; :: thesis:

per cases ;

suppose A91: x = indx b2 ; :: thesis:

then (b2 +* ((indx b2),S)) . x = S by A89, FUNCT_7:31;
then (b2 +* ((indx b2),S)) . x c= the carrier of (A . ((permutation_of_indices f) . (indx b1))) ;
hence (b2 +* ((indx b2),S)) . x c= b2 . x by B1, A1, A2, A91, Def3; :: thesis:

end;

suppose x <> indx b2 ; :: thesis:

hence (b2 +* ((indx b2),S)) . x c= b2 . x by FUNCT_7:32; :: thesis:

end;

dom (b2 +* ((indx b2),S)) = I by PARTFUN1:def 2;
then L c= product b2 by A89, A90, CARD_3:27;
then (product b1) /\ (product k) = K by A1, A37, A87, RELAT_1:143, XBOOLE_1:28;
then A92: 2 c= card ((product b1) /\ (product k)) by PENCIL_1:def 6;
then A93: indx k = indx b1 by PENCIL_1:26;
M " S = k . (indx k)

proof

thus M " S c= k . (indx k) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be set ; :: according to TARSKI:def 3 :: thesis:
A94: dom b2 = I by PARTFUN1:def 2;
assume A95: o in M " S ; :: thesis:
then reconsider u = o as Point of (A . (indx b1)) ;
consider p being ManySortedSet of I such that
A96: p in product b1 and
A97: {(p +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18;
reconsider q = p +* ((indx b1),u) as Point of (Segre_Product A) by B2, A96, PENCIL_1:25;
reconsider fq = f . q as ManySortedSet of I by PENCIL_1:14;
Im (f,(p +* ((indx b1),u))) = {(f . q)} by A36, FUNCT_1:59;
then A98: fq in f .: (product (b1 +* ((indx b1),{u}))) by A97, TARSKI:def 1;
product (b1 +* ((indx b1),{u})) c= product b1

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
A99: dom b1 = I by PARTFUN1:def 2;
assume a in product (b1 +* ((indx b1),{u})) ; :: thesis:
then consider g being Function such that
A100: a = g and
A101: dom g = dom (b1 +* ((indx b1),{u})) and
A102: for o being set st o in dom (b1 +* ((indx b1),{u})) holds
g . o in (b1 +* ((indx b1),{u})) . o by CARD_3:def 5;
A103: dom g = I by A101, PARTFUN1:def 2;

now :: thesis:

let o be set ; :: thesis:
assume o in I ; :: thesis:
then A104: g . o in (b1 +* ((indx b1),{u})) . o by A101, A102, A103;

per cases ;

suppose A105: o = indx b1 ; :: thesis:

then g . o in {u} by A99, A104, FUNCT_7:31;
then g . o in [#] (A . (indx b1)) ;
hence g . o in b1 . o by B2, A105, Th10; :: thesis:

end;

suppose o <> indx b1 ; :: thesis:

hence g . o in b1 . o by A104, FUNCT_7:32; :: thesis:

end;

hence a in product b1 by A100, A103, A99, CARD_3:9; :: thesis:

end;

then A106: f .: (product (b1 +* ((indx b1),{u}))) c= product b2 by A1, RELAT_1:123;
M . o in S by A95, FUNCT_1:def 7;
then A107: fq . ((permutation_of_indices f) . (indx b1)) in S by A35, A98;

A108: now :: thesis:

let o be set ; :: thesis:
assume A109: o in I ; :: thesis:

per cases ;

suppose o = indx b2 ; :: thesis:

hence fq . o in (b2 +* ((indx b2),S)) . o by A43, A107, A94, FUNCT_7:31; :: thesis:

end;

suppose o <> indx b2 ; :: thesis:

then (b2 +* ((indx b2),S)) . o = b2 . o by FUNCT_7:32;
hence fq . o in (b2 +* ((indx b2),S)) . o by A98, A106, A94, A109, CARD_3:9; :: thesis:

end;

( dom fq = I & dom (b2 +* ((indx b2),S)) = I ) by PARTFUN1:def 2;
then fq in L by A108, CARD_3:9;
then ( dom k = I & q in K ) by A36, FUNCT_1:def 7, PARTFUN1:def 2;
then ( dom p = I & (p +* ((indx b1),u)) . (indx b1) in k . (indx b1) ) by A87, CARD_3:9, PARTFUN1:def 2;
hence o in k . (indx k) by A93, FUNCT_7:31; :: thesis:

end;

let o be set ; :: according to TARSKI:def 3 :: thesis:
assume A110: o in k . (indx k) ; :: thesis:
k . (indx k) in the topology of (A . (indx b1)) by A88, A93;
then reconsider u = o as Point of (A . (indx b1)) by A110;
consider p0 being ManySortedSet of I such that
A111: p0 in product b1 and
A112: {(p0 +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18;
reconsider p = p0 +* ((indx b1),u) as Point of (Segre_Product A) by B2, A111, PENCIL_1:25;
reconsider fp = f . p as ManySortedSet of I by PENCIL_1:14;
A113: dom b1 = I by PARTFUN1:def 2;
A114: dom p0 = I by PARTFUN1:def 2;

A115: now :: thesis:

let a be set ; :: thesis:
assume A116: a in I ; :: thesis:

per cases ;

suppose a = indx b1 ; :: thesis:

hence (p0 +* ((indx b1),u)) . a in k . a by A93, A110, A114, FUNCT_7:31; :: thesis:

end;

suppose A117: a <> indx b1 ; :: thesis:

then (p0 +* ((indx b1),u)) . a = p0 . a by FUNCT_7:32;
then (p0 +* ((indx b1),u)) . a in b1 . a by A111, A113, A116, CARD_3:9;
hence (p0 +* ((indx b1),u)) . a in k . a by A92, A117, PENCIL_1:26; :: thesis:

end;

( dom (p0 +* ((indx b1),u)) = I & dom k = I ) by PARTFUN1:def 2;
then p in K by A87, A115, 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 A118: fp . ((permutation_of_indices f) . (indx b1)) in S by A43, FUNCT_7:31;
Im (f,(p0 +* ((indx b1),u))) = {(f . p)} by A36, FUNCT_1:59;
then fp in f .: (product (b1 +* ((indx b1),{u}))) by A112, TARSKI:def 1;
then M . u = fp . ((permutation_of_indices f) . (indx b1)) by A35;
hence o in M " S by A35, A118, FUNCT_1:def 7; :: thesis:

end;

then (M ") .: S is Block of (A . (indx b1)) by A44, A85, A88, A93, FUNCT_1:85;
hence (M ") .: S0 is open by PRE_TOPC:def 2; :: thesis:

end;

A119: M is open

proof

let S0 be Subset of (A . (indx b1)); :: according to T_0TOPSP:def 2 :: thesis:
assume S0 is open ; :: thesis:
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
A120: K = product k and
A121: k . (indx k) is Block of (A . (indx k)) by PENCIL_1:24;
A122: dom b1 = I by PARTFUN1:def 2;

A123: now :: thesis:

let x be set ; :: thesis:
assume x in I ; :: thesis:

per cases ;

suppose A124: x = indx b1 ; :: thesis:

then (b1 +* ((indx b1),S)) . x = S by A122, FUNCT_7:31;
then (b1 +* ((indx b1),S)) . x c= [#] (A . (indx b1)) ;
hence (b1 +* ((indx b1),S)) . x c= b1 . x by B2, A124, Th10; :: thesis:

end;

suppose x <> indx b1 ; :: thesis:

hence (b1 +* ((indx b1),S)) . x c= b1 . x by FUNCT_7:32; :: thesis:

end;

dom (b1 +* ((indx b1),S)) = I by PARTFUN1:def 2;
then A125: L c= product b1 by A122, A123, CARD_3:27;
then (product b2) /\ (product k) = K by A1, A120, RELAT_1:123, XBOOLE_1:28;
then 2 c= card ((product b2) /\ (product k)) by PENCIL_1:def 6;
then A126: indx k = (permutation_of_indices f) . (indx b1) by A43, PENCIL_1:26;
A127: dom k = I by PARTFUN1:def 2;
M .: S = k . (indx k)

proof

thus M .: S c= k . (indx k) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be set ; :: according to TARSKI:def 3 :: thesis:
A128: dom b1 = I by PARTFUN1:def 2;
assume o in M .: S ; :: thesis:
then consider u being set such that
A129: u in dom M and
A130: u in S and
A131: o = M . u by FUNCT_1:def 6;
reconsider u = u as Point of (A . (indx b1)) by A129;
consider p0 being ManySortedSet of I such that
A132: p0 in product b1 and
A133: {(p0 +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18;
reconsider p = p0 +* ((indx b1),u) as Point of (Segre_Product A) by B2, A132, PENCIL_1:25;
reconsider q = f . p as ManySortedSet of I by PENCIL_1:14;
Im (f,(p0 +* ((indx b1),u))) = {(f . p)} by A36, FUNCT_1:59;
then q in f .: (product (b1 +* ((indx b1),{u}))) by A133, TARSKI:def 1;
then A134: M . u = q . ((permutation_of_indices f) . (indx b1)) by A35;
A135: dom p0 = I by PARTFUN1:def 2;

A136: now :: thesis:

let a be set ; :: thesis:
assume A137: a in I ; :: thesis:

per cases ;

suppose A138: a = indx b1 ; :: thesis:

then (p0 +* ((indx b1),u)) . a = u by A135, FUNCT_7:31;
hence (p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a by A130, A128, A138, FUNCT_7:31; :: thesis:

end;

suppose A139: a <> indx b1 ; :: thesis:

then (p0 +* ((indx b1),u)) . a = p0 . a by FUNCT_7:32;
then (p0 +* ((indx b1),u)) . a in b1 . a by A132, A128, A137, CARD_3:9;
hence (p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a by A139, FUNCT_7:32; :: thesis:

end;

( dom (p0 +* ((indx b1),u)) = I & dom (b1 +* ((indx b1),S)) = I ) by PARTFUN1:def 2;
then p in L by A136, CARD_3:9;
then q in product k by A36, A120, FUNCT_1:def 6;
hence o in k . (indx k) by A127, A126, A131, A134, CARD_3:9; :: thesis:

end;

let o be set ; :: according to TARSKI:def 3 :: thesis:
assume A140: o in k . (indx k) ; :: thesis:
k . (indx k) in the topology of (A . ((permutation_of_indices f) . (indx b1))) by A121, A126;
then reconsider u = o as Point of (A . ((permutation_of_indices f) . (indx b1))) by A140;
consider p0 being ManySortedSet of I such that
A141: p0 in product k and
{(p0 +* (((permutation_of_indices f) . (indx b1)),u))} = product (k +* (((permutation_of_indices f) . (indx b1)),{u})) by A126, 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 A120, A141, PENCIL_1:25;
reconsider q = (f ") . p as ManySortedSet of I by PENCIL_1:14;
A142: dom k = I by PARTFUN1:def 2;
A143: dom p0 = I by PARTFUN1:def 2;

A144: now :: thesis:

let z be set ; :: thesis:
assume A145: z in I ; :: thesis:

per cases ;

suppose z = (permutation_of_indices f) . (indx b1) ; :: thesis:

hence (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z by A126, A140, A143, FUNCT_7:31; :: thesis:

end;

suppose z <> (permutation_of_indices f) . (indx b1) ; :: thesis:

then (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z = p0 . z by FUNCT_7:32;
hence (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z by A141, A142, A145, CARD_3:9; :: thesis:

end;

A146: p = f . q by A68, A3, A69, FUNCT_1:35;
dom (p0 +* (((permutation_of_indices f) . (indx b1)),u)) = I by PARTFUN1:def 2;
then p in f .: L by A120, A142, A144, 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 A147: q in L by A36, A3, A146, 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 A147, CARD_3:9;
then A148: q . (indx b1) in S by A122, FUNCT_7:31;
then reconsider qi = q . (indx b1) as Point of (A . (indx b1)) ;
consider q0 being ManySortedSet of I such that
A149: q0 in product b1 and
A150: {(q0 +* ((indx b1),qi))} = product (b1 +* ((indx b1),{qi})) by Th18;
A151: dom q0 = I by PARTFUN1:def 2;

A152: now :: thesis:

let a be set ; :: thesis:
assume a in I ; :: thesis:

per cases ;

suppose a = indx b1 ; :: thesis:

hence (q0 +* ((indx b1),qi)) . a = q . a by A151, FUNCT_7:31; :: thesis:

end;

suppose A153: a <> indx b1 ; :: thesis:

then (q0 +* ((indx b1),qi)) . a = q0 . a by FUNCT_7:32;
hence (q0 +* ((indx b1),qi)) . a = q . a by A125, A147, A149, A153, PENCIL_1:23; :: thesis:

end;

( dom q = I & dom (q0 +* ((indx b1),qi)) = I ) by PARTFUN1:def 2;
then q0 +* ((indx b1),qi) = q by A152, FUNCT_1:2;
then Im (f,(q0 +* ((indx b1),qi))) = {(f . q)} by A36, FUNCT_1:59;
then p in f .: (product (b1 +* ((indx b1),{qi}))) by A146, A150, TARSKI:def 1;
then M . (q . (indx b1)) = (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . ((permutation_of_indices f) . (indx b1)) by A35;
then M . (q . (indx b1)) = o by A143, FUNCT_7:31;
hence o in M .: S by A35, A148, FUNCT_1:def 6; :: thesis:

end;

hence M .: S0 is open by A121, A126, PRE_TOPC:def 2; :: thesis:

end;

take M ; :: thesis:
A154: M is onto by A84, FUNCT_2:def 3;
then M " is bijective by A44, PENCIL_2:12;
hence M is isomorphic by A44, A154, A119, A86, PENCIL_2:def 4; :: thesis:
let a be ManySortedSet of I; :: thesis:
assume that
A155: a is Point of (Segre_Product A) and
A156: a in product b1 ; :: thesis:
dom (Carrier A) = I by PARTFUN1:def 2;
then a . (indx b1) in (Carrier A) . (indx b1) by A5, A155, 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)) ;
A157: dom b1 = I by PARTFUN1:def 2;

A158: now :: thesis:

let o be set ; :: thesis:
assume A159: o in I ; :: thesis:

per cases ;

suppose A160: o = indx b1 ; :: thesis:

then (b1 +* ((indx b1),{ai})) . o = {ai} by A157, FUNCT_7:31;
hence a . o in (b1 +* ((indx b1),{ai})) . o by A160, TARSKI:def 1; :: thesis:

end;

suppose o <> indx b1 ; :: thesis:

then (b1 +* ((indx b1),{ai})) . o = b1 . o by FUNCT_7:32;
hence a . o in (b1 +* ((indx b1),{ai})) . o by A156, A157, A159, CARD_3:9; :: thesis:

end;

( dom a = I & dom (b1 +* ((indx b1),{ai})) = I ) by PARTFUN1:def 2;
then A161: a in product (b1 +* ((indx b1),{ai})) by A158, CARD_3:9;
let b be ManySortedSet of I; :: thesis:
assume b = f . a ; :: thesis:
then b in f .: (product (b1 +* ((indx b1),{ai}))) by A36, A155, A161, FUNCT_1:def 6;
hence b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) by A35; :: thesis: