let I be non empty set ; :: thesis:
let A be PLS-yielding ManySortedSet of I; :: thesis:
let S be Subset of (Segre_Product A); :: thesis:
thus ( not S is trivial & S is strong & S is closed_under_lines implies ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ) ) ) :: thesis:

proof

assume A1: ( not S is trivial & S is strong & S is closed_under_lines ) ; :: thesis:
then 2 c= card S by Th4;
then consider a, b being object such that
A2: a in S and
A3: b in S and
A4: a <> b by Th2;
reconsider a = a, b = b as Point of (Segre_Product A) by A2, A3;
a,b are_collinear by A1, A2, A3;
then consider C being Block of (Segre_Product A) such that
A5: {a,b} c= C by A4;
consider CC being Segre-like ManySortedSubset of Carrier A such that
A6: C = product CC and
ex i being Element of I st CC . i is Block of (A . i) by Def22;
( a in product CC & b in product CC ) by A5, A6, ZFMISC_1:32;
then 2 c= card (product CC) by A4, Th2;
then reconsider CC = CC as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th13;
A7: dom CC = I by PARTFUN1:def 2;
reconsider a1 = a, b1 = b as ManySortedSet of I by Th14;
A8: dom a1 = I by PARTFUN1:def 2;
A9: dom b1 = I by PARTFUN1:def 2;

A10: now :: thesis:

assume A11: a1 . (indx CC) = b1 . (indx CC) ; :: thesis:
for i being object st i in I holds
a1 . i = b1 . i

proof

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

per cases ;

suppose i = indx CC ; :: thesis:

hence a1 . i = b1 . i by A11; :: thesis:

end;

suppose A12: i <> indx CC ; :: thesis:

( a1 in product CC & b1 in product CC ) by A5, A6, ZFMISC_1:32;
hence a1 . i = b1 . i by A12, Th23; :: thesis:

end;

hence contradiction by A4, A8, A9, FUNCT_1:2; :: thesis:

end;

A13: for f being ManySortedSet of I st f in S holds
for i being Element of I st i <> indx CC holds
f . i in CC . i

proof

let f be ManySortedSet of I; :: thesis:
assume A14: f in S ; :: thesis:
then reconsider f1 = f as Point of (Segre_Product A) ;
let i be Element of I; :: thesis:
assume A15: i <> indx CC ; :: thesis:

now :: thesis:

b1 in product CC by A5, A6, ZFMISC_1:32;
then A16: b1 . i in CC . i by A7, CARD_3:9;
assume A17: not f . i in CC . i ; :: thesis:
f1,b are_collinear by A1, A3, A14;
then consider lb being Block of (Segre_Product A) such that
A18: {f1,b} c= lb by A17, A16;
consider Lb being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A19: lb = product Lb and
Lb . (indx Lb) is Block of (A . (indx Lb)) by Th24;
A20: b1 in product Lb by A18, A19, ZFMISC_1:32;
A21: f in product Lb by A18, A19, ZFMISC_1:32;
then indx Lb = i by A17, A16, A20, Th23;
then Lb . (indx CC) is 1 -element by A15, Th12;
then consider cb being object such that
A22: Lb . (indx CC) = {cb} by ZFMISC_1:131;
A23: dom Lb = I by PARTFUN1:def 2;
then b1 . (indx CC) in {cb} by A20, A22, CARD_3:9;
then A24: b1 . (indx CC) = cb by TARSKI:def 1;
a1 in product CC by A5, A6, ZFMISC_1:32;
then A25: a1 . i in CC . i by A7, CARD_3:9;
f1,a are_collinear by A1, A2, A14;
then consider la being Block of (Segre_Product A) such that
A26: {f1,a} c= la by A17, A25;
consider La being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A27: la = product La and
La . (indx La) is Block of (A . (indx La)) by Th24;
A28: a1 in product La by A26, A27, ZFMISC_1:32;
A29: f in product La by A26, A27, ZFMISC_1:32;
then indx La = i by A17, A25, A28, Th23;
then La . (indx CC) is 1 -element by A15, Th12;
then consider ca being object such that
A30: La . (indx CC) = {ca} by ZFMISC_1:131;
A31: dom La = I by PARTFUN1:def 2;
then a1 . (indx CC) in {ca} by A28, A30, CARD_3:9;
then A32: ca <> cb by A10, A24, TARSKI:def 1;
f . (indx CC) in {ca} by A29, A30, A31, CARD_3:9;
then A33: f . (indx CC) <> cb by A32, TARSKI:def 1;
f . (indx CC) in {cb} by A21, A22, A23, CARD_3:9;
hence contradiction by A33, TARSKI:def 1; :: thesis:

end;

hence f . i in CC . i ; :: thesis:

end;

( a1 . (indx CC) in pi (S,(indx CC)) & b1 . (indx CC) in pi (S,(indx CC)) ) by A2, A3, CARD_3:def 6;
then 2 c= card (pi (S,(indx CC))) by A10, Th2;
then reconsider p = pi (S,(indx CC)) as non trivial set by Th4;
CC +* ((indx CC),p) c= Carrier A

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis:
assume A34: i in I ; :: thesis:

per cases ;

suppose A35: i <> indx CC ; :: thesis:

A36: CC c= Carrier A by PBOOLE:def 18;
(CC +* ((indx CC),p)) . i = CC . i by A35, FUNCT_7:32;
hence (CC +* ((indx CC),p)) . i c= (Carrier A) . i by A34, A36; :: thesis:

end;

suppose A37: i = indx CC ; :: thesis:

A38: p c= (Carrier A) . i

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in p ; :: thesis:
then A39: ex f being Function st
( f in S & y = f . i ) by A37, CARD_3:def 6;
i in dom (Carrier A) by A34, PARTFUN1:def 2;
hence y in (Carrier A) . i by A39, CARD_3:9; :: thesis:

end;

dom CC = I by PARTFUN1:def 2;
hence (CC +* ((indx CC),p)) . i c= (Carrier A) . i by A37, A38, FUNCT_7:31; :: thesis:

end;

then reconsider B = CC +* ((indx CC),p) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th27, PBOOLE:def 18;
take B ; :: thesis:
A40: dom B = I by PARTFUN1:def 2;
A41: B . (indx CC) = p by A7, FUNCT_7:31;
thus A42: S = product B :: thesis:

proof

thus S c= product B :: according to XBOOLE_0:def 10 :: thesis:

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A43: e in S ; :: thesis:
then reconsider f = e as ManySortedSet of I by Th14;

A44: now :: thesis:

let i be object ; :: thesis:
assume i in I ; :: thesis:
then reconsider j = i as Element of I ;

per cases ;

suppose j = indx CC ; :: thesis:

hence f . i in B . i by A41, A43, CARD_3:def 6; :: thesis:

end;

suppose A45: j <> indx CC ; :: thesis:

then f . j in CC . j by A13, A43;
hence f . i in B . i by A45, FUNCT_7:32; :: thesis:

end;

dom f = I by PARTFUN1:def 2;
hence e in product B by A40, A44, CARD_3:9; :: thesis:

end;

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in product B ; :: thesis:
then consider f being Function such that
A46: ( e = f & dom f = I ) and
A47: for i being object st i in I holds
f . i in B . i by A40, CARD_3:def 5;
f . (indx CC) in p by A41, A47;
then consider g being Function such that
A48: g in S and
A49: f . (indx CC) = g . (indx CC) by CARD_3:def 6;
reconsider g = g as ManySortedSet of I by A48;

A50: now :: thesis:

let i be object ; :: thesis:
assume i in I ; :: thesis:
then reconsider j = i as Element of I ;

per cases ;

suppose i = indx CC ; :: thesis:

hence f . i = g . i by A49; :: thesis:

end;

suppose A51: i <> indx CC ; :: thesis:

then CC . j is 1 -element by Th12;
then consider c being object such that
A52: CC . i = {c} by ZFMISC_1:131;
A53: g . j in CC . j by A13, A48, A51;
f . j in B . j by A47;
then f . j in {c} by A51, A52, FUNCT_7:32;
hence f . i = c by TARSKI:def 1
.= g . i by A52, A53, TARSKI:def 1 ;
:: thesis:

end;

dom g = I by PARTFUN1:def 2;
hence e in S by A46, A48, A50, FUNCT_1:2; :: thesis:

end;

let SS be Subset of (A . (indx B)); :: thesis:
assume A54: SS = B . (indx B) ; :: thesis:
thus SS is strong :: thesis:

proof

let q, r be Point of (A . (indx B)); :: according to PENCIL_1:def 3 :: thesis:
assume that
A55: q in SS and
A56: r in SS ; :: thesis:
thus q,r are_collinear :: thesis:

proof

per cases ;

suppose q = r ; :: thesis:

hence q,r are_collinear ; :: thesis:

end;

suppose A57: q <> r ; :: thesis:

reconsider R = a1 +* ((indx B),r) as Point of (Segre_Product A) by Th25;
reconsider Q = a1 +* ((indx B),q) as Point of (Segre_Product A) by Th25;
reconsider Q1 = Q, R1 = R as ManySortedSet of I ;

A58: now :: thesis:

dom a1 = I by PARTFUN1:def 2;
then A59: Q1 . (indx B) = q by FUNCT_7:31;
A60: dom a1 = I by PARTFUN1:def 2;
assume Q = R ; :: thesis:
hence contradiction by A57, A59, A60, FUNCT_7:31; :: thesis:

end;

A61: for i being object st i in dom B holds
Q1 . i in B . i

proof

let i be object ; :: thesis:
assume A62: i in dom B ; :: thesis:
then i in I by PARTFUN1:def 2;
then A63: i in dom a1 by PARTFUN1:def 2;

per cases ;

suppose i <> indx B ; :: thesis:

then Q1 . i = a1 . i by FUNCT_7:32;
hence Q1 . i in B . i by A2, A42, A62, CARD_3:9; :: thesis:

end;

suppose i = indx B ; :: thesis:

hence Q1 . i in B . i by A54, A55, A63, FUNCT_7:31; :: thesis:

end;

A64: for i being object st i in dom B holds
R1 . i in B . i

proof

let i be object ; :: thesis:
assume A65: i in dom B ; :: thesis:
then i in I by PARTFUN1:def 2;
then A66: i in dom a1 by PARTFUN1:def 2;

per cases ;

suppose i <> indx B ; :: thesis:

then R1 . i = a1 . i by FUNCT_7:32;
hence R1 . i in B . i by A2, A42, A65, CARD_3:9; :: thesis:

end;

suppose i = indx B ; :: thesis:

hence R1 . i in B . i by A54, A56, A66, FUNCT_7:31; :: thesis:

end;

dom R1 = I by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2 ;
then A67: R in product B by A64, CARD_3:9;
dom Q1 = I by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2 ;
then Q in product B by A61, CARD_3:9;
then Q,R are_collinear by A1, A42, A67;
then consider L being Block of (Segre_Product A) such that
A68: {Q,R} c= L by A58;
dom a1 = I by PARTFUN1:def 2;
then A69: R1 . (indx B) = r by FUNCT_7:31;
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A70: L = product L1 and
A71: L1 . (indx L1) is Block of (A . (indx L1)) by Th24;
A72: dom L1 = I by PARTFUN1:def 2;
Q1 in product L1 by A68, A70, ZFMISC_1:32;
then A73: Q1 . (indx B) in L1 . (indx B) by A72, CARD_3:9;
A74: dom L1 = I by PARTFUN1:def 2;
R1 in product L1 by A68, A70, ZFMISC_1:32;
then A75: R1 . (indx B) in L1 . (indx B) by A74, CARD_3:9;

now :: thesis:

dom a1 = I by PARTFUN1:def 2;
then A76: Q1 . (indx B) = q by FUNCT_7:31;
A77: dom a1 = I by PARTFUN1:def 2;
assume Q1 . (indx B) = R1 . (indx B) ; :: thesis:
hence contradiction by A57, A76, A77, FUNCT_7:31; :: thesis:

end;

then 2 c= card (L1 . (indx B)) by A73, A75, Th2;
then A78: not L1 . (indx B) is trivial by Th4;
then reconsider LI = L1 . (indx L1) as Block of (A . (indx B)) by A71, Def21;
dom a1 = I by PARTFUN1:def 2;
then A79: Q1 . (indx B) = q by FUNCT_7:31;
indx B = indx L1 by A78, Def21;
then {q,r} c= LI by A73, A75, A79, A69, ZFMISC_1:32;
hence q,r are_collinear ; :: thesis:

end;

thus SS is closed_under_lines :: thesis:

proof

let L be Block of (A . (indx B)); :: according to PENCIL_1:def 2 :: thesis:
A80: dom B = I by PARTFUN1:def 2;
2 c= card L by Def6;
then reconsider L1 = L as non trivial set by Th4;
L in the topology of (A . (indx B)) ;
then A81: L c= the carrier of (A . (indx B)) ;
B +* ((indx B),L1) c= Carrier A

proof

let o be object ; :: according to PBOOLE:def 2 :: thesis:
assume A82: o in I ; :: thesis:
thus (B +* ((indx B),L1)) . o c= (Carrier A) . o :: thesis:

proof

per cases ;

suppose A83: o <> indx B ; :: thesis:

A84: B c= Carrier A by PBOOLE:def 18;
(B +* ((indx B),L1)) . o = B . o by A83, FUNCT_7:32;
hence (B +* ((indx B),L1)) . o c= (Carrier A) . o by A82, A84; :: thesis:

end;

suppose A85: o = indx B ; :: thesis:

then (B +* ((indx B),L1)) . o = L by A40, FUNCT_7:31;
hence (B +* ((indx B),L1)) . o c= (Carrier A) . o by A81, A85, YELLOW_6:2; :: thesis:

end;

then reconsider L2 = B +* ((indx B),L1) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by Th27, PBOOLE:def 18;
A86: L2 . (indx B) = L1 by A40, FUNCT_7:31;
then indx B = indx L2 by Def21;
then L2 . (indx L2) is Block of (A . (indx L2)) by A80, FUNCT_7:31;
then reconsider L3 = product L2 as Block of (Segre_Product A) by Th24;
assume 2 c= card (L /\ SS) ; :: thesis:
then consider x, y being object such that
A87: x in L /\ SS and
A88: y in L /\ SS and
A89: x <> y by Th2;
set y1 = a1 +* ((indx B),y);
A90: dom (a1 +* ((indx B),y)) = I by PARTFUN1:def 2;

now :: thesis:

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

per cases ;

suppose o <> indx B ; :: thesis:

then (a1 +* ((indx B),y)) . o = a1 . o by FUNCT_7:32;
hence (a1 +* ((indx B),y)) . o in B . o by A2, A40, A42, A91, CARD_3:9; :: thesis:

end;

suppose A92: o = indx B ; :: thesis:

then (a1 +* ((indx B),y)) . o = y by A8, FUNCT_7:31;
hence (a1 +* ((indx B),y)) . o in B . o by A54, A88, A92, XBOOLE_0:def 4; :: thesis:

end;

then A93: a1 +* ((indx B),y) in S by A40, A42, A90, CARD_3:9;
A94: dom L2 = I by PARTFUN1:def 2;

now :: thesis:

let o be object ; :: thesis:
assume A95: o in dom L2 ; :: thesis:

per cases ;

suppose A96: o <> indx B ; :: thesis:

then A97: (a1 +* ((indx B),y)) . o = a1 . o by FUNCT_7:32;
a1 . o in B . o by A2, A40, A42, A94, A95, CARD_3:9;
hence (a1 +* ((indx B),y)) . o in L2 . o by A96, A97, FUNCT_7:32; :: thesis:

end;

suppose A98: o = indx B ; :: thesis:

then (a1 +* ((indx B),y)) . o = y by A8, FUNCT_7:31;
hence (a1 +* ((indx B),y)) . o in L2 . o by A88, A86, A98, XBOOLE_0:def 4; :: thesis:

end;

then a1 +* ((indx B),y) in L3 by A94, A90, CARD_3:9;
then A99: a1 +* ((indx B),y) in L3 /\ S by A93, XBOOLE_0:def 4;
set x1 = a1 +* ((indx B),x);
A100: dom (a1 +* ((indx B),x)) = I by PARTFUN1:def 2;

now :: thesis:

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

per cases ;

suppose o <> indx B ; :: thesis:

then (a1 +* ((indx B),x)) . o = a1 . o by FUNCT_7:32;
hence (a1 +* ((indx B),x)) . o in B . o by A2, A40, A42, A101, CARD_3:9; :: thesis:

end;

suppose A102: o = indx B ; :: thesis:

then (a1 +* ((indx B),x)) . o = x by A8, FUNCT_7:31;
hence (a1 +* ((indx B),x)) . o in B . o by A54, A87, A102, XBOOLE_0:def 4; :: thesis:

end;

then A103: a1 +* ((indx B),x) in S by A40, A42, A100, CARD_3:9;
A104: ( (a1 +* ((indx B),x)) . (indx B) = x & (a1 +* ((indx B),y)) . (indx B) = y ) by A8, FUNCT_7:31;

now :: thesis:

let o be object ; :: thesis:
assume A105: o in dom L2 ; :: thesis:

per cases ;

suppose A106: o <> indx B ; :: thesis:

then A107: (a1 +* ((indx B),x)) . o = a1 . o by FUNCT_7:32;
a1 . o in B . o by A2, A40, A42, A94, A105, CARD_3:9;
hence (a1 +* ((indx B),x)) . o in L2 . o by A106, A107, FUNCT_7:32; :: thesis:

end;

suppose A108: o = indx B ; :: thesis:

then (a1 +* ((indx B),x)) . o = x by A8, FUNCT_7:31;
hence (a1 +* ((indx B),x)) . o in L2 . o by A87, A86, A108, XBOOLE_0:def 4; :: thesis:

end;

then a1 +* ((indx B),x) in L3 by A94, A100, CARD_3:9;
then a1 +* ((indx B),x) in L3 /\ S by A103, XBOOLE_0:def 4;
then 2 c= card (L3 /\ S) by A89, A104, A99, Th2;
then A109: L3 c= S by A1;
thus L c= SS :: thesis:

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
consider f being object such that
A110: f in L3 by XBOOLE_0:def 1;
A111: ex F being Function st
( F = f & dom F = I & ( for o being object st o in I holds
F . o in L2 . o ) ) by A94, A110, CARD_3:def 5;
then reconsider f = f as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
assume A112: e in L ; :: thesis:

A113: now :: thesis:

let o be object ; :: thesis:
assume A114: o in dom L2 ; :: thesis:

per cases ;

suppose o <> indx B ; :: thesis:

then (f +* ((indx B),e)) . o = f . o by FUNCT_7:32;
hence (f +* ((indx B),e)) . o in L2 . o by A94, A111, A114; :: thesis:

end;

suppose A115: o = indx B ; :: thesis:

then (f +* ((indx B),e)) . o = e by A111, FUNCT_7:31;
hence (f +* ((indx B),e)) . o in L2 . o by A40, A112, A115, FUNCT_7:31; :: thesis:

end;

dom (f +* ((indx B),e)) = dom L2 by A94, PARTFUN1:def 2;
then f +* ((indx B),e) in L3 by A113, CARD_3:9;
then (f +* ((indx B),e)) . (indx B) in B . (indx B) by A40, A42, A109, CARD_3:9;
hence e in SS by A54, A111, FUNCT_7:31; :: thesis:

end;

given B being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A116: S = product B and
A117: for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines ) ; :: thesis:
thus not S is trivial by A116; :: thesis:
A118: dom B = I by PARTFUN1:def 2;
A119: dom (Carrier A) = I by PARTFUN1:def 2;
thus S is strong :: thesis:

proof

let x, y be Point of (Segre_Product A); :: according to PENCIL_1:def 3 :: thesis:
assume that
A120: x in S and
A121: y in S ; :: thesis:

per cases ;

suppose x = y ; :: thesis:

hence x,y are_collinear ; :: thesis:

end;

suppose A122: x <> y ; :: thesis:

consider y1 being Function such that
A123: y1 = y and
A124: dom y1 = dom (Carrier A) and
A125: for a being object st a in dom (Carrier A) holds
y1 . a in (Carrier A) . a by CARD_3:def 5;
A126: dom (Carrier A) = I by PARTFUN1:def 2;
then reconsider y1 = y1 as ManySortedSet of I by A124, PARTFUN1:def 2, RELAT_1:def 18;
consider x1 being Function such that
A127: x1 = x and
A128: dom x1 = dom (Carrier A) and
A129: for a being object st a in dom (Carrier A) holds
x1 . a in (Carrier A) . a by CARD_3:def 5;
reconsider x1 = x1 as ManySortedSet of I by A128, A126, PARTFUN1:def 2, RELAT_1:def 18;

A130: now :: thesis:

assume A131: x1 . (indx B) = y1 . (indx B) ; :: thesis:

now :: thesis:

let i be object ; :: thesis:
assume i in dom (Carrier A) ; :: thesis:

per cases ;

suppose i <> indx B ; :: thesis:

hence x1 . i = y1 . i by A116, A120, A121, A127, A123, Th23; :: thesis:

end;

suppose i = indx B ; :: thesis:

hence x1 . i = y1 . i by A131; :: thesis:

end;

hence contradiction by A122, A127, A128, A123, A124, FUNCT_1:2; :: thesis:

end;

B c= Carrier A by PBOOLE:def 18;
then B . (indx B) c= (Carrier A) . (indx B) ;
then reconsider C = B . (indx B) as Subset of (A . (indx B)) by YELLOW_6:2;
A132: C is strong by A117;
y1 . (indx B) in (Carrier A) . (indx B) by A119, A125;
then reconsider y1i = y1 . (indx B) as Point of (A . (indx B)) by YELLOW_6:2;
A133: y1i in C by A116, A118, A121, A123, CARD_3:9;
x1 . (indx B) in (Carrier A) . (indx B) by A119, A129;
then reconsider x1i = x1 . (indx B) as Point of (A . (indx B)) by YELLOW_6:2;
x1i in C by A116, A118, A120, A127, CARD_3:9;
then x1i,y1i are_collinear by A133, A132;
then consider l being Block of (A . (indx B)) such that
A134: {x1i,y1i} c= l by A130;
A135: dom {x1} = I by PARTFUN1:def 2;
A136: for a being object st a in dom ({x1} +* ((indx B),l)) holds
y1 . a in ({x1} +* ((indx B),l)) . a

proof

let a be object ; :: thesis:
assume a in dom ({x1} +* ((indx B),l)) ; :: thesis:
then A137: a in I by PARTFUN1:def 2;

per cases ;

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

then ({x1} +* ((indx B),l)) . a = l by A135, FUNCT_7:31;
hence y1 . a in ({x1} +* ((indx B),l)) . a by A134, A138, ZFMISC_1:32; :: thesis:

end;

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

x1 . a in {(x1 . a)} by TARSKI:def 1;
then x1 . a in {x1} . a by A137, PZFMISC1:def 1;
then y1 . a in {x1} . a by A116, A120, A121, A127, A123, A139, Th23;
hence y1 . a in ({x1} +* ((indx B),l)) . a by A139, FUNCT_7:32; :: thesis:

end;

{x1} +* ((indx B),l) c= Carrier A

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis:
assume A140: i in I ; :: thesis:
then reconsider i1 = i as Element of I ;
thus ({x1} +* ((indx B),l)) . i c= (Carrier A) . i :: thesis:

proof

per cases ;

suppose A141: i = indx B ; :: thesis:

then ({x1} +* ((indx B),l)) . i = l by A135, FUNCT_7:31;
then ({x1} +* ((indx B),l)) . i in the topology of (A . (indx B)) ;
then ({x1} +* ((indx B),l)) . i c= the carrier of (A . (indx B)) ;
hence ({x1} +* ((indx B),l)) . i c= (Carrier A) . i by A141, YELLOW_6:2; :: thesis:

end;

suppose A142: i <> indx B ; :: thesis:

x1 . i in (Carrier A) . i1 by A119, A129;
then x1 . i in the carrier of (A . i1) by YELLOW_6:2;
then A143: {(x1 . i)} c= the carrier of (A . i1) by ZFMISC_1:31;
({x1} +* ((indx B),l)) . i = {x1} . i by A142, FUNCT_7:32
.= {(x1 . i)} by A140, PZFMISC1:def 1 ;
hence ({x1} +* ((indx B),l)) . i c= (Carrier A) . i by A143, YELLOW_6:2; :: thesis:

end;

then A144: {x1} +* ((indx B),l) is ManySortedSubset of Carrier A by PBOOLE:def 18;
for i being Element of I st i <> indx B holds
({x1} +* ((indx B),l)) . i is 1 -element

proof

let i be Element of I; :: thesis:
assume i <> indx B ; :: thesis:
then ({x1} +* ((indx B),l)) . i = {x1} . i by FUNCT_7:32
.= {(x1 . i)} by PZFMISC1:def 1 ;
hence ({x1} +* ((indx B),l)) . i is 1 -element ; :: thesis:

end;

then A145: {x1} +* ((indx B),l) is Segre-like ;
A146: for a being object st a in dom ({x1} +* ((indx B),l)) holds
x1 . a in ({x1} +* ((indx B),l)) . a

proof

let a be object ; :: thesis:
assume a in dom ({x1} +* ((indx B),l)) ; :: thesis:
then A147: a in I by PARTFUN1:def 2;

per cases ;

suppose A148: a = indx B ; :: thesis:

then ({x1} +* ((indx B),l)) . a = l by A135, FUNCT_7:31;
hence x1 . a in ({x1} +* ((indx B),l)) . a by A134, A148, ZFMISC_1:32; :: thesis:

end;

suppose A149: a <> indx B ; :: thesis:

x1 . a in {(x1 . a)} by TARSKI:def 1;
then x1 . a in {x1} . a by A147, PZFMISC1:def 1;
hence x1 . a in ({x1} +* ((indx B),l)) . a by A149, FUNCT_7:32; :: thesis:

end;

({x1} +* ((indx B),l)) . (indx B) is Block of (A . (indx B)) by A135, FUNCT_7:31;
then reconsider L = product ({x1} +* ((indx B),l)) as Block of (Segre_Product A) by A145, A144, Def22;
dom y1 = I by PARTFUN1:def 2
.= dom ({x1} +* ((indx B),l)) by PARTFUN1:def 2 ;
then A150: y1 in L by A136, CARD_3:9;
dom x1 = I by PARTFUN1:def 2
.= dom ({x1} +* ((indx B),l)) by PARTFUN1:def 2 ;
then x1 in L by A146, CARD_3:9;
then {x,y} c= L by A127, A123, A150, ZFMISC_1:32;
hence x,y are_collinear ; :: thesis:

end;

thus S is closed_under_lines :: thesis:

proof

let l be Block of (Segre_Product A); :: according to PENCIL_1:def 2 :: thesis:
consider L being Segre-like ManySortedSubset of Carrier A such that
A151: l = product L and
A152: ex i being Element of I st L . i is Block of (A . i) by Def22;
assume A153: 2 c= card (l /\ S) ; :: thesis:
then consider a, b being object such that
A154: a in l /\ S and
A155: b in l /\ S and
A156: a <> b by Th2;
card (l /\ S) c= card l by CARD_1:11, XBOOLE_1:17;
then 2 c= card l by A153;
then reconsider L = L as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A151, Th13;
reconsider a1 = a, b1 = b as ManySortedSet of I by A154, A155, Th14;
A157: dom L = I by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2 ;
A158: indx B = indx L by A116, A153, A151, Th26;
for a being object st a in dom L holds
L . a c= B . a

proof

let a be object ; :: thesis:
assume a in dom L ; :: thesis:

per cases ;

suppose a <> indx B ; :: thesis:

hence L . a c= B . a by A116, A153, A151, Th26; :: thesis:

end;

suppose A159: a = indx B ; :: thesis:

B c= Carrier A by PBOOLE:def 18;
then B . (indx B) c= (Carrier A) . (indx B) ;
then reconsider C = B . (indx B) as Subset of (A . (indx B)) by YELLOW_6:2;
consider j being Element of I such that
A160: L . j is Block of (A . j) by A152;
2 c= card (L . j) by A160, Def6;
then not L . j is trivial by Th4;
then j = indx L by Def21;
then reconsider Li = L . (indx B) as Block of (A . (indx B)) by A158, A160;
A161: C is closed_under_lines by A117;
a1 in product L by A154, A151, XBOOLE_0:def 4;
then A162: a1 . (indx B) in L . (indx B) by A118, A157, CARD_3:9;
b1 in product L by A155, A151, XBOOLE_0:def 4;
then A163: b1 . (indx B) in L . (indx B) by A118, A157, CARD_3:9;
A164: b1 in product B by A116, A155, XBOOLE_0:def 4;
then b1 . (indx B) in B . (indx B) by A118, CARD_3:9;
then A165: b1 . (indx B) in Li /\ C by A163, XBOOLE_0:def 4;
A166: a1 in product B by A116, A154, XBOOLE_0:def 4;

A167: now :: thesis:

assume A168: a1 . (indx B) = b1 . (indx B) ; :: thesis:
A169: for o being object st o in dom a1 holds
a1 . o = b1 . o

proof

let o be object ; :: thesis:
assume o in dom a1 ; :: thesis:

per cases ;

suppose o <> indx B ; :: thesis:

hence a1 . o = b1 . o by A166, A164, Th23; :: thesis:

end;

suppose o = indx B ; :: thesis:

hence a1 . o = b1 . o by A168; :: thesis:

end;

dom a1 = I by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2 ;
hence contradiction by A156, A169, FUNCT_1:2; :: thesis:

end;

a1 . (indx B) in B . (indx B) by A118, A166, CARD_3:9;
then a1 . (indx B) in Li /\ C by A162, XBOOLE_0:def 4;
then 2 c= card (Li /\ C) by A167, A165, Th2;
hence L . a c= B . a by A159, A161; :: thesis:

end;

hence l c= S by A116, A151, A157, CARD_3:27; :: thesis:

end;