let I be non empty finite set ; :: thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds

for f being Collineation of (Segre_Product A) ex s being Permutation of I st

for i, j being Element of I holds

( s . i = j iff for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds

indx b2 = j )

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) ex s being Permutation of I st

for i, j being Element of I holds

( s . i = j iff for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds

indx b2 = j ) )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for f being Collineation of (Segre_Product A) ex s being Permutation of I st

for i, j being Element of I holds

( s . i = j iff for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds

indx b2 = j )

let f be Collineation of (Segre_Product A); :: thesis: ex s being Permutation of I st

for i, j being Element of I holds

( s . i = j iff for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds

indx b2 = j )

defpred S_{1}[ set , set ] means for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = $1 holds

indx b2 = $2;

A2: for x, y, x9 being Element of I st S_{1}[x,y] & S_{1}[x9,y] holds

x = x9_{1}[x,y]
_{1}[x,y]
_{1}[x,y] & S_{1}[x,y9] holds

y = y9

for x, y being Element of I holds

( f . x = y iff S_{1}[x,y] )
from TRANSGEO:sch 1(A33, A20, A2, A45); :: thesis: verum

for f being Collineation of (Segre_Product A) ex s being Permutation of I st

for i, j being Element of I holds

( s . i = j iff for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds

indx b2 = j )

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) ex s being Permutation of I st

for i, j being Element of I holds

( s . i = j iff for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds

indx b2 = j ) )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for f being Collineation of (Segre_Product A) ex s being Permutation of I st

for i, j being Element of I holds

( s . i = j iff for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds

indx b2 = j )

let f be Collineation of (Segre_Product A); :: thesis: ex s being Permutation of I st

for i, j being Element of I holds

( s . i = j iff for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds

indx b2 = j )

defpred S

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = $1 holds

indx b2 = $2;

A2: for x, y, x9 being Element of I st S

x = x9

proof

A20:
for y being Element of I ex x being Element of I st S
reconsider ff = f " as Collineation of (Segre_Product A) by PENCIL_2:13;

let x, y, x9 be Element of I; :: thesis: ( S_{1}[x,y] & S_{1}[x9,y] implies x = x9 )

assume that

A3: for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds

indx b2 = y and

A4: for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x9 holds

indx b2 = y ; :: thesis: x = x9

consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A5: indx b1 = x and

A6: product b1 is Segre-Coset of A by Th8;

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

reconsider fB1 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24;

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A7: fB1 = product L1 and

L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;

consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A8: indx b2 = x9 and

A9: product b2 is Segre-Coset of A by Th8;

reconsider B2 = product b2 as Segre-Coset of A by A9;

reconsider fB2 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24;

consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A10: fB2 = product L2 and

L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;

A11: indx L2 = y by A4, A8, A10;

A12: f is bijective by PENCIL_2:def 4;

A13: ff = f " by A12, TOPS_2:def 4;

then A14: ff .: fB2 = f " fB2 by A12, FUNCT_1:85;

A15: ff .: fB1 = f " fB1 by A12, A13, FUNCT_1:85;

dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

then A16: B2 c= ff .: fB2 by A14, FUNCT_1:76;

ff .: fB2 c= B2 by A12, A14, FUNCT_1:82;

then A17: B2 = ff .: fB2 by A16;

dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

then A18: B1 c= ff .: fB1 by A15, FUNCT_1:76;

ff .: fB1 c= B1 by A12, A15, FUNCT_1:82;

then A19: B1 = ff .: fB1 by A18;

indx L1 = y by A3, A5, A7;

hence x = x9 by A1, A5, A7, A8, A10, A11, A19, A17, Th24; :: thesis: verum

end;let x, y, x9 be Element of I; :: thesis: ( S

assume that

A3: for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds

indx b2 = y and

A4: for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x9 holds

indx b2 = y ; :: thesis: x = x9

consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A5: indx b1 = x and

A6: product b1 is Segre-Coset of A by Th8;

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

reconsider fB1 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24;

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A7: fB1 = product L1 and

L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;

consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A8: indx b2 = x9 and

A9: product b2 is Segre-Coset of A by Th8;

reconsider B2 = product b2 as Segre-Coset of A by A9;

reconsider fB2 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24;

consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A10: fB2 = product L2 and

L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;

A11: indx L2 = y by A4, A8, A10;

A12: f is bijective by PENCIL_2:def 4;

A13: ff = f " by A12, TOPS_2:def 4;

then A14: ff .: fB2 = f " fB2 by A12, FUNCT_1:85;

A15: ff .: fB1 = f " fB1 by A12, A13, FUNCT_1:85;

dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

then A16: B2 c= ff .: fB2 by A14, FUNCT_1:76;

ff .: fB2 c= B2 by A12, A14, FUNCT_1:82;

then A17: B2 = ff .: fB2 by A16;

dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

then A18: B1 c= ff .: fB1 by A15, FUNCT_1:76;

ff .: fB1 c= B1 by A12, A15, FUNCT_1:82;

then A19: B1 = ff .: fB1 by A18;

indx L1 = y by A3, A5, A7;

hence x = x9 by A1, A5, A7, A8, A10, A11, A19, A17, Th24; :: thesis: verum

proof

A33:
for x being Element of I ex y being Element of I st S
set p0 = the Point of (Segre_Product A);

reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6;

let x be Element of I; :: thesis: ex x being Element of I st S_{1}[x,x]

reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;

dom A = I by PARTFUN1:def 2;

then A . x in rng A by FUNCT_1:3;

then not A . x is trivial by PENCIL_1:def 18;

then reconsider C = [#] (A . x) as non trivial set ;

reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;

dom p = I by PARTFUN1:def 2;

then A21: b . x = C by FUNCT_7:31;

then A22: indx b = x by PENCIL_1:def 21;

product b c= the carrier of (Segre_Product A)

reconsider fB = f " B as Segre-Coset of A by A1, PENCIL_2:25;

consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A31: fB = product b0 and

b0 . (indx b0) = [#] (A . (indx b0)) by PENCIL_2:def 2;

take y = indx b0; :: thesis: S_{1}[y,x]

let B1 be Segre-Coset of A; :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = y holds

indx b2 = x

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y implies indx b2 = x )

f is bijective by PENCIL_2:def 4;

then rng f = the carrier of (Segre_Product A) by FUNCT_2:def 3;

then A32: f .: fB = product b by FUNCT_1:77;

assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y ) ; :: thesis: indx b2 = x

hence indx b2 = x by A1, A22, A31, A32, Th24; :: thesis: verum

end;reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6;

let x be Element of I; :: thesis: ex x being Element of I st S

reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;

dom A = I by PARTFUN1:def 2;

then A . x in rng A by FUNCT_1:3;

then not A . x is trivial by PENCIL_1:def 18;

then reconsider C = [#] (A . x) as non trivial set ;

reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;

dom p = I by PARTFUN1:def 2;

then A21: b . x = C by FUNCT_7:31;

then A22: indx b = x by PENCIL_1:def 21;

product b c= the carrier of (Segre_Product A)

proof

then reconsider B = product b as Segre-Coset of A by A21, A22, PENCIL_2:def 2;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in product b or a in the carrier of (Segre_Product A) )

assume a in product b ; :: thesis: a in the carrier of (Segre_Product A)

then consider f being Function such that

A23: a = f and

A24: dom f = dom b and

A25: for x being object st x in dom b holds

f . x in b . x by CARD_3:def 5;

dom (Carrier A) = I by PARTFUN1:def 2;

then A26: dom f = dom (Carrier A) by A24, PARTFUN1:def 2;

hence a in the carrier of (Segre_Product A) by A23, A26, A27, CARD_3:def 5; :: thesis: verum

end;assume a in product b ; :: thesis: a in the carrier of (Segre_Product A)

then consider f being Function such that

A23: a = f and

A24: dom f = dom b and

A25: for x being object st x in dom b holds

f . x in b . x by CARD_3:def 5;

dom (Carrier A) = I by PARTFUN1:def 2;

then A26: dom f = dom (Carrier A) by A24, PARTFUN1:def 2;

A27: now :: thesis: for i being object st i in dom (Carrier A) holds

f . i in (Carrier A) . i

Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #)
by PENCIL_1:def 23;f . i in (Carrier A) . i

let i be object ; :: thesis: ( i in dom (Carrier A) implies f . b_{1} in (Carrier A) . b_{1} )

assume A28: i in dom (Carrier A) ; :: thesis: f . b_{1} in (Carrier A) . b_{1}

then reconsider i1 = i as Element of I ;

A29: f . i in b . i by A24, A25, A26, A28;

end;assume A28: i in dom (Carrier A) ; :: thesis: f . b

then reconsider i1 = i as Element of I ;

A29: f . i in b . i by A24, A25, A26, A28;

per cases
( i1 = x or i1 <> x )
;

end;

suppose
i1 <> x
; :: thesis: f . b_{1} in (Carrier A) . b_{1}

then
f . i1 in p . i1
by A29, FUNCT_7:32;

then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;

then f . i1 = p0 . i1 by TARSKI:def 1;

then A30: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;

not [#] (A . i1) is empty ;

then not (Carrier A) . i1 is empty by Th7;

hence f . i in (Carrier A) . i by A30; :: thesis: verum

end;then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;

then f . i1 = p0 . i1 by TARSKI:def 1;

then A30: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;

not [#] (A . i1) is empty ;

then not (Carrier A) . i1 is empty by Th7;

hence f . i in (Carrier A) . i by A30; :: thesis: verum

hence a in the carrier of (Segre_Product A) by A23, A26, A27, CARD_3:def 5; :: thesis: verum

reconsider fB = f " B as Segre-Coset of A by A1, PENCIL_2:25;

consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A31: fB = product b0 and

b0 . (indx b0) = [#] (A . (indx b0)) by PENCIL_2:def 2;

take y = indx b0; :: thesis: S

let B1 be Segre-Coset of A; :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = y holds

indx b2 = x

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y implies indx b2 = x )

f is bijective by PENCIL_2:def 4;

then rng f = the carrier of (Segre_Product A) by FUNCT_2:def 3;

then A32: f .: fB = product b by FUNCT_1:77;

assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y ) ; :: thesis: indx b2 = x

hence indx b2 = x by A1, A22, A31, A32, Th24; :: thesis: verum

proof

A45:
for x, y, y9 being Element of I st S
set p0 = the Point of (Segre_Product A);

reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6;

let x be Element of I; :: thesis: ex y being Element of I st S_{1}[x,y]

reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;

dom A = I by PARTFUN1:def 2;

then A . x in rng A by FUNCT_1:3;

then not A . x is trivial by PENCIL_1:def 18;

then reconsider C = [#] (A . x) as non trivial set ;

reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;

dom p = I by PARTFUN1:def 2;

then A34: b . x = C by FUNCT_7:31;

then A35: indx b = x by PENCIL_1:def 21;

product b c= the carrier of (Segre_Product A)

reconsider fB = f .: B as Segre-Coset of A by A1, PENCIL_2:24;

consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A44: fB = product b0 and

b0 . (indx b0) = [#] (A . (indx b0)) by PENCIL_2:def 2;

take indx b0 ; :: thesis: S_{1}[x, indx b0]

let B1 be Segre-Coset of A; :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds

indx b2 = indx b0

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x implies indx b2 = indx b0 )

assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x ) ; :: thesis: indx b2 = indx b0

hence indx b2 = indx b0 by A1, A35, A44, Th24; :: thesis: verum

end;reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6;

let x be Element of I; :: thesis: ex y being Element of I st S

reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;

dom A = I by PARTFUN1:def 2;

then A . x in rng A by FUNCT_1:3;

then not A . x is trivial by PENCIL_1:def 18;

then reconsider C = [#] (A . x) as non trivial set ;

reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;

dom p = I by PARTFUN1:def 2;

then A34: b . x = C by FUNCT_7:31;

then A35: indx b = x by PENCIL_1:def 21;

product b c= the carrier of (Segre_Product A)

proof

then reconsider B = product b as Segre-Coset of A by A34, A35, PENCIL_2:def 2;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in product b or a in the carrier of (Segre_Product A) )

assume a in product b ; :: thesis: a in the carrier of (Segre_Product A)

then consider f being Function such that

A36: a = f and

A37: dom f = dom b and

A38: for x being object st x in dom b holds

f . x in b . x by CARD_3:def 5;

dom (Carrier A) = I by PARTFUN1:def 2;

then A39: dom f = dom (Carrier A) by A37, PARTFUN1:def 2;

hence a in the carrier of (Segre_Product A) by A36, A39, A40, CARD_3:def 5; :: thesis: verum

end;assume a in product b ; :: thesis: a in the carrier of (Segre_Product A)

then consider f being Function such that

A36: a = f and

A37: dom f = dom b and

A38: for x being object st x in dom b holds

f . x in b . x by CARD_3:def 5;

dom (Carrier A) = I by PARTFUN1:def 2;

then A39: dom f = dom (Carrier A) by A37, PARTFUN1:def 2;

A40: now :: thesis: for i being object st i in dom (Carrier A) holds

f . i in (Carrier A) . i

Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #)
by PENCIL_1:def 23;f . i in (Carrier A) . i

let i be object ; :: thesis: ( i in dom (Carrier A) implies f . b_{1} in (Carrier A) . b_{1} )

assume A41: i in dom (Carrier A) ; :: thesis: f . b_{1} in (Carrier A) . b_{1}

then reconsider i1 = i as Element of I ;

A42: f . i in b . i by A37, A38, A39, A41;

end;assume A41: i in dom (Carrier A) ; :: thesis: f . b

then reconsider i1 = i as Element of I ;

A42: f . i in b . i by A37, A38, A39, A41;

per cases
( i1 = x or i1 <> x )
;

end;

suppose
i1 <> x
; :: thesis: f . b_{1} in (Carrier A) . b_{1}

then
f . i1 in p . i1
by A42, FUNCT_7:32;

then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;

then f . i1 = p0 . i1 by TARSKI:def 1;

then A43: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;

not [#] (A . i1) is empty ;

then not (Carrier A) . i1 is empty by Th7;

hence f . i in (Carrier A) . i by A43; :: thesis: verum

end;then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;

then f . i1 = p0 . i1 by TARSKI:def 1;

then A43: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;

not [#] (A . i1) is empty ;

then not (Carrier A) . i1 is empty by Th7;

hence f . i in (Carrier A) . i by A43; :: thesis: verum

hence a in the carrier of (Segre_Product A) by A36, A39, A40, CARD_3:def 5; :: thesis: verum

reconsider fB = f .: B as Segre-Coset of A by A1, PENCIL_2:24;

consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A44: fB = product b0 and

b0 . (indx b0) = [#] (A . (indx b0)) by PENCIL_2:def 2;

take indx b0 ; :: thesis: S

let B1 be Segre-Coset of A; :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds

indx b2 = indx b0

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x implies indx b2 = indx b0 )

assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x ) ; :: thesis: indx b2 = indx b0

hence indx b2 = indx b0 by A1, A35, A44, Th24; :: thesis: verum

y = y9

proof

thus
ex f being Permutation of I st
let x, y, y9 be Element of I; :: thesis: ( S_{1}[x,y] & S_{1}[x,y9] implies y = y9 )

assume that

A46: for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds

indx b2 = y and

A47: for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds

indx b2 = y9 ; :: thesis: y = y9

consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A48: indx b1 = x and

A49: product b1 is Segre-Coset of A by Th8;

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

reconsider fB1 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24;

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A50: fB1 = product L1 and

L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;

indx L1 = y by A46, A48, A50;

hence y = y9 by A47, A48, A50; :: thesis: verum

end;assume that

A46: for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds

indx b2 = y and

A47: for B1 being Segre-Coset of A

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds

indx b2 = y9 ; :: thesis: y = y9

consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A48: indx b1 = x and

A49: product b1 is Segre-Coset of A by Th8;

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

reconsider fB1 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24;

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A50: fB1 = product L1 and

L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;

indx L1 = y by A46, A48, A50;

hence y = y9 by A47, A48, A50; :: thesis: verum

for x, y being Element of I holds

( f . x = y iff S