:: On Segre's Product of Partial Line Spaces
:: by Adam Naumowicz
::
:: Received May 29, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, CARD_3, RELAT_1, XBOOLE_0, TARSKI, CARD_1,
ZFMISC_1, SUBSET_1, PRE_TOPC, STRUCT_0, RELAT_2, FINSEQ_1, NAT_1,
XXREAL_0, ARYTM_3, FINSET_1, SETFAM_1, PRALG_1, PBOOLE, FUNCOP_1,
WAYBEL_3, FUNCT_4, RLVECT_2, INTEGRA1, ARYTM_1, ORDINAL4, PENCIL_1,
WAYBEL18;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, XCMPLX_0, SETFAM_1,
CARD_1, ORDINAL1, NUMBERS, NAT_1, FINSET_1, RELAT_1, DOMAIN_1, STRUCT_0,
FUNCT_1, PBOOLE, FUNCT_7, WAYBEL_3, FINSEQ_1, CARD_3, PRE_TOPC, PZFMISC1,
FUNCOP_1, PRALG_1, XXREAL_0, WAYBEL18;
constructors PZFMISC1, REALSET2, PRALG_1, WAYBEL_3, POLYNOM1, PBOOLE, FUNCT_7,
FUNCT_4, RELSET_1, SETFAM_1, WAYBEL18;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XREAL_0, CARD_3,
PZFMISC1, STRUCT_0, YELLOW_6, ORDINAL1, CARD_1, ZFMISC_1, PRE_POLY,
FUNCOP_1, WAYBEL18;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
definitions TARSKI, PBOOLE, XBOOLE_0;
equalities STRUCT_0, ORDINAL1;
expansions TARSKI, WAYBEL_3, PBOOLE, XBOOLE_0, WAYBEL18;
theorems TARSKI, FUNCT_1, FUNCOP_1, PBOOLE, CARD_3, PRALG_1, STRUCT_0, CARD_1,
YELLOW11, ENUMSET1, FINSEQ_1, CARD_2, ZFMISC_1, NAT_1, FUNCT_7, YELLOW_6,
PZFMISC1, PUA2MSS1, FINSEQ_3, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, ORDINAL1, PARTFUN1, SUBSET_1, WAYBEL18;
schemes FINSEQ_1, XBOOLE_0;
begin
theorem Th1:
for f,g being Function st product f = product g holds f is
non-empty implies g is non-empty
proof
let f,g be Function;
assume
A1: product f = product g;
now
assume that
A2: f is non-empty and
A3: not g is non-empty;
ex n being object st n in dom g & g.n is empty by A3,FUNCT_1:def 9;
then {} in rng g by FUNCT_1:def 3;
then product g = {} by CARD_3:26;
then {} in rng f by A1,CARD_3:26;
then ex n being object st n in dom f & f.n = {} by FUNCT_1:def 3;
hence contradiction by A2,FUNCT_1:def 9;
end;
hence thesis;
end;
theorem Th2:
for X being set holds 2 c= card X iff ex x,y being object st x in X
& y in X & x<>y
proof
let X be set;
thus 2 c= card X implies ex x,y being object st x in X & y in X & x<>y
proof
assume 2 c= card X;
then card 2 c= card X;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = 2 and
A3: rng f c= X by CARD_1:10;
take x=f.0;
take y=f.1;
A4: 0 in dom f by A2,CARD_1:50,TARSKI:def 2;
then f.0 in rng f by FUNCT_1:def 3;
hence x in X by A3;
A5: 1 in dom f by A2,CARD_1:50,TARSKI:def 2;
then f.1 in rng f by FUNCT_1:def 3;
hence y in X by A3;
thus thesis by A1,A4,A5,FUNCT_1:def 4;
end;
given x,y being object such that
A6: x in X & y in X and
A7: x<>y;
{x,y} c= X
by A6,TARSKI:def 2;
then card {x,y} c= card X by CARD_1:11;
hence thesis by A7,CARD_2:57;
end;
theorem Th3:
for X being set st 2 c= card X for x being object ex y being object st
y in X & x<>y
proof
let X be set;
assume 2 c= card X;
then consider a,b being object such that
A1: a in X and
A2: b in X & a <> b by Th2;
let x be object;
per cases;
suppose
A3: x=a;
take b;
thus thesis by A2,A3;
end;
suppose
A4: x <> a;
take a;
thus thesis by A1,A4;
end;
end;
theorem Th4:
for X being set holds 2 c= card X iff X is non trivial
proof
let X be set;
set z = the Element of X;
thus 2 c= card X implies X is non trivial
proof
assume 2 c= card X;
then consider x,y being object such that
A1: x in X and
A2: y in X and
A3: x<>y by Th2;
now
given z being object such that
A4: X={z};
thus x = z by A1,A4,TARSKI:def 1
.= y by A2,A4,TARSKI:def 1;
end;
hence thesis by A1,A3,ZFMISC_1:131;
end;
assume
A5: X is non trivial;
then X c= {z} implies X={z};
then consider w being object such that
A6: w in X and
A7: not w in {z} by A5;
w <> z by A7,TARSKI:def 1;
hence thesis by A6,Th2;
end;
theorem Th5:
for X being set holds 3 c= card X iff ex x,y,z being object st x in
X & y in X & z in X & x<>y & x<>z & y<>z
proof
let X be set;
thus 3 c= card X implies
ex x,y,z being object st x in X & y in X & z in X & x
<>y & x<>z & y<>z
proof
assume 3 c= card X;
then card 3 c= card X;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = 3 and
A3: rng f c= X by CARD_1:10;
take x=f.0;
take y=f.1;
take z=f.2;
A4: 0 in dom f by A2,ENUMSET1:def 1,YELLOW11:1;
then f.0 in rng f by FUNCT_1:def 3;
hence x in X by A3;
A5: 1 in dom f by A2,ENUMSET1:def 1,YELLOW11:1;
then f.1 in rng f by FUNCT_1:def 3;
hence y in X by A3;
A6: 2 in dom f by A2,ENUMSET1:def 1,YELLOW11:1;
then f.2 in rng f by FUNCT_1:def 3;
hence z in X by A3;
thus x <> y by A1,A4,A5,FUNCT_1:def 4;
thus x <> z by A1,A4,A6,FUNCT_1:def 4;
thus thesis by A1,A5,A6,FUNCT_1:def 4;
end;
given x,y,z being object such that
A7: x in X & y in X & z in X and
A8: x<>y & x<>z & y<>z;
{x,y,z} c= X
by A7,ENUMSET1:def 1;
then card {x,y,z} c= card X by CARD_1:11;
hence thesis by A8,CARD_2:58;
end;
theorem Th6:
for X being set st 3 c= card X for x,y being object ex z being object
st z in X & x<>z & y<>z
proof
let X be set;
assume 3 c= card X;
then consider a,b,c being object such that
A1: a in X and
A2: b in X and
A3: c in X and
A4: a<>b and
A5: a<>c & b<>c by Th5;
let x,y be object;
per cases;
suppose
x <> a & y <> a;
hence thesis by A1;
end;
suppose
x <> a & y = a & x = b;
hence thesis by A3,A5;
end;
suppose
x <> a & y = a & x <> b;
hence thesis by A2,A4;
end;
suppose
x = a & y <> a & y=b;
hence thesis by A3,A5;
end;
suppose
x = a & y <> a & y<>b;
hence thesis by A2,A4;
end;
suppose
x = a & y = a;
hence thesis by A2,A4;
end;
end;
begin
definition
let S be TopStruct;
mode Block of S is Element of the topology of S;
end;
definition
let S be TopStruct;
let x,y be Point of S;
pred x,y are_collinear means
x=y or ex l being Block of S st {x,y} c= l;
end;
definition
let S be TopStruct;
let T be Subset of S;
attr T is closed_under_lines means
for l being Block of S st 2 c= card (l /\ T) holds l c= T;
attr T is strong means
for x,y being Point of S st x in T & y in T holds x,y are_collinear;
end;
definition
let S be TopStruct;
attr S is void means
:Def4:
the topology of S is empty;
attr S is degenerated means
the carrier of S is Block of S;
attr S is with_non_trivial_blocks means
:Def6:
for k being Block of S holds 2 c= card k;
attr S is identifying_close_blocks means
:Def7:
for k,l being Block of S st 2 c= card(k /\ l) holds k=l;
attr S is truly-partial means
ex x,y being Point of S st not x,y are_collinear;
attr S is without_isolated_points means
:Def9:
for x being Point of S ex l being Block of S st x in l;
attr S is connected means
for x,y being Point of S ex f being FinSequence of
the carrier of S st x=f.1 & y=f.(len f) & for i being Nat st 1 <= i & i < len f
for a,b being Point of S st a = f.i & b = f.(i+1) holds a,b are_collinear;
attr S is strongly_connected means
for x being Point of S for X
being Subset of S st X is closed_under_lines strong ex f being FinSequence of
bool the carrier of S st X = f.1 & x in f.(len f) & (for W being Subset of S st
W in rng f holds W is closed_under_lines strong) & for i being Nat st 1 <= i &
i < len f holds 2 c= card((f.i) /\ (f.(i+1)));
end;
theorem Th7:
for X being non empty set st 3 c= card X
for S being TopStruct st
the carrier of S = X & the topology of S = {L where L is Subset of X : 2 = card
L} holds S is non empty non void non degenerated non truly-partial
with_non_trivial_blocks identifying_close_blocks without_isolated_points
proof
let X be non empty set;
assume
A1: 3 c= card X;
A2: Segm 2 c= Segm 3 by NAT_1:39;
then 2 c= card X by A1;
then consider x,y being object such that
A3: x in X & y in X and
A4: x <> y by Th2;
{x,y} c= X
by A3,TARSKI:def 2;
then reconsider l = {x,y} as Subset of X;
let S be TopStruct;
assume that
A5: the carrier of S = X and
A6: the topology of S = {L where L is Subset of X : 2 = card L};
thus S is non empty by A5;
2 = card l by A4,CARD_2:57;
then
A7: l in the topology of S by A6;
then reconsider
F={L where L is Subset of X : 2 = card L} as non empty set by A6;
thus S is non void by A7;
now
assume X in F;
then ex L being Subset of X st X=L & 2 = card L;
then Segm 3 c= Segm 2 by A1;
hence contradiction by NAT_1:39;
end;
then not X is Element of F;
hence S is non degenerated by A5,A6;
for x,y being Point of S holds x,y are_collinear
proof
let x,y be Point of S;
per cases;
suppose
A8: x=y;
consider z being object such that
A9: z in X and
A10: z <> x by A1,A2,Th3,XBOOLE_1:1;
reconsider z as Point of S by A5,A9;
A11: {x,y} c= {x,z}
proof
let a be object;
assume a in {x,y};
then a=x or a=y by TARSKI:def 2;
hence thesis by A8,TARSKI:def 2;
end;
{x,z} c= X
proof
let a be object;
assume a in {x,z};
then a = x or a = z by TARSKI:def 2;
hence thesis by A5;
end;
then reconsider l = {x,z} as Subset of X;
card l = 2 by A10,CARD_2:57;
then l in the topology of S by A6;
hence thesis by A11;
end;
suppose
A12: x<>y;
{x,y} c= X
proof
let a be object;
assume a in {x,y};
then a=x or a=y by TARSKI:def 2;
hence thesis by A5;
end;
then reconsider l = {x,y} as Subset of X;
card {x,y} = 2 by A12,CARD_2:57;
then l in the topology of S by A6;
hence thesis;
end;
end;
hence S is non truly-partial;
thus S is with_non_trivial_blocks
proof
let k be Block of S;
k in the topology of S by A7;
then ex m being Subset of X st m = k & card m = 2 by A6;
hence thesis;
end;
thus S is identifying_close_blocks
proof
let k,l be Block of S;
assume 2 c= card(k /\ l);
then consider a,b being object such that
A13: a in k /\ l & b in k /\ l and
A14: a <> b by Th2;
A15: {a,b} c= k /\ l
by A13,TARSKI:def 2;
l in the topology of S by A7;
then
A16: ex n being Subset of X st n = l & card n = 2 by A6;
then reconsider l1=l as finite set;
A17: k /\ l c= l1 by XBOOLE_1:17;
k in the topology of S by A7;
then
A18: ex m being Subset of X st m = k & card m = 2 by A6;
then reconsider k1=k as finite set;
A19: card {a,b} = 2 by A14,CARD_2:57;
k /\ l c= k1 by XBOOLE_1:17;
then {a,b} = k1 by A18,A15,A19,CARD_2:102,XBOOLE_1:1;
hence thesis by A15,A19,A16,A17,CARD_2:102,XBOOLE_1:1;
end;
thus S is without_isolated_points
proof
let x be Point of S;
consider z being object such that
A20: z in X and
A21: z <> x by A1,A2,Th3,XBOOLE_1:1;
{x,z} c= X
proof
let a be object;
assume a in {x,z};
then a=x or a=z by TARSKI:def 2;
hence thesis by A5,A20;
end;
then reconsider l = {x,z} as Subset of X;
card {x,z} = 2 by A21,CARD_2:57;
then l in the topology of S by A6;
then reconsider l as Block of S;
take l;
thus thesis by TARSKI:def 2;
end;
end;
theorem Th8:
for X being non empty set st 3 c= card X
for K being Subset of X st card K = 2
for S being TopStruct st the carrier of S = X & the topology of S
= {L where L is Subset of X : 2 = card L} \ {K} holds S is non empty non void
non degenerated truly-partial with_non_trivial_blocks identifying_close_blocks
without_isolated_points
proof
let X be non empty set;
assume
A1: 3 c= card X;
let K be Subset of X;
assume
A2: card K = 2;
then reconsider K9=K as finite Subset of X;
consider x,y being object such that
A3: x <> y and
A4: K9 = {x,y} by A2,CARD_2:60;
let S be TopStruct;
assume that
A5: the carrier of S = X and
A6: the topology of S = {L where L is Subset of X : 2 = card L} \ {K};
reconsider x,y as Point of S by A5,A4,ZFMISC_1:32;
consider z being object such that
A7: z in X and
A8: z <> x and
A9: z <> y by A1,Th6;
{x,z} c= X
proof
let a be object;
assume a in {x,z};
then a=x or a=z by TARSKI:def 2;
hence thesis by A5,A7;
end;
then reconsider l = {x,z} as Subset of X;
card l = 2 by A8,CARD_2:57;
then
A10: z in l & l in {L where L is Subset of X : 2 = card L} by TARSKI:def 2;
thus S is non empty by A5;
not z in K9 by A4,A8,A9,TARSKI:def 2;
then
A11: not {L where L is Subset of X : 2 = card L} c= {K} by A10,TARSKI:def 1;
then
A12: {L where L is Subset of X : 2 = card L} \ {K} is non empty by XBOOLE_1:37;
hence S is non void by A6;
reconsider F={L where L is Subset of X : 2 = card L} \ {K} as non empty set
by A11,XBOOLE_1:37;
now
assume X in F;
then X in {L where L is Subset of X : 2 = card L};
then ex L being Subset of X st X=L & 2 = card L;
then Segm 3 c= Segm 2 by A1;
hence contradiction by NAT_1:39;
end;
then not X is Element of F;
hence S is non degenerated by A5,A6;
thus S is truly-partial
proof
take x,y;
for l being Block of S holds not {x,y} c= l
proof
let l be Block of S;
l in {L where L is Subset of X : 2 = card L} by A6,A12,XBOOLE_0:def 5;
then consider L being Subset of X such that
A13: l = L and
A14: card L = 2;
reconsider L9=L as finite Subset of X by A14;
consider a,b being object such that
a <> b and
A15: L9 = {a,b} by A14,CARD_2:60;
A16: not l in {K} by A6,A12,XBOOLE_0:def 5;
now
assume
A17: {x,y} c= l;
then y in L9 by A13,ZFMISC_1:32;
then
A18: y = a or y = b by A15,TARSKI:def 2;
x in L9 by A13,A17,ZFMISC_1:32;
then x = a or x = b by A15,TARSKI:def 2;
hence contradiction by A3,A4,A16,A13,A15,A18,TARSKI:def 1;
end;
hence thesis;
end;
hence thesis by A3;
end;
thus S is with_non_trivial_blocks
proof
let k be Block of S;
k in {L where L is Subset of X : 2 = card L} by A6,A12,XBOOLE_0:def 5;
then ex m being Subset of X st m = k & card m = 2;
hence thesis;
end;
thus S is identifying_close_blocks
proof
let k,l be Block of S;
assume 2 c= card(k /\ l);
then consider a,b being object such that
A19: a in k /\ l & b in k /\ l and
A20: a <> b by Th2;
A21: {a,b} c= k /\ l
by A19,TARSKI:def 2;
l in {L where L is Subset of X : 2 = card L} by A6,A12,XBOOLE_0:def 5;
then
A22: ex n being Subset of X st n = l & card n = 2;
then reconsider l1=l as finite set;
A23: k /\ l c= l1 by XBOOLE_1:17;
k in {L where L is Subset of X : 2 = card L} by A6,A12,XBOOLE_0:def 5;
then
A24: ex m being Subset of X st m = k & card m = 2;
then reconsider k1=k as finite set;
A25: card {a,b} = 2 by A20,CARD_2:57;
k /\ l c= k1 by XBOOLE_1:17;
then {a,b} = k1 by A24,A21,A25,CARD_2:102,XBOOLE_1:1;
hence thesis by A21,A25,A22,A23,CARD_2:102,XBOOLE_1:1;
end;
A26: Segm 2 c= Segm 3 by NAT_1:39;
thus S is without_isolated_points
proof
let p be Point of S;
per cases;
suppose
A27: p <> x & p <> y;
consider z being object such that
A28: z in X and
A29: z <> p by A1,A26,Th3,XBOOLE_1:1;
{p,z} c= X
proof
let a be object;
assume a in {p,z};
then a=p or a=z by TARSKI:def 2;
hence thesis by A5,A28;
end;
then reconsider el = {p,z} as Subset of X;
card {p,z} = 2 by A29,CARD_2:57;
then
A30: el in {L where L is Subset of X : 2 = card L};
p in el by TARSKI:def 2;
then el <> K by A4,A27,TARSKI:def 2;
then not el in {K} by TARSKI:def 1;
then reconsider el as Block of S by A6,A30,XBOOLE_0:def 5;
take el;
thus thesis by TARSKI:def 2;
end;
suppose
A31: p=x or p=y;
consider z being object such that
A32: z in X and
A33: z <> x & z <> y by A1,Th6;
{p,z} c= X
proof
let a be object;
assume a in {p,z};
then a=p or a=z by TARSKI:def 2;
hence thesis by A5,A32;
end;
then reconsider el = {p,z} as Subset of X;
card {p,z} = 2 by A31,A33,CARD_2:57;
then
A34: el in {L where L is Subset of X : 2 = card L};
z in el by TARSKI:def 2;
then el <> K by A4,A33,TARSKI:def 2;
then not el in {K} by TARSKI:def 1;
then reconsider el as Block of S by A6,A34,XBOOLE_0:def 5;
take el;
thus thesis by TARSKI:def 2;
end;
end;
end;
registration
cluster strict non empty non void non degenerated non truly-partial
with_non_trivial_blocks identifying_close_blocks without_isolated_points
for TopStruct;
existence
proof
{L where L is Subset of Segm 3 : 2 = card L} c= bool 3
proof
let x be object;
assume x in {L where L is Subset of Segm 3 : 2 = card L};
then ex L being Subset of 3 st x=L & 2 = card L;
hence thesis;
end;
then reconsider
B = {L where L is Subset of 3 : 2 = card L} as Subset-Family of 3;
take TopStruct(# 3, B #);
3 = card 3;
then for S being TopStruct st
the carrier of S = Segm 3 & the topology of
S = {L where L is Subset of Segm 3 : 2 = card L}
holds S is non empty non void non degenerated non truly-partial
with_non_trivial_blocks identifying_close_blocks without_isolated_points
by Th7;
hence thesis;
end;
cluster strict non empty non void non degenerated truly-partial
with_non_trivial_blocks identifying_close_blocks without_isolated_points
for TopStruct;
existence
proof
Segm 2 c= Segm 3 & card 2 = 2 by NAT_1:39;
then consider K being Subset of 3 such that
A1: card K = 2;
{L where L is Subset of 3 : 2 = card L} c= bool 3
proof
let x be object;
assume x in {L where L is Subset of 3 : 2 = card L};
then ex L being Subset of 3 st x=L & 2 = card L;
hence thesis;
end;
then reconsider
B = {L where L is Subset of Segm 3 : 2 = card L}\{K} as Subset-Family
of Segm 3 by XBOOLE_1:1;
take TopStruct(# Segm 3, B #);
3 c= card 3;
then for K being Subset of Segm 3 st card K = 2
for S being TopStruct st the carrier of S = Segm 3 & the topology of S
= {L where L is Subset of Segm 3 : 2 = card L} \ {K}
holds S is non empty non void
non degenerated truly-partial with_non_trivial_blocks identifying_close_blocks
without_isolated_points by Th8;
hence thesis by A1;
end;
end;
registration
let S be non void TopStruct;
cluster the topology of S -> non empty;
coherence by Def4;
end;
definition
let S be without_isolated_points TopStruct;
let x,y be Point of S;
redefine pred x,y are_collinear means :: redefines are_collinear (PENCIL_1, definition)
ex l being Block of S st {x,y} c= l;
compatibility
proof
thus x,y are_collinear implies ex l being Block of S st {x,y} c= l
proof
assume
A1: x,y are_collinear;
per cases;
suppose
A2: x=y;
consider l being Block of S such that
A3: x in l by Def9;
take l;
thus thesis by A2,A3,ZFMISC_1:32;
end;
suppose
x<>y;
hence thesis by A1;
end;
end;
given l being Block of S such that
A4: {x,y} c= l;
thus thesis by A4;
end;
end;
definition
mode PLS is non empty non void non degenerated with_non_trivial_blocks
identifying_close_blocks TopStruct;
end;
definition
::$CD
let F be Relation;
attr F is non-void-yielding means
for S being TopStruct st S in rng F holds S is non void;
end;
definition
let F be TopStruct-yielding Function;
redefine attr F is non-void-yielding means :: redefines non-void-yielding (PENCIL_1, definition)
for i being set st i in rng F holds i is non void TopStruct;
compatibility by WAYBEL18:def 1;
end;
definition
let F be Relation;
attr F is trivial-yielding means
:Def16:
for S being set st S in rng F holds S is trivial;
end;
definition
let F be Relation;
attr F is non-Trivial-yielding means
:Def17:
for S being 1-sorted st S in rng F holds S is non trivial;
end;
registration
cluster non-Trivial-yielding -> non-Empty for Relation;
coherence;
end;
definition
let F be 1-sorted-yielding Function;
redefine attr F is non-Trivial-yielding means :: redefines non-Trivial-yielding (PENCIL_1, definition)
for i being set st i in rng F holds i is non trivial 1-sorted;
compatibility by PRALG_1:def 11;
end;
definition
let I be non empty set;
let A be TopStruct-yielding ManySortedSet of I;
let j be Element of I;
redefine func A.j -> TopStruct; :: redefines . (FUNCT_1, definition)
coherence
proof
dom A = I by PARTFUN1:def 2;
then A.j in rng A by FUNCT_1:def 3;
hence thesis;
end;
end;
definition
let F be Relation;
attr F is PLS-yielding means
:Def19:
for x being set st x in rng F holds x is PLS;
end;
registration
cluster PLS-yielding -> non-Empty TopStruct-yielding for Function;
coherence;
cluster PLS-yielding -> non-void-yielding for TopStruct-yielding Function;
coherence;
cluster PLS-yielding -> non-Trivial-yielding for
TopStruct-yielding Function;
coherence
proof
let f be TopStruct-yielding Function such that
A1: f is PLS-yielding;
let x be set;
assume x in rng f;
then reconsider
S1=x as with_non_trivial_blocks non void non empty TopStruct by A1;
consider s being object such that
A2: s in the topology of S1 by XBOOLE_0:def 1;
reconsider s as Block of S1 by A2;
2 c= card s by Def6;
then ex s1,s2 being object st s1 in s & s2 in s & s1 <> s2 by Th2;
hence thesis by A2,STRUCT_0:def 10;
end;
end;
registration
let I be set;
cluster PLS-yielding for ManySortedSet of I;
existence
proof
set R = the PLS;
take I --> R;
let v be set;
assume
A1: v in rng(I-->R);
rng(I-->R) c= {R} by FUNCOP_1:13;
hence thesis by A1,TARSKI:def 1;
end;
end;
definition
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let j be Element of I;
redefine func A.j -> PLS; :: redefines . (FUNCT_1, definition)
coherence
proof
dom A = I by PARTFUN1:def 2;
then A.j in rng A by FUNCT_1:def 3;
hence thesis by Def19;
end;
end;
definition
let I be set;
let A be ManySortedSet of I;
attr A is Segre-like means
:Def20:
ex i being Element of I st for j being
Element of I st i<>j holds A.j is 1-element;
end;
registration
let I be set;
let A be ManySortedSet of I;
cluster {A} -> trivial-yielding;
coherence
proof
let a be set;
assume a in rng {A};
then consider i being object such that
A1: i in dom {A} & a = {A}.i by FUNCT_1:def 3;
dom {A} = I by PARTFUN1:def 2;
then a = {A.i} by A1,PZFMISC1:def 1;
hence thesis;
end;
end;
theorem
for I being non empty set for A being ManySortedSet of I for i being
Element of I for S being non trivial set holds A+*(i,S) is non trivial-yielding
proof
let I be non empty set;
let A be ManySortedSet of I;
let i be Element of I;
let S be non trivial set;
take a = A+*(i,S).i;
dom A = I by PARTFUN1:def 2;
then i in dom A;
then i in dom (A+*(i,S)) by FUNCT_7:30;
hence a in rng (A+*(i,S)) by FUNCT_1:def 3;
dom A = I by PARTFUN1:def 2;
hence thesis by FUNCT_7:31;
end;
registration
let I be non empty set;
let A be ManySortedSet of I;
cluster {A} -> Segre-like;
coherence
proof
set i = the Element of I;
take i;
let j be Element of I such that
i<>j;
{A}.j = {A.j} by PZFMISC1:def 1;
hence thesis;
end;
end;
theorem
for I being non empty set for A being ManySortedSet of I for i,S be
set holds {A}+*(i,S) is Segre-like
proof
let I be non empty set;
let A be ManySortedSet of I;
let i,S be set;
per cases;
suppose
not i in I;
then not i in dom {A} by PARTFUN1:def 2;
hence thesis by FUNCT_7:def 3;
end;
suppose
i in I;
then reconsider i as Element of I;
take i;
let j be Element of I such that
A1: i<>j;
{A}.j = {A.j} by PZFMISC1:def 1;
hence thesis by A1,FUNCT_7:32;
end;
end;
theorem Th11:
for I being non empty set for A being non-Empty
1-sorted-yielding ManySortedSet of I for B being Element of Carrier A holds {B
} is ManySortedSubset of Carrier A
proof
let I be non empty set;
let A be non-Empty 1-sorted-yielding ManySortedSet of I;
let B be Element of Carrier A;
{B} c= Carrier A
proof
let i be object;
assume
A1: i in I;
then reconsider j=i as Element of I;
j in dom A by A1,PARTFUN1:def 2;
then A.j in rng A by FUNCT_1:def 3;
then
A2: A.j is non empty by YELLOW_6:def 2;
B.j is Element of (Carrier A).j by PBOOLE:def 14;
then B.j is Element of A.j by YELLOW_6:2;
then {B.j} c= the carrier of A.j by A2,ZFMISC_1:31;
then {B}.j c= the carrier of A.j by PZFMISC1:def 1;
hence thesis by YELLOW_6:2;
end;
hence thesis by PBOOLE:def 18;
end;
registration
let I be non empty set;
let A be non-Empty 1-sorted-yielding ManySortedSet of I;
cluster Segre-like trivial-yielding non-empty for
ManySortedSubset of Carrier A;
existence
proof
set B = the Element of Carrier A;
reconsider C={B} as ManySortedSubset of Carrier A by Th11;
take C;
thus thesis;
end;
end;
registration
let I be non empty set;
let A be non-Trivial-yielding 1-sorted-yielding ManySortedSet of I;
cluster Segre-like non trivial-yielding non-empty for ManySortedSubset of
Carrier A;
existence
proof
set B = the Element of Carrier A;
set i1 = the Element of I;
A1: ex R being 1-sorted st R=A.i1 & the carrier of R = ( Carrier A).i1 by
PRALG_1:def 15;
then reconsider b1=B.i1 as Element of A.i1 by PBOOLE:def 14;
reconsider B as ManySortedSet of I;
dom A = I by PARTFUN1:def 2;
then A.i1 in rng A by FUNCT_1:def 3;
then A.i1 is non trivial by Def17;
then reconsider Ai1=the carrier of A.i1 as non trivial set;
ex x1,x2 being Element of Ai1 st x1 <> x2 by SUBSET_1:def 7;
then 2 c= card the carrier of (A.i1) by Th2;
then consider b2 being object such that
A2: b2 in the carrier of (A.i1) and
A3: b1 <> b2 by Th3;
reconsider b2 as Element of A.i1 by A2;
set B1=B+*(i1,b2);
A4: for i being set st i in I holds B1.i is Element of (Carrier A).i
proof
let i be set such that
A5: i in I;
per cases;
suppose
i <> i1;
then B1.i = B.i by FUNCT_7:32;
hence thesis by A5,PBOOLE:def 14;
end;
suppose
A6: i = i1;
then i1 in dom B by A5,PARTFUN1:def 2;
hence thesis by A1,A6,FUNCT_7:31;
end;
end;
{B,B1} c= Carrier A
proof
let i be object;
assume
A7: i in I;
then reconsider j=i as Element of I;
j in dom A by A7,PARTFUN1:def 2;
then A.j in rng A by FUNCT_1:def 3;
then
A8: A.j is non empty by YELLOW_6:def 2;
B.j is Element of (Carrier A).j by PBOOLE:def 14;
then
A9: B.j is Element of A.j by YELLOW_6:2;
B1.j is Element of (Carrier A).j by A4;
then B1.j is Element of A.j by YELLOW_6:2;
then {B.j,B1.j} c= the carrier of A.j by A8,A9,ZFMISC_1:32;
then {B,B1}.j c= the carrier of A.j by PZFMISC1:def 2;
hence thesis by YELLOW_6:2;
end;
then reconsider C = {B,B1} as ManySortedSubset of Carrier A by
PBOOLE:def 18;
dom B = I by PARTFUN1:def 2;
then B1.i1 = b2 by FUNCT_7:31;
then
A10: C.i1 = {b1,b2} by PZFMISC1:def 2;
A11: now
assume C.i1 is trivial;
then C.i1 is empty or ex x being object st C.i1 = {x} by ZFMISC_1:131;
hence contradiction by A3,A10,ZFMISC_1:5;
end;
take C;
thus C is Segre-like
proof
take i1;
let j be Element of I;
assume i1<>j;
then B.j = B1.j by FUNCT_7:32;
then C.j = {B.j,B.j} by PZFMISC1:def 2
.= {B.j} by ENUMSET1:29;
hence thesis;
end;
dom C = I by PARTFUN1:def 2;
then C.i1 in rng C by FUNCT_1:def 3;
hence C is non trivial-yielding by A11;
thus thesis;
end;
end;
registration
let I be non empty set;
cluster Segre-like non trivial-yielding for ManySortedSet of I;
existence
proof
set B = the ManySortedSet of I;
set i = the Element of I;
take C={B}+*(i,{0,1});
thus C is Segre-like
proof
take i;
let j be Element of I;
assume j<>i;
then
A1: C.j = {B}.j by FUNCT_7:32;
j in I;
then
A2: j in dom {B} by PARTFUN1:def 2;
then C.j in rng {B} by A1,FUNCT_1:def 3;
then C.j is non empty trivial by A2,A1,Def16,FUNCT_1:def 9;
hence C.j is 1-element;
end;
thus C is non trivial-yielding
proof
take S = C.i;
dom C = I by PARTFUN1:def 2;
hence S in rng C by FUNCT_1:def 3;
dom {B} = I by PARTFUN1:def 2;
then
A3: C.i = {0,1} by FUNCT_7:31;
0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
then 2 c= card {0,1} by Th2;
hence thesis by A3,Th4;
end;
end;
end;
definition
let I be non empty set;
let B be Segre-like non trivial-yielding ManySortedSet of I;
func indx(B) -> Element of I means
:Def21:
B.it is non trivial;
existence
proof
consider i being Element of I such that
A1: for j being Element of I st i<>j holds B.j is 1-element by Def20;
take i;
now
assume
A2: B.i is trivial;
for S being set st S in rng B holds S is trivial
proof
let S be set;
assume S in rng B;
then consider j being object such that
A3: j in dom B and
A4: S = B.j by FUNCT_1:def 3;
reconsider j as Element of I by A3,PARTFUN1:def 2;
per cases;
suppose
i=j;
hence thesis by A2,A4;
end;
suppose
i<>j;
then B.j is 1-element by A1;
hence thesis by A4;
end;
end;
hence contradiction by Def16;
end;
hence thesis;
end;
uniqueness
proof
let i1,i2 be Element of I;
assume that
A5: B.i1 is non trivial and
A6: B.i2 is non trivial;
consider i being Element of I such that
A7: for j being Element of I st i<>j holds B.j is 1-element by Def20;
A8: B.i2 is not 1-element by A6;
B.i1 is not 1-element by A5;
hence i1=i by A7
.= i2 by A7,A8;
end;
end;
theorem Th12:
for I being non empty set for A being Segre-like non
trivial-yielding ManySortedSet of I for i being Element of I st i <> indx(A)
holds A.i is 1-element
proof
let I be non empty set;
let A be Segre-like non trivial-yielding ManySortedSet of I;
let i be Element of I;
consider j being Element of I such that
A1: for k being Element of I st k<>j holds A.k is 1-element by Def20;
A2: now
assume indx(A) <> j;
then A.indx(A) is 1-element by A1;
hence contradiction by Def21;
end;
assume i <> indx(A);
hence thesis by A1,A2;
end;
registration
let I be non empty set;
cluster Segre-like non trivial-yielding -> non-empty for ManySortedSet of I;
coherence
proof
let f be ManySortedSet of I;
assume f is Segre-like non trivial-yielding;
then reconsider g=f as Segre-like non trivial-yielding ManySortedSet of I;
now
assume {} in rng g;
then consider i being object such that
A1: i in dom f and
A2: g.i = {} by FUNCT_1:def 3;
reconsider i as Element of I by A1,PARTFUN1:def 2;
per cases;
suppose
i=indx(g);
hence contradiction by A2,Def21;
end;
suppose
i <> indx(g);
then g.i is 1-element by Th12;
hence contradiction by A2;
end;
end;
hence thesis by RELAT_1:def 9;
end;
end;
theorem Th13:
for I being non empty set for A being ManySortedSet of I holds 2
c= card (product A) iff A is non-empty non trivial-yielding
proof
let I be non empty set;
let A be ManySortedSet of I;
A1: dom A = I by PARTFUN1:def 2;
thus 2 c= card (product A) implies A is non-empty non trivial-yielding
proof
assume 2 c= card product A;
then consider a,b being object such that
A2: a in product A and
A3: b in product A and
A4: a<>b by Th2;
consider a1 being Function such that
A5: a=a1 & dom a1 = dom A and
A6: for e being object st e in dom A holds a1.e in A.e by A2,CARD_3:def 5;
thus A is non-empty
by A1,A6;
consider b1 being Function such that
A7: b=b1 & dom b1 = dom A and
A8: for e being object st e in dom A holds b1.e in A.e by A3,CARD_3:def 5;
consider e being object such that
A9: e in dom A and
A10: b1.e <> a1.e by A4,A5,A7,FUNCT_1:2;
thus A is non trivial-yielding
proof
take A.e;
thus A.e in rng A by A9,FUNCT_1:def 3;
a1.e in A.e & b1.e in A.e by A6,A8,A9;
then 2 c= card (A.e) by A10,Th2;
hence thesis by Th4;
end;
end;
assume
A11: A is non-empty non trivial-yielding;
then consider r being set such that
A12: r in rng A and
A13: r is non trivial;
now
assume {} in rng A;
then ex o being object st o in dom A & A.o = {} by FUNCT_1:def 3;
hence contradiction by A1,A11;
end;
then product A is non empty by CARD_3:26;
then consider a1 being object such that
A14: a1 in product A;
consider p being object such that
A15: p in dom A and
A16: r = A.p by A12,FUNCT_1:def 3;
consider a being Function such that
A17: a=a1 and
A18: dom a = dom A and
A19: for o being object st o in dom A holds a.o in A.o by A14,CARD_3:def 5;
reconsider a as ManySortedSet of I by A1,A18,PARTFUN1:def 2,RELAT_1:def 18;
2 c= card r by A13,Th4;
then consider t being object such that
A20: t in r and
A21: t <> a.p by Th3;
reconsider p as Element of I by A15,PARTFUN1:def 2;
set b=a+*(p,t);
A22: now
let o be object;
assume
A23: o in dom A;
per cases;
suppose
o<>p;
then b.o = a.o by FUNCT_7:32;
hence b.o in A.o by A19,A23;
end;
suppose
o=p;
hence b.o in A.o by A18,A15,A16,A20,FUNCT_7:31;
end;
end;
dom b = I by PARTFUN1:def 2
.= dom A by PARTFUN1:def 2;
then
A24: b in product A by A22,CARD_3:9;
b.p = t by A18,A15,FUNCT_7:31;
hence thesis by A14,A17,A21,A24,Th2;
end;
registration
let I be non empty set;
let B be Segre-like non trivial-yielding ManySortedSet of I;
cluster product B -> non trivial;
coherence
proof
consider f being object such that
A1: f in product B by XBOOLE_0:def 1;
A2: ex g being Function st g=f & dom g = dom B & for x being object st x in
dom B holds g.x in B.x by A1,CARD_3:def 5;
dom B = I by PARTFUN1:def 2;
then reconsider f as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18
;
B.indx(B) is non trivial by Def21;
then 2 c= card (B.indx(B)) by Th4;
then consider y being object such that
A3: y in B.indx(B) and
A4: y <> f.indx(B) by Th3;
set l=f+*(indx(B),y);
A5: for x being object st x in dom B holds l.x in B.x
proof
let x be object;
assume
A6: x in dom B;
then x in I by PARTFUN1:def 2;
then
A7: x in dom f by PARTFUN1:def 2;
per cases;
suppose
x=indx(B);
hence thesis by A3,A7,FUNCT_7:31;
end;
suppose
x<>indx(B);
then l.x = f.x by FUNCT_7:32;
hence thesis by A2,A6;
end;
end;
dom f=I by PARTFUN1:def 2;
then
A8: l.indx(B) = y by FUNCT_7:31;
dom l = I by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2;
then l in product B by A5,CARD_3:def 5;
then 2 c= card product B by A1,A4,A8,Th2;
hence thesis by Th4;
end;
end;
begin
definition
let I be non empty set;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
func Segre_Blocks(A) -> Subset-Family of product Carrier A means
:Def22:
for
x being set holds x in it iff ex B being Segre-like ManySortedSubset of Carrier
A st x = product B & ex i being Element of I st B.i is Block of A.i;
existence
proof
defpred P[object] means
ex B being Segre-like ManySortedSubset of Carrier A
st $1 = product B & ex i being Element of I st B.i is Block of A.i;
consider S being set such that
A1: for x being object holds x in S iff x in bool (product Carrier A) & P
[x] from XBOOLE_0:sch 1;
S c= bool (product Carrier A)
by A1;
then reconsider S as Subset-Family of product Carrier A;
take S;
let x be set;
thus x in S implies ex B being Segre-like ManySortedSubset of Carrier A st
x = product B & ex i being Element of I st B.i is Block of A.i by A1;
given B being Segre-like ManySortedSubset of Carrier A such that
A2: x = product B and
A3: ex i being Element of I st B.i is Block of A.i;
x c= product Carrier A
proof
let a be object;
assume a in x;
then consider g being Function such that
A4: g=a and
A5: dom g = dom B and
A6: for y being object st y in dom B holds g.y in B.y by A2,CARD_3:def 5;
A7: for y being object st y in dom Carrier A holds g.y in (Carrier A).y
proof
let y be object;
assume y in dom Carrier A;
then
A8: y in I by PARTFUN1:def 2;
then y in dom g by A5,PARTFUN1:def 2;
then
A9: g.y in B.y by A5,A6;
B c= (Carrier A) by PBOOLE:def 18;
then B.y c= (Carrier A).y by A8;
hence thesis by A9;
end;
dom g = I by A5,PARTFUN1:def 2
.= dom Carrier A by PARTFUN1:def 2;
hence thesis by A4,A7,CARD_3:def 5;
end;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let S1,S2 be Subset-Family of product Carrier A such that
A10: for x being set holds x in S1 iff ex B being Segre-like
ManySortedSubset of Carrier A st x = product B & ex i being Element of I st B.i
is Block of A.i and
A11: for x being set holds x in S2 iff ex B being Segre-like
ManySortedSubset of Carrier A st x = product B & ex i being Element of I st B.i
is Block of A.i;
for x being object holds x in S1 iff x in S2
proof
let x be object;
x in S1 iff ex B being Segre-like ManySortedSubset of Carrier A st
x = product B & ex i being Element of I st B.i is Block of A.i by A10;
hence thesis by A11;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let I be non empty set;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
func Segre_Product A -> non empty TopStruct equals
TopStruct(#product Carrier A, Segre_Blocks A#);
correctness;
end;
theorem Th14:
for I being non empty set for A be non-Empty TopStruct-yielding
ManySortedSet of I for x being Point of Segre_Product A holds x is
ManySortedSet of I
proof
let I be non empty set;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
let x be Point of Segre_Product A;
ex f being Function st x=f & dom f = dom Carrier A &
for a being object st a in dom Carrier A holds f.a in (Carrier A).a
by CARD_3:def 5;
hence thesis;
end;
theorem Th15:
for I being non empty set for A being non-Empty
TopStruct-yielding ManySortedSet of I st ex i being Element of I st A.i is non
void holds Segre_Product A is non void
proof
let I be non empty set;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
set B = the trivial-yielding non-empty ManySortedSubset of Carrier A;
given i being Element of I such that
A1: A.i is non void;
set l = the Block of A.i;
A2: the topology of A.i is non empty by A1;
A3: B+*(i,l) c= Carrier A
proof
let i1 be object;
assume
A4: i1 in I;
then
A5: i1 in dom B by PARTFUN1:def 2;
per cases;
suppose
A6: i = i1;
then B+*(i,l).i1 = l by A5,FUNCT_7:31;
then
A7: B+*(i,l).i1 in the topology of (A.i) by A2;
ex R being 1-sorted st R=A.i1 & the carrier of R = ( Carrier A).i1
by A4,PRALG_1:def 15;
hence thesis by A6,A7;
end;
suppose
A8: i1 <> i;
A9: B c= Carrier A by PBOOLE:def 18;
B+*(i,l).i1 = B.i1 by A8,FUNCT_7:32;
hence thesis by A4,A9;
end;
end;
for j being Element of I st i<>j holds B+*(i,l).j is 1-element
proof
let j be Element of I;
assume i<>j;
then
A10: B+*(i,l).j = B.j by FUNCT_7:32;
j in I;
then
A11: j in dom B by PARTFUN1:def 2;
then B+*(i,l).j in rng B by A10,FUNCT_1:def 3;
then B+*(i,l).j is non empty trivial by A11,A10,Def16,FUNCT_1:def 9;
hence thesis;
end;
then reconsider C=B+*(i,l) as Segre-like ManySortedSubset of Carrier A by A3
,Def20,PBOOLE:def 18;
dom B = I by PARTFUN1:def 2;
then C.i is Block of A.i by FUNCT_7:31;
then product C in Segre_Blocks A by Def22;
hence thesis;
end;
theorem Th16:
for I being non empty set for A being non-Empty
TopStruct-yielding ManySortedSet of I st for i being Element of I holds A.i is
non degenerated & ex i being Element of I st A.i is non void holds
Segre_Product A is non degenerated
proof
let I be non empty set;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds A.i is non degenerated & ex i being
Element of I st A.i is non void;
then Segre_Product A is non void by Th15;
then reconsider SB=Segre_Blocks A as non empty set;
now
assume product Carrier A in SB;
then consider B being Segre-like ManySortedSubset of Carrier A such that
A2: product Carrier A = product B and
A3: ex i being Element of I st B.i is Block of A.i by Def22;
consider i being Element of I such that
A4: B.i is Block of A.i by A3;
B is non-empty by A2,Th1;
then
(ex R being 1-sorted st R=A.i & the carrier of R = ( Carrier A).i )& (
Carrier A).i is Block of A.i by A2,A4,PRALG_1:def 15,PUA2MSS1:2;
then A.i is degenerated;
hence contradiction by A1;
end;
then not product Carrier A is Element of SB;
hence thesis;
end;
theorem Th17:
for I being non empty set for A being non-Empty
TopStruct-yielding ManySortedSet of I st for i being Element of I holds A.i is
with_non_trivial_blocks & ex i being Element of I st A.i is non void holds
Segre_Product A is with_non_trivial_blocks
proof
let I be non empty set;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds A.i is with_non_trivial_blocks & ex i
being Element of I st A.i is non void;
for k being Block of Segre_Product A holds 2 c= card k
proof
let k be Block of Segre_Product A;
Segre_Product A is non void by A1,Th15;
then consider B being Segre-like ManySortedSubset of Carrier A such that
A2: k = product B and
A3: ex i being Element of I st B.i is Block of A.i by Def22;
consider i being Element of I such that
A4: B.i is Block of A.i by A3;
A.i is with_non_trivial_blocks by A1;
then 2 c= card (B.i) by A4;
then
A5: B.i is non trivial by Th4;
dom B = I by PARTFUN1:def 2;
then B.i in rng B by FUNCT_1:def 3;
then reconsider
BB=B as Segre-like non trivial-yielding ManySortedSet of I by A5,Def16;
product BB is non trivial;
hence thesis by A2,Th4;
end;
hence thesis;
end;
theorem Th18:
for I being non empty set for A being non-Empty
TopStruct-yielding ManySortedSet of I st for i being Element of I holds A.i is
identifying_close_blocks with_non_trivial_blocks & ex i being Element of I st A
.i is non void holds Segre_Product A is identifying_close_blocks
proof
let I be non empty set;
let A be non-Empty TopStruct-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds A.i is identifying_close_blocks
with_non_trivial_blocks & ex i being Element of I st A.i is non void;
for k,l being Block of Segre_Product A st 2 c= card(k /\ l) holds k=l
proof
let k,l be Block of Segre_Product A;
assume 2 c= card(k /\ l);
then consider a,b being object such that
A2: a in k /\ l and
A3: b in k /\ l and
A4: a <> b by Th2;
Segre_Product A is non void by A1,Th15;
then consider B being Segre-like ManySortedSubset of Carrier A such that
A5: k = product B and
A6: ex i being Element of I st B.i is Block of A.i by Def22;
A7: b in product B by A5,A3,XBOOLE_0:def 4;
then reconsider b as Function by CARD_3:48;
A8: dom b = dom B by A7,CARD_3:9
.= I by PARTFUN1:def 2;
then reconsider b as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
A9: a in product B by A5,A2,XBOOLE_0:def 4;
consider i being Element of I such that
A10: B.i is Block of A.i by A6;
A11: for j being Element of I st j<>i holds B.j is 1-element
proof
let j be Element of I;
assume
A12: j<>i;
consider i1 being Element of I such that
A13: for j1 being Element of I st j1<>i1 holds B.j1 is 1-element by Def20;
A.i is with_non_trivial_blocks by A1;
then 2 c= card (B.i) by A10;
then B.i is not 1-element by Th4;
then i1 = i by A13;
hence thesis by A12,A13;
end;
Segre_Product A is non void by A1,Th15;
then consider C being Segre-like ManySortedSubset of Carrier A such that
A14: l = product C and
A15: ex i being Element of I st C.i is Block of A.i by Def22;
A16: dom C = I by PARTFUN1:def 2;
consider j being Element of I such that
A17: C.j is Block of A.j by A15;
reconsider a as Function by A9,CARD_3:48;
A18: dom a = dom B by A9,CARD_3:9
.= I by PARTFUN1:def 2;
then reconsider a as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
consider x being object such that
A19: x in I and
A20: a.x <> b.x by A4,A18,A8,FUNCT_1:2;
reconsider x as Element of I by A19;
dom B = I by PARTFUN1:def 2;
then
A21: b.x in B.x by A7,CARD_3:9;
dom B = I by PARTFUN1:def 2;
then
A22: a.x in B.x by A9,CARD_3:9;
then 2 c= card (B.x) by A20,A21,Th2;
then B.x is not 1-element by Th4;
then
A23: x=i by A11;
b in product C by A14,A3,XBOOLE_0:def 4;
then
A24: b.x in C.x by A16,CARD_3:9;
A25: a in product C by A14,A2,XBOOLE_0:def 4;
A26: for i being Element of I st j<>i holds C.i is 1-element
proof
let i be Element of I;
assume
A27: j<>i;
consider j1 being Element of I such that
A28: for i1 being Element of I st j1<>i1 holds C.i1 is 1-element by Def20;
A.j is with_non_trivial_blocks by A1;
then 2 c= card (C.j) by A17;
then C.j is not 1-element by Th4;
then j1 = j by A28;
hence thesis by A27,A28;
end;
A29: dom B = I by PARTFUN1:def 2
.= dom C by PARTFUN1:def 2;
dom C = I by PARTFUN1:def 2;
then
A30: a.x in C.x by A25,CARD_3:9;
then 2 c= card (C.x) by A20,A24,Th2;
then C.x is not 1-element by Th4;
then
A31: x=j by A26;
for s being object st s in dom B holds B.s c= C.s
proof
let s be object;
assume
A32: s in dom B;
then reconsider t=s as Element of I by PARTFUN1:def 2;
per cases;
suppose
A33: t=x;
then reconsider Ct = C.t as Block of A.t by A17,A31;
reconsider Bt = B.t as Block of A.t by A10,A23,A33;
a.t in (Bt /\ Ct) & b.t in (Bt /\ Ct) by A22,A21,A30,A24,A33,
XBOOLE_0:def 4;
then
A34: 2 c= card (Bt /\ Ct) by A20,A33,Th2;
A.t is identifying_close_blocks by A1;
hence thesis by A34;
end;
suppose
s<>x;
then B.t is 1-element by A11,A23;
then consider y being object such that
A35: B.t = {y} by ZFMISC_1:131;
A36: a.t in C.t by A25,A29,A32,CARD_3:9;
a.t in B.t by A9,A32,CARD_3:9;
then a.t = y by A35,TARSKI:def 1;
hence thesis by A35,A36,ZFMISC_1:31;
end;
end;
hence k c= l by A5,A14,A29,CARD_3:27;
for s being object st s in dom C holds C.s c= B.s
proof
let s be object;
assume
A37: s in dom C;
then reconsider t=s as Element of I by PARTFUN1:def 2;
per cases;
suppose
A38: t=x;
then reconsider Ct = C.t as Block of A.t by A17,A31;
reconsider Bt = B.t as Block of A.t by A10,A23,A38;
a.t in (Bt /\ Ct) & b.t in (Bt /\ Ct) by A22,A21,A30,A24,A38,
XBOOLE_0:def 4;
then
A39: 2 c= card (Bt /\ Ct) by A20,A38,Th2;
A.t is identifying_close_blocks by A1;
hence thesis by A39;
end;
suppose
s<>x;
then C.t is 1-element by A26,A31;
then consider y being object such that
A40: C.t = {y} by ZFMISC_1:131;
A41: a.t in B.t by A9,A29,A37,CARD_3:9;
a.t in C.t by A25,A37,CARD_3:9;
then a.t = y by A40,TARSKI:def 1;
hence thesis by A40,A41,ZFMISC_1:31;
end;
end;
hence thesis by A5,A14,A29,CARD_3:27;
end;
hence thesis;
end;
registration
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
cluster Segre_Product A -> non void non degenerated
with_non_trivial_blocks identifying_close_blocks;
coherence
proof
A1: (for j being Element of I holds A.j is with_non_trivial_blocks)& for
j being Element of I holds A.j is identifying_close_blocks;
A.the Element of I is non void & for j being Element of I holds A.j is non
degenerated;
hence thesis by A1,Th15,Th16,Th17,Th18;
end;
end;
theorem
for T being TopStruct for S being Subset of T holds S is trivial
implies S is strong closed_under_lines
proof
let T be TopStruct;
let S be Subset of T;
assume
A1: S is trivial;
thus S is strong
proof
let x,y be Point of T;
assume
A2: x in S & y in S;
thus x,y are_collinear
proof
per cases;
suppose
x=y;
hence thesis;
end;
suppose
x<>y;
then 2 c= card S by A2,Th2;
hence thesis by A1,Th4;
end;
end;
end;
thus S is closed_under_lines
proof
let l be Block of T;
A3: card (l /\ S) c= card S by CARD_1:11,XBOOLE_1:17;
assume 2 c= card (l /\ S);
then 2 c= card S by A3;
hence thesis by A1,Th4;
end;
end;
theorem Th20:
for S being identifying_close_blocks TopStruct, l being Block of
S for L being Subset of S st L=l holds L is closed_under_lines
by Def7;
theorem Th21:
for S being TopStruct, l being Block of S for L being Subset of
S st L=l holds L is strong
proof
let S be TopStruct;
let l be Block of S;
let L be Subset of S;
assume
A1: L=l;
thus L is strong
proof
let x,y be Point of S;
assume x in L & y in L;
then {x,y} c= l by A1,ZFMISC_1:32;
hence thesis;
end;
end;
theorem
for S being non void TopStruct holds [#]S is closed_under_lines
proof
let S be non void TopStruct;
thus [#]S is closed_under_lines
proof
let K be Block of S;
assume 2 c= card (K /\ [#]S);
K in the topology of S;
hence thesis;
end;
end;
theorem Th23:
for I being non empty set for A being Segre-like non
trivial-yielding ManySortedSet of I for x,y being ManySortedSet of I st x in
product A & y in product A
for i being object st i <> indx(A) holds x.i = y.i
proof
let I be non empty set;
let A be Segre-like non trivial-yielding ManySortedSet of I;
let x,y be ManySortedSet of I such that
A1: x in product A and
A2: y in product A;
let i be object;
A3: dom A = I by PARTFUN1:def 2;
assume
A4: i <> indx(A);
per cases;
suppose
A5: not i in I;
then
A6: not i in dom y by PARTFUN1:def 2;
not i in dom x by A5,PARTFUN1:def 2;
hence x.i = {} by FUNCT_1:def 2
.= y.i by A6,FUNCT_1:def 2;
end;
suppose
i in I;
then reconsider ii=i as Element of I;
consider j being Element of I such that
A7: for k being Element of I st k<>j holds A.k is 1-element by Def20;
now
assume j <> indx(A);
then A.indx(A) is 1-element by A7;
hence contradiction by Def21;
end;
then A.ii is 1-element by A4,A7;
then consider o being object such that
A8: A.i = {o} by ZFMISC_1:131;
A9: x.ii in A.ii by A1,A3,CARD_3:9;
y.ii in A.ii by A2,A3,CARD_3:9;
hence y.i = o by A8,TARSKI:def 1
.= x.i by A8,A9,TARSKI:def 1;
end;
end;
theorem Th24:
for I being non empty set for A being PLS-yielding ManySortedSet
of I for x being set holds x is Block of Segre_Product A iff ex L being
Segre-like non trivial-yielding ManySortedSubset of Carrier A st x = product L
& L.indx(L) is Block of A.indx(L)
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let x be set;
thus x is Block of Segre_Product A implies ex L being Segre-like non
trivial-yielding ManySortedSubset of Carrier A st x = product L & L.indx(L) is
Block of A.indx(L)
proof
assume
A1: x is Block of Segre_Product A;
then consider L being Segre-like ManySortedSubset of Carrier A such that
A2: x = product L and
A3: ex i being Element of I st L.i is Block of A.i by Def22;
2 c= card (product L) by A1,A2,Def6;
then reconsider L as Segre-like non trivial-yielding ManySortedSubset of
Carrier A by Th13;
consider i being Element of I such that
A4: L.i is Block of A.i by A3;
now
assume i <> indx(L);
then
A5: L.i is 1-element by Th12;
2 c= card (L.i) by A4,Def6;
hence contradiction by A5,Th4;
end;
hence thesis by A2,A4;
end;
given L being Segre-like non trivial-yielding ManySortedSubset of Carrier A
such that
A6: x = product L & L.indx(L) is Block of A.indx(L);
thus thesis by A6,Def22;
end;
theorem Th25:
for I being non empty set for A being PLS-yielding ManySortedSet
of I for P being ManySortedSet of I st P is Point of Segre_Product A for i
being Element of I for p being Point of A.i holds P+*(i,p) is Point of
Segre_Product A
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let P be ManySortedSet of I such that
A1: P is Point of Segre_Product A;
let j be Element of I;
let p be Point of A.j;
A2: for i be object st i in dom Carrier A holds P+*(j,p).i in (Carrier A).i
proof
let i be object;
assume
A3: i in dom Carrier A;
then i in I by PARTFUN1:def 2;
then
A4: i in dom P by PARTFUN1:def 2;
per cases;
suppose
i <> j;
then P+*(j,p).i = P.i by FUNCT_7:32;
hence thesis by A1,A3,CARD_3:9;
end;
suppose
A5: i = j;
A6: p in the carrier of A.j;
P+*(j,p).i = p by A4,A5,FUNCT_7:31;
hence thesis by A5,A6,YELLOW_6:2;
end;
end;
dom (P+*(j,p)) = I by PARTFUN1:def 2
.= dom Carrier A by PARTFUN1:def 2;
hence thesis by A2,CARD_3:9;
end;
theorem Th26:
for I being non empty set for A,B being Segre-like non
trivial-yielding ManySortedSet of I st 2 c= card ((product A) /\ (product B))
holds indx(A) = indx(B) &
for i being object st i <> indx(A) holds A.i = B.i
proof
let I be non empty set;
let A,B be Segre-like non trivial-yielding ManySortedSet of I;
A1: dom B = I by PARTFUN1:def 2;
assume 2 c= card ((product A) /\ (product B));
then consider a,b being object such that
A2: a in (product A) /\ (product B) and
A3: b in (product A) /\ (product B) and
A4: a<>b by Th2;
b in (product A) by A3,XBOOLE_0:def 4;
then consider b1 being Function such that
A5: b1=b and
A6: dom b1=dom A and
A7: for o being object st o in dom A holds b1.o in A.o by CARD_3:def 5;
a in (product A) by A2,XBOOLE_0:def 4;
then consider a1 being Function such that
A8: a1=a and
A9: dom a1=dom A and
A10: for o being object st o in dom A holds a1.o in A.o by CARD_3:def 5;
consider o being object such that
A11: o in dom A and
A12: a1.o <> b1.o by A4,A8,A9,A5,A6,FUNCT_1:2;
reconsider o as Element of I by A11,PARTFUN1:def 2;
b in (product B) by A3,XBOOLE_0:def 4;
then
A13: b1.o in B.o by A5,A1,CARD_3:9;
A14: a in (product B) by A2,XBOOLE_0:def 4;
then a1.o in B.o by A8,A1,CARD_3:9;
then 2 c= card (B.o) by A12,A13,Th2;
then
A15: B.o is non trivial by Th4;
then
A16: o = indx(B) by Def21;
A17: b1.o in A.o by A7,A11;
a1.o in A.o by A10,A11;
then 2 c= card (A.o) by A12,A17,Th2;
then A.o is non trivial by Th4;
then
A18: o = indx(A) by Def21;
hence indx(A) = indx(B) by A15,Def21;
let i be object;
assume
A19: i <> indx(A);
per cases;
suppose
A20: i in I;
then B.i is 1-element by A18,A16,A19,Th12;
then
A21: ex y being object st B.i = {y} by ZFMISC_1:131;
A.i is 1-element by A19,A20,Th12;
then consider x being object such that
A22: A.i = {x} by ZFMISC_1:131;
dom B = I by PARTFUN1:def 2;
then
A23: a1.i in B.i by A8,A14,A20,CARD_3:9;
dom A = I by PARTFUN1:def 2;
then a1.i in A.i by A10,A20;
then a1.i = x by A22,TARSKI:def 1;
hence thesis by A22,A21,A23,TARSKI:def 1;
end;
suppose
A24: not i in I;
then
A25: not i in dom B by PARTFUN1:def 2;
not i in dom A by A24,PARTFUN1:def 2;
hence A.i = {} by FUNCT_1:def 2
.= B.i by A25,FUNCT_1:def 2;
end;
end;
theorem Th27:
for I being non empty set for A being Segre-like non
trivial-yielding ManySortedSet of I for N being non trivial set holds A+*(indx(
A),N) is Segre-like non trivial-yielding
proof
let I be non empty set;
let A be Segre-like non trivial-yielding ManySortedSet of I;
let N be non trivial set;
thus A+*(indx(A),N) is Segre-like
proof
take indx(A);
let i be Element of I;
assume
A1: i <> indx(A);
then A+*(indx(A),N).i = A.i by FUNCT_7:32;
hence thesis by A1,Th12;
end;
thus A+*(indx(A),N) is non trivial-yielding
proof
take A+*(indx(A),N).indx(A);
dom (A+*(indx(A),N)) = I by PARTFUN1:def 2;
hence A+*(indx(A),N).indx(A) in rng (A+*(indx(A),N)) by FUNCT_1:def 3;
I = dom A by PARTFUN1:def 2;
hence thesis by FUNCT_7:31;
end;
end;
theorem
for S being non empty non void identifying_close_blocks
without_isolated_points TopStruct holds S is strongly_connected implies S is
connected
proof
let S be non empty non void identifying_close_blocks without_isolated_points
TopStruct;
assume
A1: S is strongly_connected;
thus S is connected
proof
let x,y be Point of S;
A2: len <*x*> = 1 by FINSEQ_1:39;
A3: len <*y*> = 1 by FINSEQ_1:39;
consider K being Block of S such that
A4: x in K by Def9;
K in the topology of S;
then reconsider L=K as Subset of S;
L is closed_under_lines strong by Th20,Th21;
then consider f being FinSequence of bool the carrier of S such that
A5: L = f.1 and
A6: y in f.(len f) and
A7: for W being Subset of S st W in rng f holds W is
closed_under_lines strong and
A8: for i being Nat st 1 <= i & i < len f holds 2 c= card((f.i) /\ (f.
(i+1))) by A1;
A9: len f in dom f by A6,FUNCT_1:def 2;
A10: 1 in dom f by A4,A5,FUNCT_1:def 2;
then reconsider n=(len f) - 1 as Nat by FINSEQ_3:26;
deffunc F(Nat) = (f.$1) /\ f.($1+1);
reconsider n as Element of NAT by ORDINAL1:def 12;
consider h being FinSequence such that
A11: len h = n & for k being Nat st k in dom h holds h.k=F(k) from
FINSEQ_1:sch 2;
A12: dom h = Seg n by A11,FINSEQ_1:def 3;
A13: (len h) + 1 = len f by A11;
now
assume {} in rng h;
then consider i being object such that
A14: i in dom h and
A15: h.i = {} by FUNCT_1:def 3;
reconsider i as Element of NAT by A14;
A16: i <= len h by A14,FINSEQ_3:25;
then
A17: i < len f by A13,NAT_1:13;
A18: 1 <= i by A14,FINSEQ_3:25;
then i in Seg n by A11,A16,FINSEQ_1:1;
then h.i=(f.i) /\ (f.(i+1)) by A11,A12;
then 2 c= card (h.i) by A8,A18,A17;
hence contradiction by A15;
end;
then product h <> {} by CARD_3:26;
then consider c being object such that
A19: c in product h by XBOOLE_0:def 1;
A20: ex ce being Function st ce = c & dom ce = dom h &
for a being object st a
in dom h holds ce.a in h.a by A19,CARD_3:def 5;
then reconsider c as Function;
A21: dom h = Seg n by A11,FINSEQ_1:def 3;
then reconsider c as FinSequence by A20,FINSEQ_1:def 2;
A22: rng f c= bool the carrier of S by FINSEQ_1:def 4;
rng (<*x*>^c^<*y*>) c= the carrier of S
proof
let r be object;
assume r in rng (<*x*>^c^<*y*>);
then r in rng (<*x*>^c) \/ rng <*y*> by FINSEQ_1:31;
then r in rng (<*x*>^c) or r in rng <*y*> by XBOOLE_0:def 3;
then
A23: r in (rng <*x*>) \/ (rng c) or r in rng <*y*> by FINSEQ_1:31;
per cases by A23,XBOOLE_0:def 3;
suppose
r in rng <*x*>;
then r in {x} by FINSEQ_1:38;
hence thesis;
end;
suppose
r in rng c;
then consider o being object such that
A24: o in dom c and
A25: r = c.o by FUNCT_1:def 3;
reconsider o as Element of NAT by A24;
h.o=(f.o) /\ f.(o+1) by A11,A20,A24;
then r in (f.o) /\ f.(o+1) by A20,A24,A25;
then
A26: r in f.o by XBOOLE_0:def 4;
len h <= len f by A13,NAT_1:11;
then dom h c= dom f by FINSEQ_3:30;
then f.o in rng f by A20,A24,FUNCT_1:def 3;
hence thesis by A22,A26;
end;
suppose
r in rng <*y*>;
then r in {y} by FINSEQ_1:38;
hence thesis;
end;
end;
then reconsider g = <*x*>^c^<*y*> as FinSequence of the carrier of S by
FINSEQ_1:def 4;
A27: len (<*x*>^c) = len <*x*> + len c by FINSEQ_1:22;
then
A28: len (<*x*>^c) = len c + 1 by FINSEQ_1:39;
take g;
A29: g = <*x*>^(c^<*y*>) by FINSEQ_1:32;
hence x=g.1 by FINSEQ_1:41;
len g = len (<*x*>^c) + len <*y*> by FINSEQ_1:22;
then
A30: len (<*x*>^c) + 1 = len g by FINSEQ_1:39;
hence
A31: y=g.(len g) by FINSEQ_1:42;
let i be Nat;
assume that
A32: 1 <= i and
A33: i < len g;
A34: i <= len (<*x*>^c) by A30,A33,NAT_1:13;
let a,b be Point of S;
assume that
A35: a = g.i and
A36: b = g.(i+1);
reconsider i as Element of NAT by ORDINAL1:def 12;
per cases by A28,A32,A34,NAT_1:8,XXREAL_0:1;
suppose
A37: i = 1 & i <= len c;
len (c^<*y*>) = len c + 1 & len (<*x*>^(c^<*y*>)) = len <*x*> + len
(c^<*y*> ) by A3,FINSEQ_1:22;
then
A38: len (<*x*>^(c^<*y*>)) = 1 + 1 + len c by A2;
A39: 1 in dom c by A37,FINSEQ_3:25;
b = (<*x*>^(c^<*y*>)).2 by A36,A37,FINSEQ_1:32;
then b = (c^<*y*>).(2 - len <*x*>) by A2,A38,FINSEQ_1:24,NAT_1:11;
then b = (c^<*y*>).(2-1) by FINSEQ_1:39;
then
A40: b = c.1 by A39,FINSEQ_1:def 7;
c.1 in h.1 & h.1=(f.1) /\ f.(1+1) by A11,A20,A39;
then
A41: b in f.1 by A40,XBOOLE_0:def 4;
A42: f.1 in rng f by A10,FUNCT_1:def 3;
then reconsider f1=f.1 as Subset of S by A22;
A43: f1 is closed_under_lines strong by A7,A42;
a = x by A29,A35,A37,FINSEQ_1:41;
hence thesis by A4,A5,A41,A43;
end;
suppose
A44: i = 1 & i = len c + 1;
A45: f.1 in rng f by A10,FUNCT_1:def 3;
then reconsider f1=f.1 as Subset of S by A22;
A46: f1 is closed_under_lines strong by A7,A45;
len <*x*> = 1 by FINSEQ_1:39;
then
A47: len g = i+1 by A30,A44,FINSEQ_1:22;
len h = 0 by A20,A44,FINSEQ_3:29;
then x,y are_collinear by A4,A5,A6,A11,A46;
hence thesis by A29,A31,A35,A36,A44,A47,FINSEQ_1:41;
end;
suppose
A48: 1 < i & i <= len c;
A49: len h <= len h + 1 & len c = len h by A20,FINSEQ_3:29,NAT_1:11;
then i <= len h + 1 by A48,XXREAL_0:2;
then
A50: i in dom f by A11,A48,FINSEQ_3:25;
then reconsider j = i-1 as Nat by FINSEQ_3:26;
i <= len c + 1 by A48,A49,XXREAL_0:2;
then i in dom (<*x*>^c) by A28,A48,FINSEQ_3:25;
then
A51: a = (<*x*>^c).i by A35,FINSEQ_1:def 7;
i <= len(<*x*>^c) by A27,A2,A48,NAT_1:13;
then
A52: a = c.j by A2,A48,A51,FINSEQ_1:24;
j + 1 = i;
then
A53: 1 <= j by A48,NAT_1:13;
A54: f.i in rng f by A50,FUNCT_1:def 3;
then reconsider ff = f.i as Subset of S by A22;
A55: j <= j + 1 by NAT_1:11;
A56: len <*x*> < i+1 & i+1 <= len c + 1 by A2,A48,NAT_1:13,XREAL_1:6;
then i+1 in dom (<*x*>^c) by A27,A2,FINSEQ_3:25;
then b = (<*x*>^c).(i+1) by A36,FINSEQ_1:def 7;
then
A57: b = c.(i + 1 - len <*x*>) by A28,A56,FINSEQ_1:24;
i <= len h by A20,A48,FINSEQ_3:29;
then
A58: i in Seg n by A11,A48,FINSEQ_1:1;
then c.i in h.i by A20,A21;
then b in (f.i) /\ f.(i+1) by A11,A12,A2,A58,A57;
then
A59: b in ff by XBOOLE_0:def 4;
i <= len h by A20,A48,FINSEQ_3:29;
then j <= n by A11,A55,XXREAL_0:2;
then
A60: j in Seg n by A53,FINSEQ_1:1;
then c.j in h.j by A20,A21;
then a in (f.j) /\ f.(j+1) by A11,A12,A60,A52;
then
A61: a in ff by XBOOLE_0:def 4;
ff is closed_under_lines strong by A7,A54;
hence thesis by A61,A59;
end;
suppose
A62: 1 < i & i = len c + 1;
then 0 + 1 < len c + 1;
then ex k being Nat st len c = k + 1 by NAT_1:6;
then 1 <= len c by NAT_1:11;
then
A63: len c in dom h by A20,FINSEQ_3:25;
A64: len (<*x*>^c) = 1 + len c by A2,FINSEQ_1:22;
then i in dom (<*x*>^c) by A62,FINSEQ_3:25;
then a = (<*x*>^c).i by A35,FINSEQ_1:def 7
.= c.(len c + 1 - 1) by A2,A62,A64,FINSEQ_1:24
.= c.(len c);
then a in h.(len c) by A20,A63;
then
A65: a in (f.(len c)) /\ (f.(len c + 1)) by A11,A63;
A66: f.(len f) in rng f by A9,FUNCT_1:def 3;
then reconsider ff = f.(len f) as Subset of S by A22;
A67: ff is closed_under_lines strong by A7,A66;
len c = len h by A20,FINSEQ_3:29;
then
A68: a in ff by A11,A65,XBOOLE_0:def 4;
b = y by A36,A62,A64,FINSEQ_1:42;
hence thesis by A6,A67,A68;
end;
end;
end;
theorem
for I being non empty set for A being PLS-yielding ManySortedSet of I
for S being Subset of Segre_Product A holds S is non trivial strong
closed_under_lines iff ex B being Segre-like non trivial-yielding
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 closed_under_lines
proof
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let S be Subset of Segre_Product A;
thus S is non trivial strong closed_under_lines implies ex B being
Segre-like non trivial-yielding 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
closed_under_lines
proof
assume
A1: S is non trivial strong closed_under_lines;
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,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 as Segre-like non trivial-yielding 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
assume
A11: a1.indx(CC) = b1.indx(CC);
for i being object st i in I holds a1.i = b1.i
proof
let i be object;
assume i in I;
per cases;
suppose
i = indx(CC);
hence thesis by A11;
end;
suppose
A12: i <> indx(CC);
a1 in product CC & b1 in product CC by A5,A6,ZFMISC_1:32;
hence thesis by A12,Th23;
end;
end;
hence contradiction by A4,A8,A9,FUNCT_1:2;
end;
A13: for f being ManySortedSet of I st f in S for i being Element of I st
i <> indx(CC) holds f.i in CC.i
proof
let f be ManySortedSet of I;
assume
A14: f in S;
then reconsider f1=f as Point of Segre_Product A;
let i be Element of I;
assume
A15: i <> indx(CC);
now
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;
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 Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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;
end;
hence 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;
assume
A34: i in I;
per cases;
suppose
A35: i <> indx(CC);
A36: CC c= Carrier A by PBOOLE:def 18;
CC+*(indx(CC),p).i = CC.i by A35,FUNCT_7:32;
hence thesis by A34,A36;
end;
suppose
A37: i=indx(CC);
A38: p c= (Carrier A).i
proof
let y be object;
assume y in p;
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 thesis by A39,CARD_3:9;
end;
dom CC = I by PARTFUN1:def 2;
hence thesis by A37,A38,FUNCT_7:31;
end;
end;
then reconsider B=CC+*(indx(CC),p) as Segre-like non trivial-yielding
ManySortedSubset of Carrier A by Th27,PBOOLE:def 18;
take B;
A40: dom B = I by PARTFUN1:def 2;
A41: B.indx(CC) = p by A7,FUNCT_7:31;
thus
A42: S = product B
proof
thus S c= product B
proof
let e be object;
assume
A43: e in S;
then reconsider f=e as ManySortedSet of I by Th14;
A44: now
let i be object;
assume i in I;
then reconsider j=i as Element of I;
per cases;
suppose
j = indx(CC);
hence f.i in B.i by A41,A43,CARD_3:def 6;
end;
suppose
A45: j <> indx(CC);
then f.j in CC.j by A13,A43;
hence f.i in B.i by A45,FUNCT_7:32;
end;
end;
dom f = I by PARTFUN1:def 2;
hence thesis by A40,A44,CARD_3:9;
end;
let e be object;
assume e in product B;
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 as ManySortedSet of I by A48;
A50: now
let i be object;
assume i in I;
then reconsider j=i as Element of I;
per cases;
suppose
i = indx(CC);
hence f.i = g.i by A49;
end;
suppose
A51: i <> indx(CC);
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;
end;
end;
dom g = I by PARTFUN1:def 2;
hence thesis by A46,A48,A50,FUNCT_1:2;
end;
let SS be Subset of A.indx(B);
assume
A54: SS=B.indx(B);
thus SS is strong
proof
let q,r be Point of A.indx(B);
assume that
A55: q in SS and
A56: r in SS;
thus q,r are_collinear
proof
per cases;
suppose
q=r;
hence thesis;
end;
suppose
A57: q <> r;
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
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;
hence contradiction by A57,A59,A60,FUNCT_7:31;
end;
A61: for i being object st i in dom B holds Q1.i in B.i
proof
let i be object;
assume
A62: i in dom B;
then i in I by PARTFUN1:def 2;
then
A63: i in dom a1 by PARTFUN1:def 2;
per cases;
suppose
i <> indx(B);
then Q1.i = a1.i by FUNCT_7:32;
hence thesis by A2,A42,A62,CARD_3:9;
end;
suppose
i = indx(B);
hence thesis by A54,A55,A63,FUNCT_7:31;
end;
end;
A64: for i being object st i in dom B holds R1.i in B.i
proof
let i be object;
assume
A65: i in dom B;
then i in I by PARTFUN1:def 2;
then
A66: i in dom a1 by PARTFUN1:def 2;
per cases;
suppose
i <> indx(B);
then R1.i = a1.i by FUNCT_7:32;
hence thesis by A2,A42,A65,CARD_3:9;
end;
suppose
i = indx(B);
hence thesis by A54,A56,A66,FUNCT_7:31;
end;
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 Segre-like non trivial-yielding 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
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);
hence contradiction by A57,A76,A77,FUNCT_7:31;
end;
then 2 c= card(L1.indx(B)) by A73,A75,Th2;
then
A78: L1.indx(B) is non 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 thesis;
end;
end;
end;
thus SS is closed_under_lines
proof
let L be Block of A.indx(B);
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;
assume
A82: o in I;
thus B+*(indx(B),L1).o c= (Carrier A).o
proof
per cases;
suppose
A83: o <> indx(B);
A84: B c= Carrier A by PBOOLE:def 18;
B+*(indx(B),L1).o = B.o by A83,FUNCT_7:32;
hence thesis by A82,A84;
end;
suppose
A85: o = indx(B);
then B+*(indx(B),L1).o = L by A40,FUNCT_7:31;
hence thesis by A81,A85,YELLOW_6:2;
end;
end;
end;
then reconsider L2 = B+*(indx(B),L1) as Segre-like non trivial-yielding
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);
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 y1 = I by PARTFUN1:def 2;
now
let o be object;
assume
A91: o in I;
per cases;
suppose
o <> indx(B);
then y1.o = a1.o by FUNCT_7:32;
hence y1.o in B.o by A2,A40,A42,A91,CARD_3:9;
end;
suppose
A92: o = indx(B);
then y1.o = y by A8,FUNCT_7:31;
hence y1.o in B.o by A54,A88,A92,XBOOLE_0:def 4;
end;
end;
then
A93: y1 in S by A40,A42,A90,CARD_3:9;
A94: dom L2 = I by PARTFUN1:def 2;
now
let o be object;
assume
A95: o in dom L2;
per cases;
suppose
A96: o <> indx(B);
then
A97: y1.o = a1.o by FUNCT_7:32;
a1.o in B.o by A2,A40,A42,A94,A95,CARD_3:9;
hence y1.o in L2.o by A96,A97,FUNCT_7:32;
end;
suppose
A98: o = indx(B);
then y1.o = y by A8,FUNCT_7:31;
hence y1.o in L2.o by A88,A86,A98,XBOOLE_0:def 4;
end;
end;
then y1 in L3 by A94,A90,CARD_3:9;
then
A99: y1 in L3 /\ S by A93,XBOOLE_0:def 4;
set x1=a1+*(indx(B),x);
A100: dom x1 = I by PARTFUN1:def 2;
now
let o be object;
assume
A101: o in I;
per cases;
suppose
o <> indx(B);
then x1.o = a1.o by FUNCT_7:32;
hence x1.o in B.o by A2,A40,A42,A101,CARD_3:9;
end;
suppose
A102: o = indx(B);
then x1.o = x by A8,FUNCT_7:31;
hence x1.o in B.o by A54,A87,A102,XBOOLE_0:def 4;
end;
end;
then
A103: x1 in S by A40,A42,A100,CARD_3:9;
A104: x1.indx(B) = x & y1.indx(B) = y by A8,FUNCT_7:31;
now
let o be object;
assume
A105: o in dom L2;
per cases;
suppose
A106: o <> indx(B);
then
A107: x1.o = a1.o by FUNCT_7:32;
a1.o in B.o by A2,A40,A42,A94,A105,CARD_3:9;
hence x1.o in L2.o by A106,A107,FUNCT_7:32;
end;
suppose
A108: o = indx(B);
then x1.o = x by A8,FUNCT_7:31;
hence x1.o in L2.o by A87,A86,A108,XBOOLE_0:def 4;
end;
end;
then x1 in L3 by A94,A100,CARD_3:9;
then x1 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
proof
let e be object;
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 as ManySortedSet of I by PARTFUN1:def 2
,RELAT_1:def 18;
assume
A112: e in L;
A113: now
let o be object;
assume
A114: o in dom L2;
per cases;
suppose
o <> indx(B);
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;
end;
suppose
A115: o = indx(B);
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;
end;
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 thesis by A54,A111,FUNCT_7:31;
end;
end;
end;
given B being Segre-like non trivial-yielding 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
closed_under_lines;
thus S is non trivial by A116;
A118: dom B = I by PARTFUN1:def 2;
A119: dom Carrier A = I by PARTFUN1:def 2;
thus S is strong
proof
let x,y be Point of Segre_Product A;
assume that
A120: x in S and
A121: y in S;
per cases;
suppose
x=y;
hence thesis;
end;
suppose
A122: x<>y;
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 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 as ManySortedSet of I by A128,A126,PARTFUN1:def 2
,RELAT_1:def 18;
A130: now
assume
A131: x1.indx(B) = y1.indx(B);
now
let i be object;
assume i in dom Carrier A;
per cases;
suppose
i<>indx(B);
hence x1.i = y1.i by A116,A120,A121,A127,A123,Th23;
end;
suppose
i=indx(B);
hence x1.i = y1.i by A131;
end;
end;
hence contradiction by A122,A127,A128,A123,A124,FUNCT_1:2;
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 be object st a in dom ({x1}+*(indx(B),l)) holds y1.a in {x1}+*(
indx(B),l).a
proof
let a be object;
assume a in dom ({x1}+*(indx(B),l));
then
A137: a in I by PARTFUN1:def 2;
per cases;
suppose
A138: a = indx(B);
then {x1}+*(indx(B),l).a = l by A135,FUNCT_7:31;
hence thesis by A134,A138,ZFMISC_1:32;
end;
suppose
A139: a <> indx(B);
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 thesis by A139,FUNCT_7:32;
end;
end;
{x1}+*(indx(B),l) c= Carrier A
proof
let i be object;
assume
A140: i in I;
then reconsider i1=i as Element of I;
thus {x1}+*(indx(B),l).i c= (Carrier A).i
proof
per cases;
suppose
A141: i=indx(B);
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 thesis by A141,YELLOW_6:2;
end;
suppose
A142: i<>indx(B);
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 thesis by A143,YELLOW_6:2;
end;
end;
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;
assume i <> indx(B);
then {x1}+*(indx(B),l).i = {x1}.i by FUNCT_7:32
.= {x1.i} by PZFMISC1:def 1;
hence thesis;
end;
then
A145: {x1}+*(indx(B),l) is Segre-like;
A146: for a be object st a in dom ({x1}+*(indx(B),l)) holds x1.a in {x1}+*(
indx(B),l).a
proof
let a be object;
assume a in dom ({x1}+*(indx(B),l));
then
A147: a in I by PARTFUN1:def 2;
per cases;
suppose
A148: a = indx(B);
then {x1}+*(indx(B),l).a = l by A135,FUNCT_7:31;
hence thesis by A134,A148,ZFMISC_1:32;
end;
suppose
A149: a <> indx(B);
x1.a in {x1.a} by TARSKI:def 1;
then x1.a in {x1}.a by A147,PZFMISC1:def 1;
hence thesis by A149,FUNCT_7:32;
end;
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 thesis;
end;
end;
thus S is closed_under_lines
proof
let l be Block of Segre_Product A;
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);
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 as Segre-like non trivial-yielding 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;
assume a in dom L;
per cases;
suppose
a <> indx(B);
hence thesis by A116,A153,A151,Th26;
end;
suppose
A159: a = indx(B);
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 L.j is non 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
assume
A168: a1.indx(B) = b1.indx(B);
A169: for o being object st o in dom a1 holds a1.o = b1.o
proof
let o be object;
assume o in dom a1;
per cases;
suppose
o <> indx(B);
hence thesis by A166,A164,Th23;
end;
suppose
o=indx(B);
hence thesis by A168;
end;
end;
dom a1 = I by PARTFUN1:def 2
.= dom b1 by PARTFUN1:def 2;
hence contradiction by A156,A169,FUNCT_1:2;
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 thesis by A159,A161;
end;
end;
hence thesis by A116,A151,A157,CARD_3:27;
end;
end;