reconsider B1 = product b1 as Segre-Coset of A by A2;
set s = permutation_of_indices f;
set i = indx b1;
defpred S₁[ 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 S₁[x,y]

proof

let x be object ; :: thesis:
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})) :: according to XBOOLE_0:def 10 :: thesis:

proof

A13: now :: thesis:

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

per cases ;

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

then (bb +* ((indx b1),x)) . z = x by A15, 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 A11, A16, FUNCT_7:31; :: thesis:

end;

suppose A17: 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 A9, A11, A14, CARD_3:9;
hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A17, FUNCT_7:32; :: thesis:

end;

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

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in product (b1 +* ((indx b1),{x})) ; :: thesis:
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 :: thesis:

let z be object ; :: thesis:
assume A23: z in dom u ; :: thesis:
then 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 ;

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

then u . z in {x} by A11, A25, FUNCT_7:31;
then u . z = x by TARSKI:def 1;
hence u . z = (bb +* ((indx b1),x)) . z by A10, A11, A26, FUNCT_7:31; :: thesis:

end;

suppose A27: 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 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; :: thesis:

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; :: thesis:

end;

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

A31: now :: thesis:

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

per cases ;

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

then (bb +* ((indx b1),x)) . u in [#] (A . (indx b1)) by A30, A10, A11, FUNCT_7:31;
hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A33, Th7; :: thesis:

end;

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

b1 c= Carrier A by PBOOLE:def 18;
then A35: b1 . o c= (Carrier A) . o by A32;
(bb +* ((indx b1),x)) . u = bb . u by A34, FUNCT_7:32;
then (bb +* ((indx b1),x)) . u in b1 . u by A9, A11, CARD_3:9;
hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A35; :: 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 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)) ; :: thesis:
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; :: 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 A12, A36, TARSKI:def 1; :: thesis:

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
S₁[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 ; :: according to TARSKI:def 3 :: thesis:
assume x in rng M ; :: thesis:
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; :: thesis:

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 ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A47: ( x1 in dom M & x2 in dom M ) and
A48: M . x1 = M . x2 ; :: thesis:
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;

A55: now :: thesis:

let o be object ; :: thesis:
assume A56: o in I ; :: thesis:

per cases ;

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

then (p1 +* ((indx b1),o1)) . o = o1 by A54, FUNCT_7:31;
then (p1 +* ((indx b1),o1)) . o in [#] (A . (indx b1)) ;
hence (p1 +* ((indx b1),o1)) . o in b1 . o by A2, A57, 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 A49, A53, A56, CARD_3:9; :: thesis:

end;

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;

A63: now :: thesis:

let o be object ; :: thesis:
assume A64: o in I ; :: thesis:

per cases ;

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

then (p2 +* ((indx b1),o2)) . o = o2 by A62, FUNCT_7:31;
then (p2 +* ((indx b1),o2)) . o in [#] (A . (indx b1)) ;
hence (p2 +* ((indx b1),o2)) . o in b1 . o by A2, A65, 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 A51, A61, A64, CARD_3:9; :: thesis:

end;

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 :: thesis:

let o be object ; :: 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 A45, A37, A48, A67, A59; :: thesis:

end;

suppose l <> indx b2 ; :: thesis:

hence J1 . o = J2 . o by A3, A58, A66, PENCIL_1:23; :: thesis:

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; :: thesis:

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 ; :: 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
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 :: thesis:

let o be object ; :: 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 A74, 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 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;

A79: now :: thesis:

let o be object ; :: thesis:
assume A80: o in I ; :: thesis:

per cases ;

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

then p1 . o = x1 by A78, FUNCT_7:31;
then p1 . o in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ;
hence p1 . o in b2 . o by A1, A3, A4, A81, Def3; :: thesis:

end;

suppose o <> indx b2 ; :: thesis:

then p1 . o = p0 . o by FUNCT_7:32;
hence p1 . o in b2 . o by A72, A77, A80, CARD_3:9; :: thesis:

end;

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; :: thesis:

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; :: thesis:

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))); :: 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 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;

A92: now :: thesis:

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

per cases ;

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

then (b2 +* ((indx b2),S)) . x = S by A91, 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 A1, A3, A4, A93, 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 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) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
A96: dom b2 = I by PARTFUN1:def 2;
assume A97: o in M " S ; :: thesis:
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

proof

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

now :: thesis:

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

per cases ;

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

then g . o in {u} by A101, A106, FUNCT_7:31;
then g . o in [#] (A . (indx b1)) ;
hence g . o in b1 . o by A2, A107, Th10; :: thesis:

end;

suppose o <> indx b1 ; :: thesis:

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

end;

hence a in product b1 by A102, A105, A101, CARD_3:9; :: thesis:

end;

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;

A110: now :: thesis:

let o be object ; :: thesis:
assume A111: o in I ; :: thesis:

per cases ;

suppose o = indx b2 ; :: thesis:

hence fq . o in (b2 +* ((indx b2),S)) . o by A45, A109, A96, 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 A100, A108, A96, A111, CARD_3:9; :: thesis:

end;

( 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; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A112: o in k . (indx k) ; :: thesis:
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;

A117: now :: thesis:

let a be object ; :: thesis:
assume A118: a in I ; :: thesis:

per cases ;

suppose a = indx b1 ; :: thesis:

hence (p0 +* ((indx b1),u)) . a in k . a by A95, A112, A116, FUNCT_7:31; :: thesis:

end;

suppose A119: 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 A113, A115, A118, CARD_3:9;
hence (p0 +* ((indx b1),u)) . a in k . a by A94, A119, PENCIL_1:26; :: thesis:

end;

( 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; :: thesis:

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; :: thesis:

end;

A121: 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
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;

A125: now :: thesis:

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

per cases ;

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

then (b1 +* ((indx b1),S)) . x = S by A124, FUNCT_7:31;
then (b1 +* ((indx b1),S)) . x c= [#] (A . (indx b1)) ;
hence (b1 +* ((indx b1),S)) . x c= b1 . x by A2, A126, 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 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) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
A130: dom b1 = I by PARTFUN1:def 2;
assume o in M .: S ; :: thesis:
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;

A138: now :: thesis:

let a be object ; :: thesis:
assume A139: a in I ; :: thesis:

per cases ;

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

then (p0 +* ((indx b1),u)) . a = u by A137, FUNCT_7:31;
hence (p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a by A132, A130, A140, FUNCT_7:31; :: thesis:

end;

suppose A141: 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 A134, A130, A139, CARD_3:9;
hence (p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a by A141, 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 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; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A142: o in k . (indx k) ; :: thesis:
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;

A146: now :: thesis:

let z be object ; :: thesis:
assume A147: 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 A128, A142, A145, 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 A143, A144, A147, CARD_3:9; :: thesis:

end;

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;

A154: now :: thesis:

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

per cases ;

suppose a = indx b1 ; :: thesis:

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

end;

suppose A155: 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 A127, A149, A151, A155, PENCIL_1:23; :: thesis:

end;

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; :: thesis:

end;

hence M .: S0 is open by A123, A128, PRE_TOPC:def 2; :: thesis:

end;

take M ; :: thesis:
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; :: thesis:
let a be ManySortedSet of I; :: thesis:
assume that
A157: a is Point of (Segre_Product A) and
A158: a in product b1 ; :: thesis:
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;

A160: now :: thesis:

let o be object ; :: thesis:
assume A161: o in I ; :: thesis:

per cases ;

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

then (b1 +* ((indx b1),{ai})) . o = {ai} by A159, FUNCT_7:31;
hence a . o in (b1 +* ((indx b1),{ai})) . o by A162, 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 A158, A159, A161, CARD_3:9; :: thesis:

end;

( 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; :: thesis:
assume b = f . a ; :: thesis:
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; :: thesis: