reconsider B1 = product b1 as Segre-Coset of A by A2;

set s = permutation_of_indices f;

set i = indx b1;

defpred S_{1}[ 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_{1}[x,y]

A37: ( dom M = the carrier of (A . (indx b1)) & ( for x being object st x in the carrier of (A . (indx b1)) holds

S_{1}[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)))

set m = M;

A45: indx b2 = (permutation_of_indices f) . (indx b1) by A1, A3, Def3;

A46: M is one-to-one

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

then M is onto by FUNCT_2:def 3;

then A87: M " = M " by A46, TOPS_2:def 4;

A88: M " is open

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

then A163: a in product (b1 +* ((indx b1),{ai})) by A160, CARD_3:9;

let b be ManySortedSet of I; :: thesis: ( b = f . a implies b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) )

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

set s = permutation_of_indices f;

set i = indx b1;

defpred S

$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

proof

consider M being Function such that
let x be object ; :: thesis: ( x in the carrier of (A . (indx b1)) implies ex y being object st S_{1}[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}))_{1}[x,y]

.= 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: S_{1}[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; :: thesis: ( 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}))) ; :: thesis: 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; :: thesis: verum

end;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

assume A30:
x in the carrier of (A . (indx b1))
; :: thesis: ex y being object st S
thus
{(bb +* ((indx b1),x))} c= product (b1 +* ((indx b1),{x}))
:: according to XBOOLE_0:def 10 :: thesis: product (b1 +* ((indx b1),{x})) c= {(bb +* ((indx b1),x))}

assume o in product (b1 +* ((indx b1),{x})) ; :: thesis: 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;

.= 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: verum

end;proof

assume o in {(bb +* ((indx b1),x))} ; :: thesis: 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; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in product (b1 +* ((indx b1),{x})) or o in {(bb +* ((indx b1),x))} )A13: now :: thesis: for z being object st z in dom (b1 +* ((indx b1),{x})) holds

(bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in {(bb +* ((indx b1),x))} or o in product (b1 +* ((indx b1),{x})) )(bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z

let z be object ; :: thesis: ( z in dom (b1 +* ((indx b1),{x})) implies (bb +* ((indx b1),x)) . b_{1} in (b1 +* ((indx b1),{x})) . b_{1} )

assume z in dom (b1 +* ((indx b1),{x})) ; :: thesis: (bb +* ((indx b1),x)) . b_{1} in (b1 +* ((indx b1),{x})) . b_{1}

then A14: z in I ;

then A15: z in dom bb by PARTFUN1:def 2;

end;assume z in dom (b1 +* ((indx b1),{x})) ; :: thesis: (bb +* ((indx b1),x)) . b

then A14: z in I ;

then A15: z in dom bb by PARTFUN1:def 2;

per cases
( z = indx b1 or z <> indx b1 )
;

end;

suppose A16:
z = indx b1
; :: thesis: (bb +* ((indx b1),x)) . b_{1} in (b1 +* ((indx b1),{x})) . b_{1}

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

end;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: verum

suppose A17:
z <> indx b1
; :: thesis: (bb +* ((indx b1),x)) . b_{1} in (b1 +* ((indx b1),{x})) . b_{1}

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

end;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: verum

assume o in {(bb +* ((indx b1),x))} ; :: thesis: 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; :: thesis: verum

assume o in product (b1 +* ((indx b1),{x})) ; :: thesis: 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 :: thesis: for z being object st z in dom u holds

u . z = (bb +* ((indx b1),x)) . z

dom u =
I
by A20, PARTFUN1:def 2
u . z = (bb +* ((indx b1),x)) . z

let z be object ; :: thesis: ( z in dom u implies u . b_{1} = (bb +* ((indx b1),x)) . b_{1} )

assume A23: z in dom u ; :: thesis: u . b_{1} = (bb +* ((indx b1),x)) . b_{1}

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;

end;assume A23: z in dom u ; :: thesis: u . b

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
( zz = indx b1 or zz <> indx b1 )
;

end;

suppose A26:
zz = indx b1
; :: thesis: u . b_{1} = (bb +* ((indx b1),x)) . b_{1}

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

end;then u . z = x by TARSKI:def 1;

hence u . z = (bb +* ((indx b1),x)) . z by A10, A11, A26, FUNCT_7:31; :: thesis: verum

suppose A27:
zz <> indx b1
; :: thesis: u . b_{1} = (bb +* ((indx b1),x)) . b_{1}

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

end;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: verum

.= 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: verum

A31: now :: thesis: for o being object st o in dom (Carrier A) holds

(bb +* ((indx b1),x)) . o in (Carrier A) . o

dom (bb +* ((indx b1),x)) =
I
by PARTFUN1:def 2
(bb +* ((indx b1),x)) . o in (Carrier A) . o

let o be object ; :: thesis: ( o in dom (Carrier A) implies (bb +* ((indx b1),x)) . b_{1} in (Carrier A) . b_{1} )

assume A32: o in dom (Carrier A) ; :: thesis: (bb +* ((indx b1),x)) . b_{1} in (Carrier A) . b_{1}

then reconsider u = o as Element of I ;

end;assume A32: o in dom (Carrier A) ; :: thesis: (bb +* ((indx b1),x)) . b

then reconsider u = o as Element of I ;

per cases
( u = indx b1 or u <> indx b1 )
;

end;

suppose A33:
u = indx b1
; :: thesis: (bb +* ((indx b1),x)) . b_{1} in (Carrier A) . b_{1}

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

end;hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A33, Th7; :: thesis: verum

suppose A34:
u <> indx b1
; :: thesis: (bb +* ((indx b1),x)) . b_{1} in (Carrier A) . b_{1}

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

end;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: verum

.= 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: S

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

A37: ( dom M = the carrier of (A . (indx b1)) & ( for x being object st x in the carrier of (A . (indx b1)) holds

S

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

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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng M or x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) )

assume x in rng M ; :: thesis: 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; :: thesis: verum

end;assume x in rng M ; :: thesis: 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; :: thesis: verum

set m = M;

A45: indx b2 = (permutation_of_indices f) . (indx b1) by A1, A3, Def3;

A46: M is one-to-one

proof

f is bijective
by PENCIL_2:def 4;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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;

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;

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;

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

end;assume that

A47: ( x1 in dom M & x2 in dom M ) and

A48: M . x1 = M . x2 ; :: thesis: 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;

A55: now :: thesis: for o being object st o in I holds

(p1 +* ((indx b1),o1)) . o in b1 . o

dom (p1 +* ((indx b1),o1)) = I
by PARTFUN1:def 2;(p1 +* ((indx b1),o1)) . o in b1 . o

let o be object ; :: thesis: ( o in I implies (p1 +* ((indx b1),o1)) . b_{1} in b1 . b_{1} )

assume A56: o in I ; :: thesis: (p1 +* ((indx b1),o1)) . b_{1} in b1 . b_{1}

end;assume A56: o in I ; :: thesis: (p1 +* ((indx b1),o1)) . b

per cases
( o = indx b1 or o <> indx b1 )
;

end;

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: for o being object st o in I holds

(p2 +* ((indx b1),o2)) . o in b1 . o

dom (p2 +* ((indx b1),o2)) = I
by PARTFUN1:def 2;(p2 +* ((indx b1),o2)) . o in b1 . o

let o be object ; :: thesis: ( o in I implies (p2 +* ((indx b1),o2)) . b_{1} in b1 . b_{1} )

assume A64: o in I ; :: thesis: (p2 +* ((indx b1),o2)) . b_{1} in b1 . b_{1}

end;assume A64: o in I ; :: thesis: (p2 +* ((indx b1),o2)) . b

per cases
( o = indx b1 or o <> indx b1 )
;

end;

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: for o being object st o in I holds

J1 . o = J2 . o

dom p2 = I
by PARTFUN1:def 2;J1 . o = J2 . o

let o be object ; :: thesis: ( o in I implies J1 . b_{1} = J2 . b_{1} )

assume o in I ; :: thesis: J1 . b_{1} = J2 . b_{1}

then reconsider l = o as Element of I ;

end;assume o in I ; :: thesis: J1 . b

then reconsider l = o as Element of I ;

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

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

then A86:
rng M = the carrier of (A . ((permutation_of_indices f) . (indx b1)))
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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))) ; :: thesis: 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;

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

end;assume x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ; :: thesis: 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 :: thesis: for o being object st o in I holds

q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o

I = dom (Carrier A)
by PARTFUN1:def 2;q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o

let o be object ; :: thesis: ( o in I implies q . b_{1} in (b1 +* ((indx b1),{(q . (indx b1))})) . b_{1} )

assume o in I ; :: thesis: q . b_{1} in (b1 +* ((indx b1),{(q . (indx b1))})) . b_{1}

then reconsider l = o as Element of I ;

end;assume o in I ; :: thesis: q . b

then reconsider l = o as Element of I ;

per cases
( l = indx b1 or l <> indx b1 )
;

end;

suppose
l = indx b1
; :: thesis: q . b_{1} in (b1 +* ((indx b1),{(q . (indx b1))})) . b_{1}

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

end;hence q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o by TARSKI:def 1; :: thesis: verum

suppose
l <> indx b1
; :: thesis: q . b_{1} in (b1 +* ((indx b1),{(q . (indx b1))})) . b_{1}

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;

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

end;A77: dom b2 = I by PARTFUN1:def 2;

A78: dom p0 = I by PARTFUN1:def 2;

A79: now :: thesis: for o being object st o in I holds

p1 . o in b2 . o

dom p1 = I
by PARTFUN1:def 2;p1 . o in b2 . o

let o be object ; :: thesis: ( o in I implies p1 . b_{1} in b2 . b_{1} )

assume A80: o in I ; :: thesis: p1 . b_{1} in b2 . b_{1}

end;assume A80: o in I ; :: thesis: p1 . b

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

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

then M is onto by FUNCT_2:def 3;

then A87: M " = M " by A46, TOPS_2:def 4;

A88: M " is open

proof

A121:
M is open
let S0 be Subset of (A . ((permutation_of_indices f) . (indx b1))); :: according to T_0TOPSP:def 2 :: thesis: ( not S0 is open or (M ") .: S0 is open )

assume S0 is open ; :: thesis: (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;

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)

hence (M ") .: S0 is open by PRE_TOPC:def 2; :: thesis: verum

end;assume S0 is open ; :: thesis: (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;

A92: now :: thesis: for x being object st x in I holds

(b2 +* ((indx b2),S)) . x c= b2 . x

dom (b2 +* ((indx b2),S)) = I
by PARTFUN1:def 2;(b2 +* ((indx b2),S)) . x c= b2 . x

let x be object ; :: thesis: ( x in I implies (b2 +* ((indx b2),S)) . b_{1} c= b2 . b_{1} )

assume x in I ; :: thesis: (b2 +* ((indx b2),S)) . b_{1} c= b2 . b_{1}

end;assume x in I ; :: thesis: (b2 +* ((indx b2),S)) . b

per cases
( x = indx b2 or x <> indx b2 )
;

end;

suppose A93:
x = indx b2
; :: thesis: (b2 +* ((indx b2),S)) . b_{1} c= b2 . b_{1}

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

end;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: verum

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

then
(M ") .: S is Block of (A . (indx b1))
by A46, A87, A90, A95, FUNCT_1:85;
thus
M " S c= k . (indx k)
:: according to XBOOLE_0:def 10 :: thesis: k . (indx k) c= M " S

assume A112: o in k . (indx k) ; :: thesis: 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;

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

end;proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in k . (indx k) or o in M " S )
let o be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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

M . o in S by A97, FUNCT_1:def 7;

then A109: fq . ((permutation_of_indices f) . (indx b1)) in S by A37, A100;

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

end;A96: dom b2 = I by PARTFUN1:def 2;

assume A97: o in M " S ; :: thesis: 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

proof

then A108:
f .: (product (b1 +* ((indx b1),{u}))) c= product b2
by A3, RELAT_1:123;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in product (b1 +* ((indx b1),{u})) or a in product b1 )

A101: dom b1 = I by PARTFUN1:def 2;

assume a in product (b1 +* ((indx b1),{u})) ; :: thesis: a in product b1

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;

end;A101: dom b1 = I by PARTFUN1:def 2;

assume a in product (b1 +* ((indx b1),{u})) ; :: thesis: a in product b1

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: for o being object st o in I holds

g . o in b1 . o

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

let o be object ; :: thesis: ( o in I implies g . b_{1} in b1 . b_{1} )

assume o in I ; :: thesis: g . b_{1} in b1 . b_{1}

then A106: g . o in (b1 +* ((indx b1),{u})) . o by A103, A104, A105;

end;assume o in I ; :: thesis: g . b

then A106: g . o in (b1 +* ((indx b1),{u})) . o by A103, A104, A105;

per cases
( o = indx b1 or o <> indx b1 )
;

end;

suppose A107:
o = indx b1
; :: thesis: g . b_{1} in b1 . b_{1}

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

end;then g . o in [#] (A . (indx b1)) ;

hence g . o in b1 . o by A2, A107, Th10; :: thesis: verum

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: for o being object st o in I holds

fq . o in (b2 +* ((indx b2),S)) . o

( dom fq = I & dom (b2 +* ((indx b2),S)) = I )
by PARTFUN1:def 2;fq . o in (b2 +* ((indx b2),S)) . o

let o be object ; :: thesis: ( o in I implies fq . b_{1} in (b2 +* ((indx b2),S)) . b_{1} )

assume A111: o in I ; :: thesis: fq . b_{1} in (b2 +* ((indx b2),S)) . b_{1}

end;assume A111: o in I ; :: thesis: fq . b

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

assume A112: o in k . (indx k) ; :: thesis: 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;

A117: now :: thesis: for a being object st a in I holds

(p0 +* ((indx b1),u)) . a in k . a

( dom (p0 +* ((indx b1),u)) = I & dom k = I )
by PARTFUN1:def 2;(p0 +* ((indx b1),u)) . a in k . a

let a be object ; :: thesis: ( a in I implies (p0 +* ((indx b1),u)) . b_{1} in k . b_{1} )

assume A118: a in I ; :: thesis: (p0 +* ((indx b1),u)) . b_{1} in k . b_{1}

end;assume A118: a in I ; :: thesis: (p0 +* ((indx b1),u)) . b

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

hence (M ") .: S0 is open by PRE_TOPC:def 2; :: thesis: verum

proof

take
M
; :: thesis: ( M is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
let S0 be Subset of (A . (indx b1)); :: according to T_0TOPSP:def 2 :: thesis: ( not S0 is open or M .: S0 is open )

assume S0 is open ; :: thesis: 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;

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)

end;assume S0 is open ; :: thesis: 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;

A125: now :: thesis: for x being object st x in I holds

(b1 +* ((indx b1),S)) . x c= b1 . x

dom (b1 +* ((indx b1),S)) = I
by PARTFUN1:def 2;(b1 +* ((indx b1),S)) . x c= b1 . x

let x be object ; :: thesis: ( x in I implies (b1 +* ((indx b1),S)) . b_{1} c= b1 . b_{1} )

assume x in I ; :: thesis: (b1 +* ((indx b1),S)) . b_{1} c= b1 . b_{1}

end;assume x in I ; :: thesis: (b1 +* ((indx b1),S)) . b

per cases
( x = indx b1 or x <> indx b1 )
;

end;

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

hence
M .: S0 is open
by A123, A128, PRE_TOPC:def 2; :: thesis: verum
thus
M .: S c= k . (indx k)
:: according to XBOOLE_0:def 10 :: thesis: k . (indx k) c= M .: S

assume A142: o in k . (indx k) ; :: thesis: 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;

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;

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

end;proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in k . (indx k) or o in M .: S )
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in M .: S or o in k . (indx k) )

A130: dom b1 = I by PARTFUN1:def 2;

assume o in M .: S ; :: thesis: 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;

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

end;A130: dom b1 = I by PARTFUN1:def 2;

assume o in M .: S ; :: thesis: 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;

A138: now :: thesis: for a being object st a in I holds

(p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a

( dom (p0 +* ((indx b1),u)) = I & dom (b1 +* ((indx b1),S)) = I )
by PARTFUN1:def 2;(p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a

let a be object ; :: thesis: ( a in I implies (p0 +* ((indx b1),u)) . b_{1} in (b1 +* ((indx b1),S)) . b_{1} )

assume A139: a in I ; :: thesis: (p0 +* ((indx b1),u)) . b_{1} in (b1 +* ((indx b1),S)) . b_{1}

end;assume A139: a in I ; :: thesis: (p0 +* ((indx b1),u)) . b

per cases
( a = indx b1 or a <> indx b1 )
;

end;

suppose A140:
a = indx b1
; :: thesis: (p0 +* ((indx b1),u)) . b_{1} in (b1 +* ((indx b1),S)) . b_{1}

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

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

suppose A141:
a <> indx b1
; :: thesis: (p0 +* ((indx b1),u)) . b_{1} in (b1 +* ((indx b1),S)) . b_{1}

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

end;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: verum

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

assume A142: o in k . (indx k) ; :: thesis: 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;

A146: now :: thesis: for z being object st z in I holds

(p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z

A148:
p = f . q
by A70, A5, A71, FUNCT_1:35;(p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z

let z be object ; :: thesis: ( z in I implies (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b_{1} in k . b_{1} )

assume A147: z in I ; :: thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b_{1} in k . b_{1}

end;assume A147: z in I ; :: thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b

per cases
( z = (permutation_of_indices f) . (indx b1) or z <> (permutation_of_indices f) . (indx b1) )
;

end;

suppose
z = (permutation_of_indices f) . (indx b1)
; :: thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b_{1} in k . b_{1}

hence
(p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z
by A128, A142, A145, FUNCT_7:31; :: thesis: verum

end;suppose
z <> (permutation_of_indices f) . (indx b1)
; :: thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b_{1} in k . b_{1}

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

end;hence (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z by A143, A144, A147, CARD_3:9; :: thesis: verum

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: for a being object st a in I holds

(q0 +* ((indx b1),qi)) . a = q . a

q0 +* ((indx b1),qi) = q
by A154;(q0 +* ((indx b1),qi)) . a = q . a

let a be object ; :: thesis: ( a in I implies (q0 +* ((indx b1),qi)) . b_{1} = q . b_{1} )

assume a in I ; :: thesis: (q0 +* ((indx b1),qi)) . b_{1} = q . b_{1}

end;assume a in I ; :: thesis: (q0 +* ((indx b1),qi)) . b

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

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

A160: now :: thesis: for o being object st o in I holds

a . o in (b1 +* ((indx b1),{ai})) . o

( dom a = I & dom (b1 +* ((indx b1),{ai})) = I )
by PARTFUN1:def 2;a . o in (b1 +* ((indx b1),{ai})) . o

let o be object ; :: thesis: ( o in I implies a . b_{1} in (b1 +* ((indx b1),{ai})) . b_{1} )

assume A161: o in I ; :: thesis: a . b_{1} in (b1 +* ((indx b1),{ai})) . b_{1}

end;assume A161: o in I ; :: thesis: a . b

then A163: a in product (b1 +* ((indx b1),{ai})) by A160, CARD_3:9;

let b be ManySortedSet of I; :: thesis: ( b = f . a implies b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) )

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