:: PENCIL_1 semantic presentation
begin
theorem Th1: :: PENCIL_1:1
for f, g being Function st product f = product g & f is non-empty holds
g is non-empty
proof
let f, g be Function; ::_thesis: ( product f = product g & f is non-empty implies g is non-empty )
assume A1: product f = product g ; ::_thesis: ( not f is non-empty or g is non-empty )
now__::_thesis:_(_f_is_non-empty_implies_g_is_non-empty_)
assume that
A2: f is non-empty and
A3: not g is non-empty ; ::_thesis: contradiction
ex n being set 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 set st
( n in dom f & f . n = {} ) by FUNCT_1:def_3;
hence contradiction by A2, FUNCT_1:def_9; ::_thesis: verum
end;
hence ( not f is non-empty or g is non-empty ) ; ::_thesis: verum
end;
theorem Th2: :: PENCIL_1:2
for X being set holds
( 2 c= card X iff ex x, y being set st
( x in X & y in X & x <> y ) )
proof
let X be set ; ::_thesis: ( 2 c= card X iff ex x, y being set st
( x in X & y in X & x <> y ) )
thus ( 2 c= card X implies ex x, y being set st
( x in X & y in X & x <> y ) ) ::_thesis: ( ex x, y being set st
( x in X & y in X & x <> y ) implies 2 c= card X )
proof
assume 2 c= card X ; ::_thesis: ex x, y being set st
( x in X & y in X & x <> y )
then card 2 c= card X by CARD_1:def_2;
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; ::_thesis: ex y being set st
( x in X & y in X & x <> y )
take y = f . 1; ::_thesis: ( x in X & y in X & x <> y )
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; ::_thesis: ( y in X & x <> y )
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; ::_thesis: x <> y
thus x <> y by A1, A4, A5, FUNCT_1:def_4; ::_thesis: verum
end;
given x, y being set such that A6: ( x in X & y in X ) and
A7: x <> y ; ::_thesis: 2 c= card X
{x,y} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in X )
assume a in {x,y} ; ::_thesis: a in X
hence a in X by A6, TARSKI:def_2; ::_thesis: verum
end;
then card {x,y} c= card X by CARD_1:11;
hence 2 c= card X by A7, CARD_2:57; ::_thesis: verum
end;
theorem Th3: :: PENCIL_1:3
for X being set st 2 c= card X holds
for x being set ex y being set st
( y in X & x <> y )
proof
let X be set ; ::_thesis: ( 2 c= card X implies for x being set ex y being set st
( y in X & x <> y ) )
assume 2 c= card X ; ::_thesis: for x being set ex y being set st
( y in X & x <> y )
then consider a, b being set such that
A1: a in X and
A2: ( b in X & a <> b ) by Th2;
let x be set ; ::_thesis: ex y being set st
( y in X & x <> y )
percases ( x = a or x <> a ) ;
supposeA3: x = a ; ::_thesis: ex y being set st
( y in X & x <> y )
take b ; ::_thesis: ( b in X & x <> b )
thus ( b in X & x <> b ) by A2, A3; ::_thesis: verum
end;
supposeA4: x <> a ; ::_thesis: ex y being set st
( y in X & x <> y )
take a ; ::_thesis: ( a in X & x <> a )
thus ( a in X & x <> a ) by A1, A4; ::_thesis: verum
end;
end;
end;
theorem Th4: :: PENCIL_1:4
for X being set holds
( 2 c= card X iff not X is trivial )
proof
let X be set ; ::_thesis: ( 2 c= card X iff not X is trivial )
set z = the Element of X;
thus ( 2 c= card X implies not X is trivial ) ::_thesis: ( not X is trivial implies 2 c= card X )
proof
assume 2 c= card X ; ::_thesis: not X is trivial
then consider x, y being set such that
A1: x in X and
A2: y in X and
A3: x <> y by Th2;
now__::_thesis:_(_ex_z_being_set_st_X_=_{z}_implies_x_=_y_)
given z being set such that A4: X = {z} ; ::_thesis: x = y
thus x = z by A1, A4, TARSKI:def_1
.= y by A2, A4, TARSKI:def_1 ; ::_thesis: verum
end;
hence not X is trivial by A1, A3, ZFMISC_1:131; ::_thesis: verum
end;
assume A5: not X is trivial ; ::_thesis: 2 c= card X
then ( X c= { the Element of X} implies X = { the Element of X} ) ;
then consider w being set such that
A6: w in X and
A7: not w in { the Element of X} by A5, TARSKI:def_3;
w <> the Element of X by A7, TARSKI:def_1;
hence 2 c= card X by A6, Th2; ::_thesis: verum
end;
theorem Th5: :: PENCIL_1:5
for X being set holds
( 3 c= card X iff ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )
proof
let X be set ; ::_thesis: ( 3 c= card X iff ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )
thus ( 3 c= card X implies ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) ) ::_thesis: ( ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) implies 3 c= card X )
proof
assume 3 c= card X ; ::_thesis: ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
then card 3 c= card X by CARD_1:def_2;
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; ::_thesis: ex y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
take y = f . 1; ::_thesis: ex z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
take z = f . 2; ::_thesis: ( x in X & y in X & z in X & x <> y & x <> z & y <> z )
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; ::_thesis: ( y in X & z in X & x <> y & x <> z & y <> z )
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; ::_thesis: ( z in X & x <> y & x <> z & y <> z )
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; ::_thesis: ( x <> y & x <> z & y <> z )
thus x <> y by A1, A4, A5, FUNCT_1:def_4; ::_thesis: ( x <> z & y <> z )
thus x <> z by A1, A4, A6, FUNCT_1:def_4; ::_thesis: y <> z
thus y <> z by A1, A5, A6, FUNCT_1:def_4; ::_thesis: verum
end;
given x, y, z being set such that A7: ( x in X & y in X & z in X ) and
A8: ( x <> y & x <> z & y <> z ) ; ::_thesis: 3 c= card X
{x,y,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y,z} or a in X )
assume a in {x,y,z} ; ::_thesis: a in X
hence a in X by A7, ENUMSET1:def_1; ::_thesis: verum
end;
then card {x,y,z} c= card X by CARD_1:11;
hence 3 c= card X by A8, CARD_2:58; ::_thesis: verum
end;
theorem Th6: :: PENCIL_1:6
for X being set st 3 c= card X holds
for x, y being set ex z being set st
( z in X & x <> z & y <> z )
proof
let X be set ; ::_thesis: ( 3 c= card X implies for x, y being set ex z being set st
( z in X & x <> z & y <> z ) )
assume 3 c= card X ; ::_thesis: for x, y being set ex z being set st
( z in X & x <> z & y <> z )
then consider a, b, c being set 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 set ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
percases ( ( x <> a & y <> a ) or ( x <> a & y = a & x = b ) or ( x <> a & y = a & x <> b ) or ( x = a & y <> a & y = b ) or ( x = a & y <> a & y <> b ) or ( x = a & y = a ) ) ;
suppose ( x <> a & y <> a ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence ex z being set st
( z in X & x <> z & y <> z ) by A1; ::_thesis: verum
end;
suppose ( x <> a & y = a & x = b ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence ex z being set st
( z in X & x <> z & y <> z ) by A3, A5; ::_thesis: verum
end;
suppose ( x <> a & y = a & x <> b ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; ::_thesis: verum
end;
suppose ( x = a & y <> a & y = b ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence ex z being set st
( z in X & x <> z & y <> z ) by A3, A5; ::_thesis: verum
end;
suppose ( x = a & y <> a & y <> b ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; ::_thesis: verum
end;
suppose ( x = a & y = a ) ; ::_thesis: ex z being set st
( z in X & x <> z & y <> z )
hence ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; ::_thesis: verum
end;
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;
predx,y are_collinear means :Def1: :: PENCIL_1:def 1
( x = y or ex l being Block of S st {x,y} c= l );
end;
:: deftheorem Def1 defines are_collinear PENCIL_1:def_1_:_
for S being TopStruct
for x, y being Point of S holds
( x,y are_collinear iff ( x = y or ex l being Block of S st {x,y} c= l ) );
definition
let S be TopStruct ;
let T be Subset of S;
attrT is closed_under_lines means :Def2: :: PENCIL_1:def 2
for l being Block of S st 2 c= card (l /\ T) holds
l c= T;
attrT is strong means :Def3: :: PENCIL_1:def 3
for x, y being Point of S st x in T & y in T holds
x,y are_collinear ;
end;
:: deftheorem Def2 defines closed_under_lines PENCIL_1:def_2_:_
for S being TopStruct
for T being Subset of S holds
( T is closed_under_lines iff for l being Block of S st 2 c= card (l /\ T) holds
l c= T );
:: deftheorem Def3 defines strong PENCIL_1:def_3_:_
for S being TopStruct
for T being Subset of S holds
( T is strong iff for x, y being Point of S st x in T & y in T holds
x,y are_collinear );
definition
let S be TopStruct ;
attrS is void means :Def4: :: PENCIL_1:def 4
the topology of S is empty ;
attrS is degenerated means :Def5: :: PENCIL_1:def 5
the carrier of S is Block of S;
attrS is with_non_trivial_blocks means :Def6: :: PENCIL_1:def 6
for k being Block of S holds 2 c= card k;
attrS is identifying_close_blocks means :Def7: :: PENCIL_1:def 7
for k, l being Block of S st 2 c= card (k /\ l) holds
k = l;
attrS is truly-partial means :Def8: :: PENCIL_1:def 8
not for x, y being Point of S holds x,y are_collinear ;
attrS is without_isolated_points means :Def9: :: PENCIL_1:def 9
for x being Point of S ex l being Block of S st x in l;
attrS is connected means :: PENCIL_1:def 10
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 holds
for a, b being Point of S st a = f . i & b = f . (i + 1) holds
a,b are_collinear ) );
attrS is strongly_connected means :Def11: :: PENCIL_1:def 11
for x being Point of S
for X being Subset of S st X is closed_under_lines & X is strong holds
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 & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) );
end;
:: deftheorem Def4 defines void PENCIL_1:def_4_:_
for S being TopStruct holds
( S is void iff the topology of S is empty );
:: deftheorem Def5 defines degenerated PENCIL_1:def_5_:_
for S being TopStruct holds
( S is degenerated iff the carrier of S is Block of S );
:: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def_6_:_
for S being TopStruct holds
( S is with_non_trivial_blocks iff for k being Block of S holds 2 c= card k );
:: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def_7_:_
for S being TopStruct holds
( S is identifying_close_blocks iff for k, l being Block of S st 2 c= card (k /\ l) holds
k = l );
:: deftheorem Def8 defines truly-partial PENCIL_1:def_8_:_
for S being TopStruct holds
( S is truly-partial iff not for x, y being Point of S holds x,y are_collinear );
:: deftheorem Def9 defines without_isolated_points PENCIL_1:def_9_:_
for S being TopStruct holds
( S is without_isolated_points iff for x being Point of S ex l being Block of S st x in l );
:: deftheorem defines connected PENCIL_1:def_10_:_
for S being TopStruct holds
( S is connected iff 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 holds
for a, b being Point of S st a = f . i & b = f . (i + 1) holds
a,b are_collinear ) ) );
:: deftheorem Def11 defines strongly_connected PENCIL_1:def_11_:_
for S being TopStruct holds
( S is strongly_connected iff for x being Point of S
for X being Subset of S st X is closed_under_lines & X is strong holds
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 & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) ) );
theorem Th7: :: PENCIL_1:7
for X being non empty set st 3 c= card X holds
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
( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
proof
let X be non empty set ; ::_thesis: ( 3 c= card X implies 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
( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume A1: 3 c= card X ; ::_thesis: 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
( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
A2: 2 c= 3 by NAT_1:39;
then 2 c= card X by A1, XBOOLE_1:1;
then consider x, y being set such that
A3: ( x in X & y in X ) and
A4: x <> y by Th2;
{x,y} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in X )
assume a in {x,y} ; ::_thesis: a in X
hence a in X by A3, TARSKI:def_2; ::_thesis: verum
end;
then reconsider l = {x,y} as Subset of X ;
let S be TopStruct ; ::_thesis: ( the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } implies ( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume that
A5: the carrier of S = X and
A6: the topology of S = { L where L is Subset of X : 2 = card L } ; ::_thesis: ( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus not S is empty by A5; ::_thesis: ( not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
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 not S is void by A7, Def4; ::_thesis: ( not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
now__::_thesis:_not_X_in_F
assume X in F ; ::_thesis: contradiction
then ex L being Subset of X st
( X = L & 2 = card L ) ;
hence contradiction by A1, NAT_1:39; ::_thesis: verum
end;
then X is not Element of F ;
hence not S is degenerated by A5, A6, Def5; ::_thesis: ( not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
for x, y being Point of S holds x,y are_collinear
proof
let x, y be Point of S; ::_thesis: x,y are_collinear
percases ( x = y or x <> y ) ;
supposeA8: x = y ; ::_thesis: x,y are_collinear
consider z being set such that
A9: z in X and
A10: z <> x by A1, A2, Th3, XBOOLE_1:1;
reconsider z = z as Point of S by A5, A9;
A11: {x,y} c= {x,z}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in {x,z} )
assume a in {x,y} ; ::_thesis: a in {x,z}
then ( a = x or a = y ) by TARSKI:def_2;
hence a in {x,z} by A8, TARSKI:def_2; ::_thesis: verum
end;
{x,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,z} or a in X )
assume a in {x,z} ; ::_thesis: a in X
then ( a = x or a = z ) by TARSKI:def_2;
hence a in X by A5; ::_thesis: verum
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 x,y are_collinear by A11, Def1; ::_thesis: verum
end;
supposeA12: x <> y ; ::_thesis: x,y are_collinear
{x,y} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in X )
assume a in {x,y} ; ::_thesis: a in X
then ( a = x or a = y ) by TARSKI:def_2;
hence a in X by A5; ::_thesis: verum
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 x,y are_collinear by Def1; ::_thesis: verum
end;
end;
end;
hence not S is truly-partial by Def8; ::_thesis: ( S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus S is with_non_trivial_blocks ::_thesis: ( S is identifying_close_blocks & S is without_isolated_points )
proof
let k be Block of S; :: according to PENCIL_1:def_6 ::_thesis: 2 c= card k
k in the topology of S by A7;
then ex m being Subset of X st
( m = k & card m = 2 ) by A6;
hence 2 c= card k ; ::_thesis: verum
end;
thus S is identifying_close_blocks ::_thesis: S is without_isolated_points
proof
let k, l be Block of S; :: according to PENCIL_1:def_7 ::_thesis: ( 2 c= card (k /\ l) implies k = l )
assume 2 c= card (k /\ l) ; ::_thesis: k = l
then consider a, b being set such that
A13: ( a in k /\ l & b in k /\ l ) and
A14: a <> b by Th2;
A15: {a,b} c= k /\ l
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} or x in k /\ l )
assume x in {a,b} ; ::_thesis: x in k /\ l
hence x in k /\ l by A13, TARSKI:def_2; ::_thesis: verum
end;
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, PRE_POLY:8, XBOOLE_1:1;
hence k = l by A15, A19, A16, A17, PRE_POLY:8, XBOOLE_1:1; ::_thesis: verum
end;
thus S is without_isolated_points ::_thesis: verum
proof
let x be Point of S; :: according to PENCIL_1:def_9 ::_thesis: ex l being Block of S st x in l
consider z being set 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,z} or a in X )
assume a in {x,z} ; ::_thesis: a in X
then ( a = x or a = z ) by TARSKI:def_2;
hence a in X by A5, A20; ::_thesis: verum
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 = l as Block of S ;
take l ; ::_thesis: x in l
thus x in l by TARSKI:def_2; ::_thesis: verum
end;
end;
theorem Th8: :: PENCIL_1:8
for X being non empty set st 3 c= card X holds
for K being Subset of X st card K = 2 holds
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
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
proof
let X be non empty set ; ::_thesis: ( 3 c= card X implies for K being Subset of X st card K = 2 holds
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
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume A1: 3 c= card X ; ::_thesis: for K being Subset of X st card K = 2 holds
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
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
let K be Subset of X; ::_thesis: ( card K = 2 implies 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
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
assume A2: card K = 2 ; ::_thesis: 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
( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
then reconsider K9 = K as finite Subset of X ;
consider x, y being set such that
A3: x <> y and
A4: K9 = {x,y} by A2, CARD_2:60;
let S be TopStruct ; ::_thesis: ( the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } \ {K} implies ( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points ) )
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} ; ::_thesis: ( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
reconsider x = x, y = y as Point of S by A5, A4, ZFMISC_1:32;
consider z being set 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,z} or a in X )
assume a in {x,z} ; ::_thesis: a in X
then ( a = x or a = z ) by TARSKI:def_2;
hence a in X by A5, A7; ::_thesis: verum
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 not S is empty by A5; ::_thesis: ( not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
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: not { L where L is Subset of X : 2 = card L } \ {K} is empty by XBOOLE_1:37;
hence not S is void by A6, Def4; ::_thesis: ( not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
reconsider F = { L where L is Subset of X : 2 = card L } \ {K} as non empty set by A11, XBOOLE_1:37;
now__::_thesis:_not_X_in_F
assume X in F ; ::_thesis: contradiction
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 ) ;
hence contradiction by A1, NAT_1:39; ::_thesis: verum
end;
then X is not Element of F ;
hence not S is degenerated by A5, A6, Def5; ::_thesis: ( S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
thus S is truly-partial ::_thesis: ( S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )
proof
take x ; :: according to PENCIL_1:def_8 ::_thesis: not for y being Point of S holds x,y are_collinear
take y ; ::_thesis: not x,y are_collinear
for l being Block of S holds not {x,y} c= l
proof
let l be Block of S; ::_thesis: not {x,y} c= l
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 set 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__::_thesis:_not_{x,y}_c=_l
assume A17: {x,y} c= l ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence not {x,y} c= l ; ::_thesis: verum
end;
hence not x,y are_collinear by A3, Def1; ::_thesis: verum
end;
thus S is with_non_trivial_blocks ::_thesis: ( S is identifying_close_blocks & S is without_isolated_points )
proof
let k be Block of S; :: according to PENCIL_1:def_6 ::_thesis: 2 c= card k
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 2 c= card k ; ::_thesis: verum
end;
thus S is identifying_close_blocks ::_thesis: S is without_isolated_points
proof
let k, l be Block of S; :: according to PENCIL_1:def_7 ::_thesis: ( 2 c= card (k /\ l) implies k = l )
assume 2 c= card (k /\ l) ; ::_thesis: k = l
then consider a, b being set such that
A19: ( a in k /\ l & b in k /\ l ) and
A20: a <> b by Th2;
A21: {a,b} c= k /\ l
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} or x in k /\ l )
assume x in {a,b} ; ::_thesis: x in k /\ l
hence x in k /\ l by A19, TARSKI:def_2; ::_thesis: verum
end;
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, PRE_POLY:8, XBOOLE_1:1;
hence k = l by A21, A25, A22, A23, PRE_POLY:8, XBOOLE_1:1; ::_thesis: verum
end;
A26: 2 c= 3 by NAT_1:39;
thus S is without_isolated_points ::_thesis: verum
proof
let p be Point of S; :: according to PENCIL_1:def_9 ::_thesis: ex l being Block of S st p in l
percases ( ( p <> x & p <> y ) or p = x or p = y ) ;
supposeA27: ( p <> x & p <> y ) ; ::_thesis: ex l being Block of S st p in l
consider z being set 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {p,z} or a in X )
assume a in {p,z} ; ::_thesis: a in X
then ( a = p or a = z ) by TARSKI:def_2;
hence a in X by A5, A28; ::_thesis: verum
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 = el as Block of S by A6, A30, XBOOLE_0:def_5;
take el ; ::_thesis: p in el
thus p in el by TARSKI:def_2; ::_thesis: verum
end;
supposeA31: ( p = x or p = y ) ; ::_thesis: ex l being Block of S st p in l
consider z being set such that
A32: z in X and
A33: ( z <> x & z <> y ) by A1, Th6;
{p,z} c= X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {p,z} or a in X )
assume a in {p,z} ; ::_thesis: a in X
then ( a = p or a = z ) by TARSKI:def_2;
hence a in X by A5, A32; ::_thesis: verum
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 = el as Block of S by A6, A34, XBOOLE_0:def_5;
take el ; ::_thesis: p in el
thus p in el by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
end;
registration
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks non truly-partial without_isolated_points for TopStruct ;
existence
ex b1 being TopStruct st
( b1 is strict & not b1 is empty & not b1 is void & not b1 is degenerated & not b1 is truly-partial & b1 is with_non_trivial_blocks & b1 is identifying_close_blocks & b1 is without_isolated_points )
proof
{ L where L is Subset of 3 : 2 = card L } c= bool 3
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { L where L is Subset of 3 : 2 = card L } or x in bool 3 )
assume x in { L where L is Subset of 3 : 2 = card L } ; ::_thesis: x in bool 3
then ex L being Subset of 3 st
( x = L & 2 = card L ) ;
hence x in bool 3 ; ::_thesis: verum
end;
then reconsider B = { L where L is Subset of 3 : 2 = card L } as Subset-Family of 3 ;
take TopStruct(# 3,B #) ; ::_thesis: ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & not TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points )
3 = card 3 by CARD_1:def_2;
hence ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & not TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points ) by Th7; ::_thesis: verum
end;
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points for TopStruct ;
existence
ex b1 being TopStruct st
( b1 is strict & not b1 is empty & not b1 is void & not b1 is degenerated & b1 is truly-partial & b1 is with_non_trivial_blocks & b1 is identifying_close_blocks & b1 is without_isolated_points )
proof
( 2 c= 3 & card 2 = 2 ) by CARD_1:def_2, 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { L where L is Subset of 3 : 2 = card L } or x in bool 3 )
assume x in { L where L is Subset of 3 : 2 = card L } ; ::_thesis: x in bool 3
then ex L being Subset of 3 st
( x = L & 2 = card L ) ;
hence x in bool 3 ; ::_thesis: verum
end;
then reconsider B = { L where L is Subset of 3 : 2 = card L } \ {K} as Subset-Family of 3 by XBOOLE_1:1;
take TopStruct(# 3,B #) ; ::_thesis: ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points )
3 c= card 3 by CARD_1:def_2;
hence ( TopStruct(# 3,B #) is strict & not TopStruct(# 3,B #) is empty & not TopStruct(# 3,B #) is void & not TopStruct(# 3,B #) is degenerated & TopStruct(# 3,B #) is truly-partial & TopStruct(# 3,B #) is with_non_trivial_blocks & TopStruct(# 3,B #) is identifying_close_blocks & TopStruct(# 3,B #) is without_isolated_points ) by A1, Th8; ::_thesis: verum
end;
end;
registration
let S be non void TopStruct ;
cluster the topology of S -> non empty ;
coherence
not the topology of S is empty 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 :: PENCIL_1:def 12
ex l being Block of S st {x,y} c= l;
compatibility
( x,y are_collinear iff ex l being Block of S st {x,y} c= l )
proof
thus ( x,y are_collinear implies ex l being Block of S st {x,y} c= l ) ::_thesis: ( ex l being Block of S st {x,y} c= l implies x,y are_collinear )
proof
assume A1: x,y are_collinear ; ::_thesis: ex l being Block of S st {x,y} c= l
percases ( x = y or x <> y ) ;
supposeA2: x = y ; ::_thesis: ex l being Block of S st {x,y} c= l
consider l being Block of S such that
A3: x in l by Def9;
take l ; ::_thesis: {x,y} c= l
thus {x,y} c= l by A2, A3, ZFMISC_1:32; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: ex l being Block of S st {x,y} c= l
hence ex l being Block of S st {x,y} c= l by A1, Def1; ::_thesis: verum
end;
end;
end;
given l being Block of S such that A4: {x,y} c= l ; ::_thesis: x,y are_collinear
thus x,y are_collinear by A4, Def1; ::_thesis: verum
end;
end;
:: deftheorem defines are_collinear PENCIL_1:def_12_:_
for S being without_isolated_points TopStruct
for x, y being Point of S holds
( x,y are_collinear iff ex l being Block of S st {x,y} c= l );
definition
mode PLS is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct ;
end;
definition
let F be Relation;
attrF is TopStruct-yielding means :Def13: :: PENCIL_1:def 13
for x being set st x in rng F holds
x is TopStruct ;
end;
:: deftheorem Def13 defines TopStruct-yielding PENCIL_1:def_13_:_
for F being Relation holds
( F is TopStruct-yielding iff for x being set st x in rng F holds
x is TopStruct );
registration
cluster Relation-like Function-like TopStruct-yielding -> 1-sorted-yielding for set ;
coherence
for b1 being Function st b1 is TopStruct-yielding holds
b1 is 1-sorted-yielding
proof
let F be Function; ::_thesis: ( F is TopStruct-yielding implies F is 1-sorted-yielding )
assume A1: F is TopStruct-yielding ; ::_thesis: F is 1-sorted-yielding
let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in dom F or F . x is 1-sorted )
assume x in dom F ; ::_thesis: F . x is 1-sorted
then F . x in rng F by FUNCT_1:def_3;
hence F . x is 1-sorted by A1, Def13; ::_thesis: verum
end;
end;
registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) TopStruct-yielding for set ;
existence
ex b1 being ManySortedSet of I st b1 is TopStruct-yielding
proof
set R = the TopStruct ;
take I --> the TopStruct ; ::_thesis: I --> the TopStruct is TopStruct-yielding
let v be set ; :: according to PENCIL_1:def_13 ::_thesis: ( v in rng (I --> the TopStruct ) implies v is TopStruct )
assume A1: v in rng (I --> the TopStruct ) ; ::_thesis: v is TopStruct
rng (I --> the TopStruct ) c= { the TopStruct } by FUNCOP_1:13;
hence v is TopStruct by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like TopStruct-yielding for set ;
existence
ex b1 being Function st b1 is TopStruct-yielding
proof
set F = the TopStruct-yielding ManySortedSet of {} ;
take the TopStruct-yielding ManySortedSet of {} ; ::_thesis: the TopStruct-yielding ManySortedSet of {} is TopStruct-yielding
thus the TopStruct-yielding ManySortedSet of {} is TopStruct-yielding ; ::_thesis: verum
end;
end;
definition
let F be Relation;
attrF is non-void-yielding means :Def14: :: PENCIL_1:def 14
for S being TopStruct st S in rng F holds
not S is void ;
end;
:: deftheorem Def14 defines non-void-yielding PENCIL_1:def_14_:_
for F being Relation holds
( F is non-void-yielding iff for S being TopStruct st S in rng F holds
not S is void );
definition
let F be TopStruct-yielding Function;
redefine attr F is non-void-yielding means :: PENCIL_1:def 15
for i being set st i in rng F holds
i is non void TopStruct ;
compatibility
( F is non-void-yielding iff for i being set st i in rng F holds
i is non void TopStruct )
proof
thus ( F is non-void-yielding implies for i being set st i in rng F holds
i is non void TopStruct ) by Def13, Def14; ::_thesis: ( ( for i being set st i in rng F holds
i is non void TopStruct ) implies F is non-void-yielding )
assume A1: for i being set st i in rng F holds
i is non void TopStruct ; ::_thesis: F is non-void-yielding
let S be TopStruct ; :: according to PENCIL_1:def_14 ::_thesis: ( S in rng F implies not S is void )
thus ( S in rng F implies not S is void ) by A1; ::_thesis: verum
end;
end;
:: deftheorem defines non-void-yielding PENCIL_1:def_15_:_
for F being TopStruct-yielding Function holds
( F is non-void-yielding iff for i being set st i in rng F holds
i is non void TopStruct );
definition
let F be Relation;
attrF is trivial-yielding means :Def16: :: PENCIL_1:def 16
for S being set st S in rng F holds
S is trivial ;
end;
:: deftheorem Def16 defines trivial-yielding PENCIL_1:def_16_:_
for F being Relation holds
( F is trivial-yielding iff for S being set st S in rng F holds
S is trivial );
definition
let F be Relation;
attrF is non-Trivial-yielding means :Def17: :: PENCIL_1:def 17
for S being 1-sorted st S in rng F holds
not S is trivial ;
end;
:: deftheorem Def17 defines non-Trivial-yielding PENCIL_1:def_17_:_
for F being Relation holds
( F is non-Trivial-yielding iff for S being 1-sorted st S in rng F holds
not S is trivial );
registration
cluster Relation-like non-Trivial-yielding -> non-Empty for set ;
coherence
for b1 being Relation st b1 is non-Trivial-yielding holds
b1 is non-Empty
proof
let F be Relation; ::_thesis: ( F is non-Trivial-yielding implies F is non-Empty )
assume A1: F is non-Trivial-yielding ; ::_thesis: F is non-Empty
let i be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not i in rng F or not i is empty )
assume i in rng F ; ::_thesis: not i is empty
hence not i is empty by A1, Def17; ::_thesis: verum
end;
end;
definition
let F be 1-sorted-yielding Function;
redefine attr F is non-Trivial-yielding means :: PENCIL_1:def 18
for i being set st i in rng F holds
i is non trivial 1-sorted ;
compatibility
( F is non-Trivial-yielding iff for i being set st i in rng F holds
i is non trivial 1-sorted )
proof
hereby ::_thesis: ( ( for i being set st i in rng F holds
i is non trivial 1-sorted ) implies F is non-Trivial-yielding )
assume A1: F is non-Trivial-yielding ; ::_thesis: for i being set st i in rng F holds
i is non trivial 1-sorted
let i be set ; ::_thesis: ( i in rng F implies i is non trivial 1-sorted )
assume A2: i in rng F ; ::_thesis: i is non trivial 1-sorted
then ex x being set st
( x in dom F & i = F . x ) by FUNCT_1:def_3;
hence i is non trivial 1-sorted by A1, A2, Def17, PRALG_1:def_11; ::_thesis: verum
end;
assume A3: for i being set st i in rng F holds
i is non trivial 1-sorted ; ::_thesis: F is non-Trivial-yielding
let S be 1-sorted ; :: according to PENCIL_1:def_17 ::_thesis: ( S in rng F implies not S is trivial )
thus ( S in rng F implies not S is trivial ) by A3; ::_thesis: verum
end;
end;
:: deftheorem defines non-Trivial-yielding PENCIL_1:def_18_:_
for F being 1-sorted-yielding Function holds
( F is non-Trivial-yielding iff for i being set st i in rng F holds
i is non trivial 1-sorted );
definition
let I be non empty set ;
let A be TopStruct-yielding ManySortedSet of I;
let j be Element of I;
:: original: .
redefine funcA . j -> TopStruct ;
coherence
A . j is TopStruct
proof
dom A = I by PARTFUN1:def_2;
then A . j in rng A by FUNCT_1:def_3;
hence A . j is TopStruct by Def13; ::_thesis: verum
end;
end;
definition
let F be Relation;
attrF is PLS-yielding means :Def19: :: PENCIL_1:def 19
for x being set st x in rng F holds
x is PLS;
end;
:: deftheorem Def19 defines PLS-yielding PENCIL_1:def_19_:_
for F being Relation holds
( F is PLS-yielding iff for x being set st x in rng F holds
x is PLS );
registration
cluster Relation-like Function-like PLS-yielding -> non-Empty TopStruct-yielding for set ;
coherence
for b1 being Function st b1 is PLS-yielding holds
( b1 is non-Empty & b1 is TopStruct-yielding )
proof
let f be Function; ::_thesis: ( f is PLS-yielding implies ( f is non-Empty & f is TopStruct-yielding ) )
assume A1: f is PLS-yielding ; ::_thesis: ( f is non-Empty & f is TopStruct-yielding )
thus f is non-Empty ::_thesis: f is TopStruct-yielding
proof
let S be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( not S in rng f or not S is empty )
assume S in rng f ; ::_thesis: not S is empty
hence not S is empty by A1, Def19; ::_thesis: verum
end;
let x be set ; :: according to PENCIL_1:def_13 ::_thesis: ( x in rng f implies x is TopStruct )
assume x in rng f ; ::_thesis: x is TopStruct
hence x is TopStruct by A1, Def19; ::_thesis: verum
end;
cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> TopStruct-yielding non-void-yielding for set ;
coherence
for b1 being TopStruct-yielding Function st b1 is PLS-yielding holds
b1 is non-void-yielding
proof
let f be TopStruct-yielding Function; ::_thesis: ( f is PLS-yielding implies f is non-void-yielding )
assume A2: f is PLS-yielding ; ::_thesis: f is non-void-yielding
let x be set ; :: according to PENCIL_1:def_15 ::_thesis: ( x in rng f implies x is non void TopStruct )
assume x in rng f ; ::_thesis: x is non void TopStruct
hence x is non void TopStruct by A2, Def19; ::_thesis: verum
end;
cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> TopStruct-yielding non-Trivial-yielding for set ;
coherence
for b1 being TopStruct-yielding Function st b1 is PLS-yielding holds
b1 is non-Trivial-yielding
proof
let f be TopStruct-yielding Function; ::_thesis: ( f is PLS-yielding implies f is non-Trivial-yielding )
assume A3: f is PLS-yielding ; ::_thesis: f is non-Trivial-yielding
let x be set ; :: according to PENCIL_1:def_18 ::_thesis: ( x in rng f implies x is non trivial 1-sorted )
assume x in rng f ; ::_thesis: x is non trivial 1-sorted
then reconsider S1 = x as non empty non void with_non_trivial_blocks TopStruct by A3, Def19;
consider s being set such that
A4: s in the topology of S1 by XBOOLE_0:def_1;
reconsider s = s as Block of S1 by A4;
2 c= card s by Def6;
then ex s1, s2 being set st
( s1 in s & s2 in s & s1 <> s2 ) by Th2;
hence x is non trivial 1-sorted by A4, STRUCT_0:def_10; ::_thesis: verum
end;
end;
registration
let I be set ;
cluster Relation-like I -defined Function-like V14(I) PLS-yielding for set ;
existence
ex b1 being ManySortedSet of I st b1 is PLS-yielding
proof
set R = the PLS;
take I --> the PLS ; ::_thesis: I --> the PLS is PLS-yielding
let v be set ; :: according to PENCIL_1:def_19 ::_thesis: ( v in rng (I --> the PLS) implies v is PLS )
assume A1: v in rng (I --> the PLS) ; ::_thesis: v is PLS
rng (I --> the PLS) c= { the PLS} by FUNCOP_1:13;
hence v is PLS by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
definition
let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
let j be Element of I;
:: original: .
redefine funcA . j -> PLS;
coherence
A . j is PLS
proof
dom A = I by PARTFUN1:def_2;
then A . j in rng A by FUNCT_1:def_3;
hence A . j is PLS by Def19; ::_thesis: verum
end;
end;
definition
let I be set ;
let A be ManySortedSet of I;
attrA is Segre-like means :Def20: :: PENCIL_1:def 20
ex i being Element of I st
for j being Element of I st i <> j holds
A . j is 1 -element ;
end;
:: deftheorem Def20 defines Segre-like PENCIL_1:def_20_:_
for I being set
for A being ManySortedSet of I holds
( A is Segre-like iff ex i being Element of I st
for j being Element of I st i <> j holds
A . j is 1 -element );
registration
let I be set ;
let A be ManySortedSet of I;
cluster{A} -> trivial-yielding ;
coherence
{A} is trivial-yielding
proof
let a be set ; :: according to PENCIL_1:def_16 ::_thesis: ( a in rng {A} implies a is trivial )
assume a in rng {A} ; ::_thesis: a is trivial
then consider i being set 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 a is trivial ; ::_thesis: verum
end;
end;
theorem :: PENCIL_1:9
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 not A +* (i,S) is trivial-yielding
proof
let I be non empty set ; ::_thesis: for A being ManySortedSet of I
for i being Element of I
for S being non trivial set holds not A +* (i,S) is trivial-yielding
let A be ManySortedSet of I; ::_thesis: for i being Element of I
for S being non trivial set holds not A +* (i,S) is trivial-yielding
let i be Element of I; ::_thesis: for S being non trivial set holds not A +* (i,S) is trivial-yielding
let S be non trivial set ; ::_thesis: not A +* (i,S) is trivial-yielding
take a = (A +* (i,S)) . i; :: according to PENCIL_1:def_16 ::_thesis: ( a in rng (A +* (i,S)) & not a is trivial )
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; ::_thesis: not a is trivial
dom A = I by PARTFUN1:def_2;
hence not a is trivial by FUNCT_7:31; ::_thesis: verum
end;
registration
let I be non empty set ;
let A be ManySortedSet of I;
cluster{A} -> Segre-like ;
coherence
{A} is Segre-like
proof
set i = the Element of I;
take the Element of I ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st the Element of I <> j holds
{A} . j is 1 -element
let j be Element of I; ::_thesis: ( the Element of I <> j implies {A} . j is 1 -element )
assume the Element of I <> j ; ::_thesis: {A} . j is 1 -element
{A} . j = {(A . j)} by PZFMISC1:def_1;
hence {A} . j is 1 -element ; ::_thesis: verum
end;
end;
theorem :: PENCIL_1:10
for I being non empty set
for A being ManySortedSet of I
for i, S being set holds {A} +* (i,S) is Segre-like
proof
let I be non empty set ; ::_thesis: for A being ManySortedSet of I
for i, S being set holds {A} +* (i,S) is Segre-like
let A be ManySortedSet of I; ::_thesis: for i, S being set holds {A} +* (i,S) is Segre-like
let i, S be set ; ::_thesis: {A} +* (i,S) is Segre-like
percases ( not i in I or i in I ) ;
suppose not i in I ; ::_thesis: {A} +* (i,S) is Segre-like
then not i in dom {A} by PARTFUN1:def_2;
hence {A} +* (i,S) is Segre-like by FUNCT_7:def_3; ::_thesis: verum
end;
suppose i in I ; ::_thesis: {A} +* (i,S) is Segre-like
then reconsider i = i as Element of I ;
take i ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st i <> j holds
({A} +* (i,S)) . j is 1 -element
let j be Element of I; ::_thesis: ( i <> j implies ({A} +* (i,S)) . j is 1 -element )
assume A1: i <> j ; ::_thesis: ({A} +* (i,S)) . j is 1 -element
{A} . j = {(A . j)} by PZFMISC1:def_1;
hence ({A} +* (i,S)) . j is 1 -element by A1, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
theorem Th11: :: PENCIL_1:11
for I being non empty set
for A being 1-sorted-yielding non-Empty ManySortedSet of I
for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A
proof
let I be non empty set ; ::_thesis: for A being 1-sorted-yielding non-Empty ManySortedSet of I
for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A
let A be 1-sorted-yielding non-Empty ManySortedSet of I; ::_thesis: for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A
let B be Element of Carrier A; ::_thesis: {B} is ManySortedSubset of Carrier A
{B} c= Carrier A
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {B} . i c= (Carrier A) . i )
assume A1: i in I ; ::_thesis: {B} . i c= (Carrier A) . 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: not A . j is 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 {B} . i c= (Carrier A) . i by YELLOW_6:2; ::_thesis: verum
end;
hence {B} is ManySortedSubset of Carrier A by PBOOLE:def_18; ::_thesis: verum
end;
registration
let I be non empty set ;
let A be 1-sorted-yielding non-Empty ManySortedSet of I;
cluster Relation-like V2() I -defined Function-like V14(I) trivial-yielding Segre-like for ManySortedSubset of Carrier A;
existence
ex b1 being ManySortedSubset of Carrier A st
( b1 is Segre-like & b1 is trivial-yielding & b1 is V2() )
proof
set B = the Element of Carrier A;
reconsider C = { the Element of Carrier A} as ManySortedSubset of Carrier A by Th11;
take C ; ::_thesis: ( C is Segre-like & C is trivial-yielding & C is V2() )
thus ( C is Segre-like & C is trivial-yielding & C is V2() ) ; ::_thesis: verum
end;
end;
registration
let I be non empty set ;
let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I;
cluster Relation-like V2() I -defined Function-like V14(I) non trivial-yielding Segre-like for ManySortedSubset of Carrier A;
existence
ex b1 being ManySortedSubset of Carrier A st
( b1 is Segre-like & not b1 is trivial-yielding & b1 is V2() )
proof
set B = the Element of Carrier A;
set i1 = the Element of I;
A1: ex R being 1-sorted st
( R = A . the Element of I & the carrier of R = (Carrier A) . the Element of I ) by PRALG_1:def_13;
then reconsider b1 = the Element of Carrier A . the Element of I as Element of (A . the Element of I) by PBOOLE:def_14;
reconsider B = the Element of Carrier A as ManySortedSet of I ;
dom A = I by PARTFUN1:def_2;
then A . the Element of I in rng A by FUNCT_1:def_3;
then not A . the Element of I is trivial by Def17;
then reconsider Ai1 = the carrier of (A . the Element of I) 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 . the Element of I) by Th2;
then consider b2 being set such that
A2: b2 in the carrier of (A . the Element of I) and
A3: b1 <> b2 by Th3;
reconsider b2 = b2 as Element of (A . the Element of I) by A2;
set B1 = B +* ( the Element of I,b2);
A4: for i being set st i in I holds
(B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
proof
let i be set ; ::_thesis: ( i in I implies (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i )
assume A5: i in I ; ::_thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
percases ( i <> the Element of I or i = the Element of I ) ;
suppose i <> the Element of I ; ::_thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
then (B +* ( the Element of I,b2)) . i = B . i by FUNCT_7:32;
hence (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i by A5, PBOOLE:def_14; ::_thesis: verum
end;
supposeA6: i = the Element of I ; ::_thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
then the Element of I in dom B by A5, PARTFUN1:def_2;
hence (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i by A1, A6, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
{B,(B +* ( the Element of I,b2))} c= Carrier A
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . i )
assume A7: i in I ; ::_thesis: {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . 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: not A . j is 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;
(B +* ( the Element of I,b2)) . j is Element of (Carrier A) . j by A4;
then (B +* ( the Element of I,b2)) . j is Element of (A . j) by YELLOW_6:2;
then {(B . j),((B +* ( the Element of I,b2)) . j)} c= the carrier of (A . j) by A8, A9, ZFMISC_1:32;
then {B,(B +* ( the Element of I,b2))} . j c= the carrier of (A . j) by PZFMISC1:def_2;
hence {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . i by YELLOW_6:2; ::_thesis: verum
end;
then reconsider C = {B,(B +* ( the Element of I,b2))} as ManySortedSubset of Carrier A by PBOOLE:def_18;
dom B = I by PARTFUN1:def_2;
then (B +* ( the Element of I,b2)) . the Element of I = b2 by FUNCT_7:31;
then A10: C . the Element of I = {b1,b2} by PZFMISC1:def_2;
A11: now__::_thesis:_not_C_._the_Element_of_I_is_trivial
assume C . the Element of I is trivial ; ::_thesis: contradiction
then ( C . the Element of I is empty or ex x being set st C . the Element of I = {x} ) by ZFMISC_1:131;
hence contradiction by A3, A10, ZFMISC_1:5; ::_thesis: verum
end;
take C ; ::_thesis: ( C is Segre-like & not C is trivial-yielding & C is V2() )
thus C is Segre-like ::_thesis: ( not C is trivial-yielding & C is V2() )
proof
take the Element of I ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st the Element of I <> j holds
C . j is 1 -element
let j be Element of I; ::_thesis: ( the Element of I <> j implies C . j is 1 -element )
assume the Element of I <> j ; ::_thesis: C . j is 1 -element
then B . j = (B +* ( the Element of I,b2)) . j by FUNCT_7:32;
then C . j = {(B . j),(B . j)} by PZFMISC1:def_2
.= {(B . j)} by ENUMSET1:29 ;
hence C . j is 1 -element ; ::_thesis: verum
end;
dom C = I by PARTFUN1:def_2;
then C . the Element of I in rng C by FUNCT_1:def_3;
hence not C is trivial-yielding by A11, Def16; ::_thesis: C is V2()
thus C is V2() ; ::_thesis: verum
end;
end;
registration
let I be non empty set ;
cluster Relation-like I -defined Function-like V14(I) non trivial-yielding Segre-like for set ;
existence
ex b1 being ManySortedSet of I st
( b1 is Segre-like & not b1 is trivial-yielding )
proof
set B = the ManySortedSet of I;
set i = the Element of I;
take C = { the ManySortedSet of I} +* ( the Element of I,{0,1}); ::_thesis: ( C is Segre-like & not C is trivial-yielding )
thus C is Segre-like ::_thesis: not C is trivial-yielding
proof
take the Element of I ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st the Element of I <> j holds
C . j is 1 -element
let j be Element of I; ::_thesis: ( the Element of I <> j implies C . j is 1 -element )
assume j <> the Element of I ; ::_thesis: C . j is 1 -element
then A1: C . j = { the ManySortedSet of I} . j by FUNCT_7:32;
j in I ;
then A2: j in dom { the ManySortedSet of I} by PARTFUN1:def_2;
then C . j in rng { the ManySortedSet of I} by A1, FUNCT_1:def_3;
then ( not C . j is empty & C . j is trivial ) by A2, A1, Def16, FUNCT_1:def_9;
hence C . j is 1 -element ; ::_thesis: verum
end;
thus not C is trivial-yielding ::_thesis: verum
proof
take S = C . the Element of I; :: according to PENCIL_1:def_16 ::_thesis: ( S in rng C & not S is trivial )
dom C = I by PARTFUN1:def_2;
hence S in rng C by FUNCT_1:def_3; ::_thesis: not S is trivial
dom { the ManySortedSet of I} = I by PARTFUN1:def_2;
then A3: C . the Element of 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 not S is trivial by A3, Th4; ::_thesis: verum
end;
end;
end;
definition
let I be non empty set ;
let B be non trivial-yielding Segre-like ManySortedSet of I;
func indx B -> Element of I means :Def21: :: PENCIL_1:def 21
not B . it is trivial ;
existence
not for b1 being Element of I holds B . b1 is trivial
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 ; ::_thesis: not B . i is trivial
now__::_thesis:_not_B_._i_is_trivial
assume A2: B . i is trivial ; ::_thesis: contradiction
for S being set st S in rng B holds
S is trivial
proof
let S be set ; ::_thesis: ( S in rng B implies S is trivial )
assume S in rng B ; ::_thesis: S is trivial
then consider j being set such that
A3: j in dom B and
A4: S = B . j by FUNCT_1:def_3;
reconsider j = j as Element of I by A3, PARTFUN1:def_2;
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: S is trivial
hence S is trivial by A2, A4; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: S is trivial
then B . j is 1 -element by A1;
hence S is trivial by A4; ::_thesis: verum
end;
end;
end;
hence contradiction by Def16; ::_thesis: verum
end;
hence not B . i is trivial ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of I st not B . b1 is trivial & not B . b2 is trivial holds
b1 = b2
proof
let i1, i2 be Element of I; ::_thesis: ( not B . i1 is trivial & not B . i2 is trivial implies i1 = i2 )
assume that
A5: not B . i1 is trivial and
A6: not B . i2 is trivial ; ::_thesis: i1 = i2
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: not B . i2 is 1 -element by A6;
not B . i1 is 1 -element by A5;
hence i1 = i by A7
.= i2 by A7, A8 ;
::_thesis: verum
end;
end;
:: deftheorem Def21 defines indx PENCIL_1:def_21_:_
for I being non empty set
for B being non trivial-yielding Segre-like ManySortedSet of I
for b3 being Element of I holds
( b3 = indx B iff not B . b3 is trivial );
theorem Th12: :: PENCIL_1:12
for I being non empty set
for A being non trivial-yielding Segre-like 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 ; ::_thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for i being Element of I st i <> indx A holds
A . i is 1 -element
let A be non trivial-yielding Segre-like ManySortedSet of I; ::_thesis: for i being Element of I st i <> indx A holds
A . i is 1 -element
let i be Element of I; ::_thesis: ( i <> indx A implies A . i is 1 -element )
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__::_thesis:_not_indx_A_<>_j
assume indx A <> j ; ::_thesis: contradiction
then A . (indx A) is 1 -element by A1;
hence contradiction by Def21; ::_thesis: verum
end;
assume i <> indx A ; ::_thesis: A . i is 1 -element
hence A . i is 1 -element by A1, A2; ::_thesis: verum
end;
registration
let I be non empty set ;
cluster Relation-like I -defined Function-like V14(I) non trivial-yielding Segre-like -> V2() for set ;
coherence
for b1 being ManySortedSet of I st b1 is Segre-like & not b1 is trivial-yielding holds
b1 is V2()
proof
let f be ManySortedSet of I; ::_thesis: ( f is Segre-like & not f is trivial-yielding implies f is V2() )
assume ( f is Segre-like & not f is trivial-yielding ) ; ::_thesis: f is V2()
then reconsider g = f as non trivial-yielding Segre-like ManySortedSet of I ;
now__::_thesis:_not_{}_in_rng_g
assume {} in rng g ; ::_thesis: contradiction
then consider i being set such that
A1: i in dom f and
A2: g . i = {} by FUNCT_1:def_3;
reconsider i = i as Element of I by A1, PARTFUN1:def_2;
percases ( i = indx g or i <> indx g ) ;
suppose i = indx g ; ::_thesis: contradiction
hence contradiction by A2, Def21; ::_thesis: verum
end;
suppose i <> indx g ; ::_thesis: contradiction
then g . i is 1 -element by Th12;
hence contradiction by A2; ::_thesis: verum
end;
end;
end;
hence f is V2() by RELAT_1:def_9; ::_thesis: verum
end;
end;
theorem Th13: :: PENCIL_1:13
for I being non empty set
for A being ManySortedSet of I holds
( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )
proof
let I be non empty set ; ::_thesis: for A being ManySortedSet of I holds
( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )
let A be ManySortedSet of I; ::_thesis: ( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )
A1: dom A = I by PARTFUN1:def_2;
thus ( 2 c= card (product A) implies ( A is V2() & not A is trivial-yielding ) ) ::_thesis: ( A is V2() & not A is trivial-yielding implies 2 c= card (product A) )
proof
assume 2 c= card (product A) ; ::_thesis: ( A is V2() & not A is trivial-yielding )
then consider a, b being set 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 set st e in dom A holds
a1 . e in A . e by A2, CARD_3:def_5;
thus A is V2() ::_thesis: not A is trivial-yielding
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not A . i is empty )
assume i in I ; ::_thesis: not A . i is empty
hence not A . i is empty by A1, A6; ::_thesis: verum
end;
consider b1 being Function such that
A7: ( b = b1 & dom b1 = dom A ) and
A8: for e being set st e in dom A holds
b1 . e in A . e by A3, CARD_3:def_5;
consider e being set such that
A9: e in dom A and
A10: b1 . e <> a1 . e by A4, A5, A7, FUNCT_1:2;
thus not A is trivial-yielding ::_thesis: verum
proof
take A . e ; :: according to PENCIL_1:def_16 ::_thesis: ( A . e in rng A & not A . e is trivial )
thus A . e in rng A by A9, FUNCT_1:def_3; ::_thesis: not A . e is trivial
( a1 . e in A . e & b1 . e in A . e ) by A6, A8, A9;
then 2 c= card (A . e) by A10, Th2;
hence not A . e is trivial by Th4; ::_thesis: verum
end;
end;
assume A11: ( A is V2() & not A is trivial-yielding ) ; ::_thesis: 2 c= card (product A)
then consider r being set such that
A12: r in rng A and
A13: not r is trivial by Def16;
now__::_thesis:_not_{}_in_rng_A
assume {} in rng A ; ::_thesis: contradiction
then ex o being set st
( o in dom A & A . o = {} ) by FUNCT_1:def_3;
hence contradiction by A1, A11, PBOOLE:def_13; ::_thesis: verum
end;
then not product A is empty by CARD_3:26;
then consider a1 being set such that
A14: a1 in product A by XBOOLE_0:def_1;
consider p being set 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 set st o in dom A holds
a . o in A . o by A14, CARD_3:def_5;
reconsider a = 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 set such that
A20: t in r and
A21: t <> a . p by Th3;
reconsider p = p as Element of I by A15, PARTFUN1:def_2;
set b = a +* (p,t);
A22: now__::_thesis:_for_o_being_set_st_o_in_dom_A_holds_
(a_+*_(p,t))_._o_in_A_._o
let o be set ; ::_thesis: ( o in dom A implies (a +* (p,t)) . b1 in A . b1 )
assume A23: o in dom A ; ::_thesis: (a +* (p,t)) . b1 in A . b1
percases ( o <> p or o = p ) ;
suppose o <> p ; ::_thesis: (a +* (p,t)) . b1 in A . b1
then (a +* (p,t)) . o = a . o by FUNCT_7:32;
hence (a +* (p,t)) . o in A . o by A19, A23; ::_thesis: verum
end;
suppose o = p ; ::_thesis: (a +* (p,t)) . b1 in A . b1
hence (a +* (p,t)) . o in A . o by A18, A15, A16, A20, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
dom (a +* (p,t)) = I by PARTFUN1:def_2
.= dom A by PARTFUN1:def_2 ;
then A24: a +* (p,t) in product A by A22, CARD_3:9;
(a +* (p,t)) . p = t by A18, A15, FUNCT_7:31;
hence 2 c= card (product A) by A14, A17, A21, A24, Th2; ::_thesis: verum
end;
registration
let I be non empty set ;
let B be non trivial-yielding Segre-like ManySortedSet of I;
cluster product B -> non trivial ;
coherence
not product B is trivial
proof
consider f being set 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 set 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 = f as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18;
not B . (indx B) is trivial by Def21;
then 2 c= card (B . (indx B)) by Th4;
then consider y being set 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 set st x in dom B holds
(f +* ((indx B),y)) . x in B . x
proof
let x be set ; ::_thesis: ( x in dom B implies (f +* ((indx B),y)) . x in B . x )
assume A6: x in dom B ; ::_thesis: (f +* ((indx B),y)) . x in B . x
then x in I by PARTFUN1:def_2;
then A7: x in dom f by PARTFUN1:def_2;
percases ( x = indx B or x <> indx B ) ;
suppose x = indx B ; ::_thesis: (f +* ((indx B),y)) . x in B . x
hence (f +* ((indx B),y)) . x in B . x by A3, A7, FUNCT_7:31; ::_thesis: verum
end;
suppose x <> indx B ; ::_thesis: (f +* ((indx B),y)) . x in B . x
then (f +* ((indx B),y)) . x = f . x by FUNCT_7:32;
hence (f +* ((indx B),y)) . x in B . x by A2, A6; ::_thesis: verum
end;
end;
end;
dom f = I by PARTFUN1:def_2;
then A8: (f +* ((indx B),y)) . (indx B) = y by FUNCT_7:31;
dom (f +* ((indx B),y)) = I by PARTFUN1:def_2
.= dom B by PARTFUN1:def_2 ;
then f +* ((indx B),y) in product B by A5, CARD_3:def_5;
then 2 c= card (product B) by A1, A4, A8, Th2;
hence not product B is trivial by Th4; ::_thesis: verum
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: :: PENCIL_1:def 22
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
ex b1 being Subset-Family of (product (Carrier A)) st
for x being set holds
( x in b1 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) ) )
proof
defpred S1[ set ] 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 set holds
( x in S iff ( x in bool (product (Carrier A)) & S1[x] ) ) from XBOOLE_0:sch_1();
S c= bool (product (Carrier A))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in S or a in bool (product (Carrier A)) )
assume a in S ; ::_thesis: a in bool (product (Carrier A))
hence a in bool (product (Carrier A)) by A1; ::_thesis: verum
end;
then reconsider S = S as Subset-Family of (product (Carrier A)) ;
take S ; ::_thesis: for x being set holds
( x in S 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) ) )
let x be set ; ::_thesis: ( x in S 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) ) )
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; ::_thesis: ( 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) ) implies x in S )
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) ; ::_thesis: x in S
x c= product (Carrier A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in product (Carrier A) )
assume a in x ; ::_thesis: a in product (Carrier A)
then consider g being Function such that
A4: g = a and
A5: dom g = dom B and
A6: for y being set st y in dom B holds
g . y in B . y by A2, CARD_3:def_5;
A7: for y being set st y in dom (Carrier A) holds
g . y in (Carrier A) . y
proof
let y be set ; ::_thesis: ( y in dom (Carrier A) implies g . y in (Carrier A) . y )
assume y in dom (Carrier A) ; ::_thesis: g . y in (Carrier A) . y
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, PBOOLE:def_2;
hence g . y in (Carrier A) . y by A9; ::_thesis: verum
end;
dom g = I by A5, PARTFUN1:def_2
.= dom (Carrier A) by PARTFUN1:def_2 ;
hence a in product (Carrier A) by A4, A7, CARD_3:def_5; ::_thesis: verum
end;
hence x in S by A1, A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of (product (Carrier A)) st ( for x being set holds
( x in b1 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 set holds
( x in b2 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) ) ) ) holds
b1 = b2
proof
let S1, S2 be Subset-Family of (product (Carrier A)); ::_thesis: ( ( 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) ) ) ) & ( 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) ) ) ) implies S1 = S2 )
assume 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) ) ) ; ::_thesis: S1 = S2
for x being set holds
( x in S1 iff x in S2 )
proof
let x be set ; ::_thesis: ( x in S1 iff x in S2 )
( 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 ( x in S1 iff x in S2 ) by A11; ::_thesis: verum
end;
hence S1 = S2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def22 defines Segre_Blocks PENCIL_1:def_22_:_
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I
for b3 being Subset-Family of (product (Carrier A)) holds
( b3 = Segre_Blocks A iff for x being set holds
( x in b3 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) ) ) );
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 :: PENCIL_1:def 23
TopStruct(# (product (Carrier A)),(Segre_Blocks A) #);
correctness
coherence
TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) is non empty TopStruct ;
;
end;
:: deftheorem defines Segre_Product PENCIL_1:def_23_:_
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I holds Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #);
theorem Th14: :: PENCIL_1:14
for I being non empty set
for A being 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 ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I
for x being Point of (Segre_Product A) holds x is ManySortedSet of I
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for x being Point of (Segre_Product A) holds x is ManySortedSet of I
let x be Point of (Segre_Product A); ::_thesis: x is ManySortedSet of I
ex f being Function st
( x = f & dom f = dom (Carrier A) & ( for a being set st a in dom (Carrier A) holds
f . a in (Carrier A) . a ) ) by CARD_3:def_5;
hence x is ManySortedSet of I ; ::_thesis: verum
end;
theorem Th15: :: PENCIL_1:15
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I st not for i being Element of I holds A . i is void holds
not Segre_Product A is void
proof
let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st not for i being Element of I holds A . i is void holds
not Segre_Product A is void
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( not for i being Element of I holds A . i is void implies not Segre_Product A is void )
set B = the V2() trivial-yielding ManySortedSubset of Carrier A;
given i being Element of I such that A1: not A . i is void ; ::_thesis: not Segre_Product A is void
set l = the Block of (A . i);
A2: not the topology of (A . i) is empty by A1;
A3: the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i)) c= Carrier A
proof
let i1 be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i1 in I or ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 )
assume A4: i1 in I ; ::_thesis: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
then A5: i1 in dom the V2() trivial-yielding ManySortedSubset of Carrier A by PARTFUN1:def_2;
percases ( i = i1 or i1 <> i ) ;
supposeA6: i = i1 ; ::_thesis: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
then ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 = the Block of (A . i) by A5, FUNCT_7:31;
then A7: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . 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_13;
hence ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 by A6, A7; ::_thesis: verum
end;
supposeA8: i1 <> i ; ::_thesis: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1
A9: the V2() trivial-yielding ManySortedSubset of Carrier A c= Carrier A by PBOOLE:def_18;
( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 = the V2() trivial-yielding ManySortedSubset of Carrier A . i1 by A8, FUNCT_7:32;
hence ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . i1 c= (Carrier A) . i1 by A4, A9, PBOOLE:def_2; ::_thesis: verum
end;
end;
end;
for j being Element of I st i <> j holds
( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element
proof
let j be Element of I; ::_thesis: ( i <> j implies ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element )
assume i <> j ; ::_thesis: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element
then A10: ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j = the V2() trivial-yielding ManySortedSubset of Carrier A . j by FUNCT_7:32;
j in I ;
then A11: j in dom the V2() trivial-yielding ManySortedSubset of Carrier A by PARTFUN1:def_2;
then ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j in rng the V2() trivial-yielding ManySortedSubset of Carrier A by A10, FUNCT_1:def_3;
then ( not ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is empty & ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is trivial ) by A11, A10, Def16, FUNCT_1:def_9;
hence ( the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i))) . j is 1 -element ; ::_thesis: verum
end;
then reconsider C = the V2() trivial-yielding ManySortedSubset of Carrier A +* (i, the Block of (A . i)) as Segre-like ManySortedSubset of Carrier A by A3, Def20, PBOOLE:def_18;
dom the V2() trivial-yielding ManySortedSubset of Carrier A = 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 not Segre_Product A is void by Def4; ::_thesis: verum
end;
theorem Th16: :: PENCIL_1:16
for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) holds
not Segre_Product A is degenerated
proof
let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) holds
not Segre_Product A is degenerated
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) implies not Segre_Product A is degenerated )
assume A1: for i being Element of I holds
( not A . i is degenerated & not for i being Element of I holds A . i is void ) ; ::_thesis: not Segre_Product A is degenerated
then not Segre_Product A is void by Th15;
then reconsider SB = Segre_Blocks A as non empty set ;
now__::_thesis:_not_product_(Carrier_A)_in_SB
assume product (Carrier A) in SB ; ::_thesis: contradiction
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 V2() 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_13, PUA2MSS1:2;
then A . i is degenerated by Def5;
hence contradiction by A1; ::_thesis: verum
end;
then product (Carrier A) is not Element of SB ;
hence not Segre_Product A is degenerated by Def5; ::_thesis: verum
end;
theorem Th17: :: PENCIL_1:17
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 & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is with_non_trivial_blocks
proof
let I be non empty set ; ::_thesis: 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 & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is with_non_trivial_blocks
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds
( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) implies Segre_Product A is with_non_trivial_blocks )
assume A1: for i being Element of I holds
( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ; ::_thesis: Segre_Product A is with_non_trivial_blocks
for k being Block of (Segre_Product A) holds 2 c= card k
proof
let k be Block of (Segre_Product A); ::_thesis: 2 c= card k
not Segre_Product A is 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, Def6;
then A5: not B . i is 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 non trivial-yielding Segre-like ManySortedSet of I by A5, Def16;
not product BB is trivial ;
hence 2 c= card k by A2, Th4; ::_thesis: verum
end;
hence Segre_Product A is with_non_trivial_blocks by Def6; ::_thesis: verum
end;
theorem Th18: :: PENCIL_1:18
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 & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is identifying_close_blocks
proof
let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is identifying_close_blocks
let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) implies Segre_Product A is identifying_close_blocks )
assume A1: for i being Element of I holds
( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ; ::_thesis: Segre_Product A is identifying_close_blocks
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); ::_thesis: ( 2 c= card (k /\ l) implies k = l )
assume 2 c= card (k /\ l) ; ::_thesis: k = l
then consider a, b being set such that
A2: a in k /\ l and
A3: b in k /\ l and
A4: a <> b by Th2;
not Segre_Product A is 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 = 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 = 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; ::_thesis: ( j <> i implies B . j is 1 -element )
assume A12: j <> i ; ::_thesis: B . j is 1 -element
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, Def6;
then not B . i is 1 -element by Th4;
then i1 = i by A13;
hence B . j is 1 -element by A12, A13; ::_thesis: verum
end;
not Segre_Product A is 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 = 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 = a as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
consider x being set such that
A19: x in I and
A20: a . x <> b . x by A4, A18, A8, FUNCT_1:2;
reconsider x = 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 not B . x is 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; ::_thesis: ( j <> i implies C . i is 1 -element )
assume A27: j <> i ; ::_thesis: C . i is 1 -element
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, Def6;
then not C . j is 1 -element by Th4;
then j1 = j by A28;
hence C . i is 1 -element by A27, A28; ::_thesis: verum
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 not C . x is 1 -element by Th4;
then A31: x = j by A26;
for s being set st s in dom B holds
B . s c= C . s
proof
let s be set ; ::_thesis: ( s in dom B implies B . s c= C . s )
assume A32: s in dom B ; ::_thesis: B . s c= C . s
then reconsider t = s as Element of I by PARTFUN1:def_2;
percases ( t = x or s <> x ) ;
supposeA33: t = x ; ::_thesis: B . s c= C . s
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 B . s c= C . s by A34, Def7; ::_thesis: verum
end;
suppose s <> x ; ::_thesis: B . s c= C . s
then B . t is 1 -element by A11, A23;
then consider y being set 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 B . s c= C . s by A35, A36, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence k c= l by A5, A14, A29, CARD_3:27; :: according to XBOOLE_0:def_10 ::_thesis: l c= k
for s being set st s in dom C holds
C . s c= B . s
proof
let s be set ; ::_thesis: ( s in dom C implies C . s c= B . s )
assume A37: s in dom C ; ::_thesis: C . s c= B . s
then reconsider t = s as Element of I by PARTFUN1:def_2;
percases ( t = x or s <> x ) ;
supposeA38: t = x ; ::_thesis: C . s c= B . s
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 C . s c= B . s by A39, Def7; ::_thesis: verum
end;
suppose s <> x ; ::_thesis: C . s c= B . s
then C . t is 1 -element by A26, A31;
then consider y being set 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 C . s c= B . s by A40, A41, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence l c= k by A5, A14, A29, CARD_3:27; ::_thesis: verum
end;
hence Segre_Product A is identifying_close_blocks by Def7; ::_thesis: verum
end;
registration
let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
cluster Segre_Product A -> non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ;
coherence
( not Segre_Product A is void & not Segre_Product A is degenerated & Segre_Product A is with_non_trivial_blocks & Segre_Product A is identifying_close_blocks )
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 ) ) ;
( not A . the Element of I is void & ( for j being Element of I holds not A . j is degenerated ) ) ;
hence ( not Segre_Product A is void & not Segre_Product A is degenerated & Segre_Product A is with_non_trivial_blocks & Segre_Product A is identifying_close_blocks ) by A1, Th15, Th16, Th17, Th18; ::_thesis: verum
end;
end;
theorem :: PENCIL_1:19
for T being TopStruct
for S being Subset of T st S is trivial holds
( S is strong & S is closed_under_lines )
proof
let T be TopStruct ; ::_thesis: for S being Subset of T st S is trivial holds
( S is strong & S is closed_under_lines )
let S be Subset of T; ::_thesis: ( S is trivial implies ( S is strong & S is closed_under_lines ) )
assume A1: S is trivial ; ::_thesis: ( S is strong & S is closed_under_lines )
thus S is strong ::_thesis: S is closed_under_lines
proof
let x, y be Point of T; :: according to PENCIL_1:def_3 ::_thesis: ( x in S & y in S implies x,y are_collinear )
assume A2: ( x in S & y in S ) ; ::_thesis: x,y are_collinear
thus x,y are_collinear ::_thesis: verum
proof
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: x,y are_collinear
hence x,y are_collinear by Def1; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: x,y are_collinear
then 2 c= card S by A2, Th2;
hence x,y are_collinear by A1, Th4; ::_thesis: verum
end;
end;
end;
end;
thus S is closed_under_lines ::_thesis: verum
proof
let l be Block of T; :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (l /\ S) implies l c= S )
A3: card (l /\ S) c= card S by CARD_1:11, XBOOLE_1:17;
assume 2 c= card (l /\ S) ; ::_thesis: l c= S
then 2 c= card S by A3, XBOOLE_1:1;
hence l c= S by A1, Th4; ::_thesis: verum
end;
end;
theorem Th20: :: PENCIL_1:20
for S being identifying_close_blocks TopStruct
for l being Block of S
for L being Subset of S st L = l holds
L is closed_under_lines
proof
let S be identifying_close_blocks TopStruct ; ::_thesis: for l being Block of S
for L being Subset of S st L = l holds
L is closed_under_lines
let l be Block of S; ::_thesis: for L being Subset of S st L = l holds
L is closed_under_lines
let L be Subset of S; ::_thesis: ( L = l implies L is closed_under_lines )
assume A1: L = l ; ::_thesis: L is closed_under_lines
thus L is closed_under_lines ::_thesis: verum
proof
let K be Block of S; :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (K /\ L) implies K c= L )
assume 2 c= card (K /\ L) ; ::_thesis: K c= L
hence K c= L by A1, Def7; ::_thesis: verum
end;
end;
theorem Th21: :: PENCIL_1:21
for S being TopStruct
for l being Block of S
for L being Subset of S st L = l holds
L is strong
proof
let S be TopStruct ; ::_thesis: for l being Block of S
for L being Subset of S st L = l holds
L is strong
let l be Block of S; ::_thesis: for L being Subset of S st L = l holds
L is strong
let L be Subset of S; ::_thesis: ( L = l implies L is strong )
assume A1: L = l ; ::_thesis: L is strong
thus L is strong ::_thesis: verum
proof
let x, y be Point of S; :: according to PENCIL_1:def_3 ::_thesis: ( x in L & y in L implies x,y are_collinear )
assume ( x in L & y in L ) ; ::_thesis: x,y are_collinear
then {x,y} c= l by A1, ZFMISC_1:32;
hence x,y are_collinear by Def1; ::_thesis: verum
end;
end;
theorem :: PENCIL_1:22
for S being non void TopStruct holds [#] S is closed_under_lines
proof
let S be non void TopStruct ; ::_thesis: [#] S is closed_under_lines
thus [#] S is closed_under_lines ::_thesis: verum
proof
let K be Block of S; :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (K /\ ([#] S)) implies K c= [#] S )
assume 2 c= card (K /\ ([#] S)) ; ::_thesis: K c= [#] S
K in the topology of S ;
hence K c= [#] S ; ::_thesis: verum
end;
end;
theorem Th23: :: PENCIL_1:23
for I being non empty set
for A being non trivial-yielding Segre-like ManySortedSet of I
for x, y being ManySortedSet of I st x in product A & y in product A holds
for i being set st i <> indx A holds
x . i = y . i
proof
let I be non empty set ; ::_thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for x, y being ManySortedSet of I st x in product A & y in product A holds
for i being set st i <> indx A holds
x . i = y . i
let A be non trivial-yielding Segre-like ManySortedSet of I; ::_thesis: for x, y being ManySortedSet of I st x in product A & y in product A holds
for i being set st i <> indx A holds
x . i = y . i
let x, y be ManySortedSet of I; ::_thesis: ( x in product A & y in product A implies for i being set st i <> indx A holds
x . i = y . i )
assume that
A1: x in product A and
A2: y in product A ; ::_thesis: for i being set st i <> indx A holds
x . i = y . i
let i be set ; ::_thesis: ( i <> indx A implies x . i = y . i )
A3: dom A = I by PARTFUN1:def_2;
assume A4: i <> indx A ; ::_thesis: x . i = y . i
percases ( not i in I or i in I ) ;
supposeA5: not i in I ; ::_thesis: x . i = y . 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 ;
::_thesis: verum
end;
suppose i in I ; ::_thesis: x . i = y . 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__::_thesis:_not_j_<>_indx_A
assume j <> indx A ; ::_thesis: contradiction
then A . (indx A) is 1 -element by A7;
hence contradiction by Def21; ::_thesis: verum
end;
then A . ii is 1 -element by A4, A7;
then consider o being set 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 ;
::_thesis: verum
end;
end;
end;
theorem Th24: :: PENCIL_1:24
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 non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for x being set holds
( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: for x being set holds
( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
let x be set ; ::_thesis: ( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) )
thus ( x is Block of (Segre_Product A) implies ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) ) ::_thesis: ( ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) implies x is Block of (Segre_Product A) )
proof
assume A1: x is Block of (Segre_Product A) ; ::_thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) )
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 = L as non trivial-yielding Segre-like 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__::_thesis:_not_i_<>_indx_L
assume i <> indx L ; ::_thesis: contradiction
then A5: L . i is 1 -element by Th12;
2 c= card (L . i) by A4, Def6;
hence contradiction by A5, Th4; ::_thesis: verum
end;
hence ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( x = product L & L . (indx L) is Block of (A . (indx L)) ) by A2, A4; ::_thesis: verum
end;
given L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A6: ( x = product L & L . (indx L) is Block of (A . (indx L)) ) ; ::_thesis: x is Block of (Segre_Product A)
thus x is Block of (Segre_Product A) by A6, Def22; ::_thesis: verum
end;
theorem Th25: :: PENCIL_1:25
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) holds
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 ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for P being ManySortedSet of I st P is Point of (Segre_Product A) holds
for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)
let A be PLS-yielding ManySortedSet of I; ::_thesis: for P being ManySortedSet of I st P is Point of (Segre_Product A) holds
for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)
let P be ManySortedSet of I; ::_thesis: ( P is Point of (Segre_Product A) implies for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A) )
assume A1: P is Point of (Segre_Product A) ; ::_thesis: for i being Element of I
for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)
let j be Element of I; ::_thesis: for p being Point of (A . j) holds P +* (j,p) is Point of (Segre_Product A)
let p be Point of (A . j); ::_thesis: P +* (j,p) is Point of (Segre_Product A)
A2: for i being set st i in dom (Carrier A) holds
(P +* (j,p)) . i in (Carrier A) . i
proof
let i be set ; ::_thesis: ( i in dom (Carrier A) implies (P +* (j,p)) . i in (Carrier A) . i )
assume A3: i in dom (Carrier A) ; ::_thesis: (P +* (j,p)) . i in (Carrier A) . i
then i in I by PARTFUN1:def_2;
then A4: i in dom P by PARTFUN1:def_2;
percases ( i <> j or i = j ) ;
suppose i <> j ; ::_thesis: (P +* (j,p)) . i in (Carrier A) . i
then (P +* (j,p)) . i = P . i by FUNCT_7:32;
hence (P +* (j,p)) . i in (Carrier A) . i by A1, A3, CARD_3:9; ::_thesis: verum
end;
supposeA5: i = j ; ::_thesis: (P +* (j,p)) . i in (Carrier A) . i
A6: p in the carrier of (A . j) ;
(P +* (j,p)) . i = p by A4, A5, FUNCT_7:31;
hence (P +* (j,p)) . i in (Carrier A) . i by A5, A6, YELLOW_6:2; ::_thesis: verum
end;
end;
end;
dom (P +* (j,p)) = I by PARTFUN1:def_2
.= dom (Carrier A) by PARTFUN1:def_2 ;
hence P +* (j,p) is Point of (Segre_Product A) by A2, CARD_3:9; ::_thesis: verum
end;
theorem Th26: :: PENCIL_1:26
for I being non empty set
for A, B being non trivial-yielding Segre-like ManySortedSet of I st 2 c= card ((product A) /\ (product B)) holds
( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) )
proof
let I be non empty set ; ::_thesis: for A, B being non trivial-yielding Segre-like ManySortedSet of I st 2 c= card ((product A) /\ (product B)) holds
( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) )
let A, B be non trivial-yielding Segre-like ManySortedSet of I; ::_thesis: ( 2 c= card ((product A) /\ (product B)) implies ( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) ) )
A1: dom B = I by PARTFUN1:def_2;
assume 2 c= card ((product A) /\ (product B)) ; ::_thesis: ( indx A = indx B & ( for i being set st i <> indx A holds
A . i = B . i ) )
then consider a, b being set 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 set 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 set st o in dom A holds
a1 . o in A . o by CARD_3:def_5;
consider o being set such that
A11: o in dom A and
A12: a1 . o <> b1 . o by A4, A8, A9, A5, A6, FUNCT_1:2;
reconsider o = 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: not B . o is 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 not A . o is trivial by Th4;
then A18: o = indx A by Def21;
hence indx A = indx B by A15, Def21; ::_thesis: for i being set st i <> indx A holds
A . i = B . i
let i be set ; ::_thesis: ( i <> indx A implies A . i = B . i )
assume A19: i <> indx A ; ::_thesis: A . i = B . i
percases ( i in I or not i in I ) ;
supposeA20: i in I ; ::_thesis: A . i = B . i
then B . i is 1 -element by A18, A16, A19, Th12;
then A21: ex y being set st B . i = {y} by ZFMISC_1:131;
A . i is 1 -element by A19, A20, Th12;
then consider x being set 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 A . i = B . i by A22, A21, A23, TARSKI:def_1; ::_thesis: verum
end;
supposeA24: not i in I ; ::_thesis: A . i = B . 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 ;
::_thesis: verum
end;
end;
end;
theorem Th27: :: PENCIL_1:27
for I being non empty set
for A being non trivial-yielding Segre-like ManySortedSet of I
for N being non trivial set holds
( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
proof
let I be non empty set ; ::_thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for N being non trivial set holds
( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
let A be non trivial-yielding Segre-like ManySortedSet of I; ::_thesis: for N being non trivial set holds
( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
let N be non trivial set ; ::_thesis: ( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )
thus A +* ((indx A),N) is Segre-like ::_thesis: not A +* ((indx A),N) is trivial-yielding
proof
take indx A ; :: according to PENCIL_1:def_20 ::_thesis: for j being Element of I st indx A <> j holds
(A +* ((indx A),N)) . j is 1 -element
let i be Element of I; ::_thesis: ( indx A <> i implies (A +* ((indx A),N)) . i is 1 -element )
assume A1: i <> indx A ; ::_thesis: (A +* ((indx A),N)) . i is 1 -element
then (A +* ((indx A),N)) . i = A . i by FUNCT_7:32;
hence (A +* ((indx A),N)) . i is 1 -element by A1, Th12; ::_thesis: verum
end;
thus not A +* ((indx A),N) is trivial-yielding ::_thesis: verum
proof
take (A +* ((indx A),N)) . (indx A) ; :: according to PENCIL_1:def_16 ::_thesis: ( (A +* ((indx A),N)) . (indx A) in rng (A +* ((indx A),N)) & not (A +* ((indx A),N)) . (indx A) is trivial )
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; ::_thesis: not (A +* ((indx A),N)) . (indx A) is trivial
I = dom A by PARTFUN1:def_2;
hence not (A +* ((indx A),N)) . (indx A) is trivial by FUNCT_7:31; ::_thesis: verum
end;
end;
theorem :: PENCIL_1:28
for S being non empty non void identifying_close_blocks without_isolated_points TopStruct st S is strongly_connected holds
S is connected
proof
let S be non empty non void identifying_close_blocks without_isolated_points TopStruct ; ::_thesis: ( S is strongly_connected implies S is connected )
assume A1: S is strongly_connected ; ::_thesis: S is connected
thus S is connected ::_thesis: verum
proof
let x, y be Point of S; :: according to PENCIL_1:def_10 ::_thesis: 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 holds
for a, b being Point of S st a = f . i & b = f . (i + 1) holds
a,b are_collinear ) )
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 & L is 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 & W is strong ) and
A8: for i being Nat st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) by A1, Def11;
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 H1( Nat) -> set = (f . $1) /\ (f . ($1 + 1));
reconsider n = 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 = H1(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__::_thesis:_not_{}_in_rng_h
assume {} in rng h ; ::_thesis: contradiction
then consider i being set such that
A14: i in dom h and
A15: h . i = {} by FUNCT_1:def_3;
reconsider i = 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; ::_thesis: verum
end;
then product h <> {} by CARD_3:26;
then consider c being set 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 set st a in dom h holds
ce . a in h . a ) ) by A19, CARD_3:def_5;
then reconsider c = c as Function ;
A21: dom h = Seg n by A11, FINSEQ_1:def_3;
then reconsider c = 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not r in rng ((<*x*> ^ c) ^ <*y*>) or r in the carrier of S )
assume r in rng ((<*x*> ^ c) ^ <*y*>) ; ::_thesis: r in the carrier of S
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;
percases ( r in rng <*x*> or r in rng c or r in rng <*y*> ) by A23, XBOOLE_0:def_3;
suppose r in rng <*x*> ; ::_thesis: r in the carrier of S
then r in {x} by FINSEQ_1:38;
hence r in the carrier of S ; ::_thesis: verum
end;
suppose r in rng c ; ::_thesis: r in the carrier of S
then consider o being set such that
A24: o in dom c and
A25: r = c . o by FUNCT_1:def_3;
reconsider o = 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 r in the carrier of S by A22, A26; ::_thesis: verum
end;
suppose r in rng <*y*> ; ::_thesis: r in the carrier of S
then r in {y} by FINSEQ_1:38;
hence r in the carrier of S ; ::_thesis: verum
end;
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 ; ::_thesis: ( x = g . 1 & y = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear ) )
A29: g = <*x*> ^ (c ^ <*y*>) by FINSEQ_1:32;
hence x = g . 1 by FINSEQ_1:41; ::_thesis: ( y = g . (len g) & ( for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear ) )
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; ::_thesis: for i being Nat st 1 <= i & i < len g holds
for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear
let i be Nat; ::_thesis: ( 1 <= i & i < len g implies for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear )
assume that
A32: 1 <= i and
A33: i < len g ; ::_thesis: for a, b being Point of S st a = g . i & b = g . (i + 1) holds
a,b are_collinear
A34: i <= len (<*x*> ^ c) by A30, A33, NAT_1:13;
let a, b be Point of S; ::_thesis: ( a = g . i & b = g . (i + 1) implies a,b are_collinear )
assume that
A35: a = g . i and
A36: b = g . (i + 1) ; ::_thesis: a,b are_collinear
reconsider i = i as Element of NAT by ORDINAL1:def_12;
percases ( ( i = 1 & i <= len c ) or ( i = 1 & i = (len c) + 1 ) or ( 1 < i & i <= len c ) or ( 1 < i & i = (len c) + 1 ) ) by A28, A32, A34, NAT_1:8, XXREAL_0:1;
supposeA37: ( i = 1 & i <= len c ) ; ::_thesis: a,b are_collinear
( 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 & f1 is strong ) by A7, A42;
a = x by A29, A35, A37, FINSEQ_1:41;
hence a,b are_collinear by A4, A5, A41, A43, Def3; ::_thesis: verum
end;
supposeA44: ( i = 1 & i = (len c) + 1 ) ; ::_thesis: a,b are_collinear
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 & f1 is 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, Def3;
hence a,b are_collinear by A29, A31, A35, A36, A44, A47, FINSEQ_1:41; ::_thesis: verum
end;
supposeA48: ( 1 < i & i <= len c ) ; ::_thesis: a,b are_collinear
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 & ff is strong ) by A7, A54;
hence a,b are_collinear by A61, A59, Def3; ::_thesis: verum
end;
supposeA62: ( 1 < i & i = (len c) + 1 ) ; ::_thesis: a,b are_collinear
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 & ff is 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 a,b are_collinear by A6, A67, A68, Def3; ::_thesis: verum
end;
end;
end;
end;
theorem :: PENCIL_1:29
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for S being Subset of (Segre_Product A) holds
( ( not S is trivial & S is strong & S is closed_under_lines ) iff 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 ) ) ) )
proof
let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I
for S being Subset of (Segre_Product A) holds
( ( not S is trivial & S is strong & S is closed_under_lines ) iff 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 ) ) ) )
let A be PLS-yielding ManySortedSet of I; ::_thesis: for S being Subset of (Segre_Product A) holds
( ( not S is trivial & S is strong & S is closed_under_lines ) iff 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 ) ) ) )
let S be Subset of (Segre_Product A); ::_thesis: ( ( not S is trivial & S is strong & S is closed_under_lines ) iff 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 ) ) ) )
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: ( 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 ) ) ) implies ( not S is trivial & S is strong & S is closed_under_lines ) )
proof
assume A1: ( not S is trivial & S is strong & S is closed_under_lines ) ; ::_thesis: 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 ) ) )
then 2 c= card S by Th4;
then consider a, b being set 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, Def3;
then consider C being Block of (Segre_Product A) such that
A5: {a,b} c= C by A4, Def1;
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:_not_a1_._(indx_CC)_=_b1_._(indx_CC)
assume A11: a1 . (indx CC) = b1 . (indx CC) ; ::_thesis: contradiction
for i being set st i in I holds
a1 . i = b1 . i
proof
let i be set ; ::_thesis: ( i in I implies a1 . i = b1 . i )
assume i in I ; ::_thesis: a1 . i = b1 . i
percases ( i = indx CC or i <> indx CC ) ;
suppose i = indx CC ; ::_thesis: a1 . i = b1 . i
hence a1 . i = b1 . i by A11; ::_thesis: verum
end;
supposeA12: i <> indx CC ; ::_thesis: a1 . i = b1 . i
( a1 in product CC & b1 in product CC ) by A5, A6, ZFMISC_1:32;
hence a1 . i = b1 . i by A12, Th23; ::_thesis: verum
end;
end;
end;
hence contradiction by A4, A8, A9, FUNCT_1:2; ::_thesis: verum
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: ( f in S implies for i being Element of I st i <> indx CC holds
f . i in CC . i )
assume A14: f in S ; ::_thesis: for i being Element of I st i <> indx CC holds
f . i in CC . i
then reconsider f1 = f as Point of (Segre_Product A) ;
let i be Element of I; ::_thesis: ( i <> indx CC implies f . i in CC . i )
assume A15: i <> indx CC ; ::_thesis: f . i in CC . i
now__::_thesis:_f_._i_in_CC_._i
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: contradiction
f1,b are_collinear by A1, A3, A14, Def3;
then consider lb being Block of (Segre_Product A) such that
A18: {f1,b} c= lb by A17, A16, Def1;
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 set 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, Def3;
then consider la being Block of (Segre_Product A) such that
A26: {f1,a} c= la by A17, A25, Def1;
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 set 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: verum
end;
hence f . i in CC . i ; ::_thesis: verum
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 set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (CC +* ((indx CC),p)) . i c= (Carrier A) . i )
assume A34: i in I ; ::_thesis: (CC +* ((indx CC),p)) . i c= (Carrier A) . i
percases ( i <> indx CC or i = indx CC ) ;
supposeA35: i <> indx CC ; ::_thesis: (CC +* ((indx CC),p)) . i c= (Carrier A) . i
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, PBOOLE:def_2; ::_thesis: verum
end;
supposeA37: i = indx CC ; ::_thesis: (CC +* ((indx CC),p)) . i c= (Carrier A) . i
A38: p c= (Carrier A) . i
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in p or y in (Carrier A) . i )
assume y in p ; ::_thesis: y in (Carrier A) . i
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: verum
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: verum
end;
end;
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: ( 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 ) ) )
A40: dom B = I by PARTFUN1:def_2;
A41: B . (indx CC) = p by A7, FUNCT_7:31;
thus A42: S = product B ::_thesis: for C being Subset of (A . (indx B)) st C = B . (indx B) holds
( C is strong & C is closed_under_lines )
proof
thus S c= product B :: according to XBOOLE_0:def_10 ::_thesis: product B c= S
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in S or e in product B )
assume A43: e in S ; ::_thesis: e in product B
then reconsider f = e as ManySortedSet of I by Th14;
A44: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
f_._i_in_B_._i
let i be set ; ::_thesis: ( i in I implies f . b1 in B . b1 )
assume i in I ; ::_thesis: f . b1 in B . b1
then reconsider j = i as Element of I ;
percases ( j = indx CC or j <> indx CC ) ;
suppose j = indx CC ; ::_thesis: f . b1 in B . b1
hence f . i in B . i by A41, A43, CARD_3:def_6; ::_thesis: verum
end;
supposeA45: j <> indx CC ; ::_thesis: f . b1 in B . b1
then f . j in CC . j by A13, A43;
hence f . i in B . i by A45, FUNCT_7:32; ::_thesis: verum
end;
end;
end;
dom f = I by PARTFUN1:def_2;
hence e in product B by A40, A44, CARD_3:9; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in product B or e in S )
assume e in product B ; ::_thesis: e in S
then consider f being Function such that
A46: ( e = f & dom f = I ) and
A47: for i being set 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:_for_i_being_set_st_i_in_I_holds_
f_._i_=_g_._i
let i be set ; ::_thesis: ( i in I implies f . b1 = g . b1 )
assume i in I ; ::_thesis: f . b1 = g . b1
then reconsider j = i as Element of I ;
percases ( i = indx CC or i <> indx CC ) ;
suppose i = indx CC ; ::_thesis: f . b1 = g . b1
hence f . i = g . i by A49; ::_thesis: verum
end;
supposeA51: i <> indx CC ; ::_thesis: f . b1 = g . b1
then CC . j is 1 -element by Th12;
then consider c being set 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: verum
end;
end;
end;
dom g = I by PARTFUN1:def_2;
hence e in S by A46, A48, A50, FUNCT_1:2; ::_thesis: verum
end;
let SS be Subset of (A . (indx B)); ::_thesis: ( SS = B . (indx B) implies ( SS is strong & SS is closed_under_lines ) )
assume A54: SS = B . (indx B) ; ::_thesis: ( SS is strong & SS is closed_under_lines )
thus SS is strong ::_thesis: SS is closed_under_lines
proof
let q, r be Point of (A . (indx B)); :: according to PENCIL_1:def_3 ::_thesis: ( q in SS & r in SS implies q,r are_collinear )
assume that
A55: q in SS and
A56: r in SS ; ::_thesis: q,r are_collinear
thus q,r are_collinear ::_thesis: verum
proof
percases ( q = r or q <> r ) ;
suppose q = r ; ::_thesis: q,r are_collinear
hence q,r are_collinear by Def1; ::_thesis: verum
end;
supposeA57: q <> r ; ::_thesis: q,r are_collinear
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:_not_Q_=_R
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: contradiction
hence contradiction by A57, A59, A60, FUNCT_7:31; ::_thesis: verum
end;
A61: for i being set st i in dom B holds
Q1 . i in B . i
proof
let i be set ; ::_thesis: ( i in dom B implies Q1 . i in B . i )
assume A62: i in dom B ; ::_thesis: Q1 . i in B . i
then i in I by PARTFUN1:def_2;
then A63: i in dom a1 by PARTFUN1:def_2;
percases ( i <> indx B or i = indx B ) ;
suppose i <> indx B ; ::_thesis: Q1 . i in B . i
then Q1 . i = a1 . i by FUNCT_7:32;
hence Q1 . i in B . i by A2, A42, A62, CARD_3:9; ::_thesis: verum
end;
suppose i = indx B ; ::_thesis: Q1 . i in B . i
hence Q1 . i in B . i by A54, A55, A63, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
A64: for i being set st i in dom B holds
R1 . i in B . i
proof
let i be set ; ::_thesis: ( i in dom B implies R1 . i in B . i )
assume A65: i in dom B ; ::_thesis: R1 . i in B . i
then i in I by PARTFUN1:def_2;
then A66: i in dom a1 by PARTFUN1:def_2;
percases ( i <> indx B or i = indx B ) ;
suppose i <> indx B ; ::_thesis: R1 . i in B . i
then R1 . i = a1 . i by FUNCT_7:32;
hence R1 . i in B . i by A2, A42, A65, CARD_3:9; ::_thesis: verum
end;
suppose i = indx B ; ::_thesis: R1 . i in B . i
hence R1 . i in B . i by A54, A56, A66, FUNCT_7:31; ::_thesis: verum
end;
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, Def3;
then consider L being Block of (Segre_Product A) such that
A68: {Q,R} c= L by A58, Def1;
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:_not_Q1_._(indx_B)_=_R1_._(indx_B)
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: contradiction
hence contradiction by A57, A76, A77, FUNCT_7:31; ::_thesis: verum
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 by Def1; ::_thesis: verum
end;
end;
end;
end;
thus SS is closed_under_lines ::_thesis: verum
proof
let L be Block of (A . (indx B)); :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (L /\ SS) implies L c= SS )
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 set ; :: according to PBOOLE:def_2 ::_thesis: ( not o in I or (B +* ((indx B),L1)) . o c= (Carrier A) . o )
assume A82: o in I ; ::_thesis: (B +* ((indx B),L1)) . o c= (Carrier A) . o
thus (B +* ((indx B),L1)) . o c= (Carrier A) . o ::_thesis: verum
proof
percases ( o <> indx B or o = indx B ) ;
supposeA83: o <> indx B ; ::_thesis: (B +* ((indx B),L1)) . o c= (Carrier A) . o
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, PBOOLE:def_2; ::_thesis: verum
end;
supposeA85: o = indx B ; ::_thesis: (B +* ((indx B),L1)) . o c= (Carrier A) . o
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: verum
end;
end;
end;
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: L c= SS
then consider x, y being set 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:_for_o_being_set_st_o_in_I_holds_
(a1_+*_((indx_B),y))_._o_in_B_._o
let o be set ; ::_thesis: ( o in I implies (a1 +* ((indx B),y)) . b1 in B . b1 )
assume A91: o in I ; ::_thesis: (a1 +* ((indx B),y)) . b1 in B . b1
percases ( o <> indx B or o = indx B ) ;
suppose o <> indx B ; ::_thesis: (a1 +* ((indx B),y)) . b1 in B . b1
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: verum
end;
supposeA92: o = indx B ; ::_thesis: (a1 +* ((indx B),y)) . b1 in B . b1
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: verum
end;
end;
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:_for_o_being_set_st_o_in_dom_L2_holds_
(a1_+*_((indx_B),y))_._o_in_L2_._o
let o be set ; ::_thesis: ( o in dom L2 implies (a1 +* ((indx B),y)) . b1 in L2 . b1 )
assume A95: o in dom L2 ; ::_thesis: (a1 +* ((indx B),y)) . b1 in L2 . b1
percases ( o <> indx B or o = indx B ) ;
supposeA96: o <> indx B ; ::_thesis: (a1 +* ((indx B),y)) . b1 in L2 . b1
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: verum
end;
supposeA98: o = indx B ; ::_thesis: (a1 +* ((indx B),y)) . b1 in L2 . b1
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: verum
end;
end;
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:_for_o_being_set_st_o_in_I_holds_
(a1_+*_((indx_B),x))_._o_in_B_._o
let o be set ; ::_thesis: ( o in I implies (a1 +* ((indx B),x)) . b1 in B . b1 )
assume A101: o in I ; ::_thesis: (a1 +* ((indx B),x)) . b1 in B . b1
percases ( o <> indx B or o = indx B ) ;
suppose o <> indx B ; ::_thesis: (a1 +* ((indx B),x)) . b1 in B . b1
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: verum
end;
supposeA102: o = indx B ; ::_thesis: (a1 +* ((indx B),x)) . b1 in B . b1
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: verum
end;
end;
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:_for_o_being_set_st_o_in_dom_L2_holds_
(a1_+*_((indx_B),x))_._o_in_L2_._o
let o be set ; ::_thesis: ( o in dom L2 implies (a1 +* ((indx B),x)) . b1 in L2 . b1 )
assume A105: o in dom L2 ; ::_thesis: (a1 +* ((indx B),x)) . b1 in L2 . b1
percases ( o <> indx B or o = indx B ) ;
supposeA106: o <> indx B ; ::_thesis: (a1 +* ((indx B),x)) . b1 in L2 . b1
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: verum
end;
supposeA108: o = indx B ; ::_thesis: (a1 +* ((indx B),x)) . b1 in L2 . b1
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: verum
end;
end;
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, Def2;
thus L c= SS ::_thesis: verum
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in L or e in SS )
consider f being set 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 set 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: e in SS
A113: now__::_thesis:_for_o_being_set_st_o_in_dom_L2_holds_
(f_+*_((indx_B),e))_._o_in_L2_._o
let o be set ; ::_thesis: ( o in dom L2 implies (f +* ((indx B),e)) . b1 in L2 . b1 )
assume A114: o in dom L2 ; ::_thesis: (f +* ((indx B),e)) . b1 in L2 . b1
percases ( o <> indx B or o = indx B ) ;
suppose o <> indx B ; ::_thesis: (f +* ((indx B),e)) . b1 in L2 . b1
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: verum
end;
supposeA115: o = indx B ; ::_thesis: (f +* ((indx B),e)) . b1 in L2 . b1
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: verum
end;
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 e in SS by A54, A111, FUNCT_7:31; ::_thesis: verum
end;
end;
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: ( not S is trivial & S is strong & S is closed_under_lines )
thus not S is trivial by A116; ::_thesis: ( S is strong & S is closed_under_lines )
A118: dom B = I by PARTFUN1:def_2;
A119: dom (Carrier A) = I by PARTFUN1:def_2;
thus S is strong ::_thesis: S is closed_under_lines
proof
let x, y be Point of (Segre_Product A); :: according to PENCIL_1:def_3 ::_thesis: ( x in S & y in S implies x,y are_collinear )
assume that
A120: x in S and
A121: y in S ; ::_thesis: x,y are_collinear
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: x,y are_collinear
hence x,y are_collinear by Def1; ::_thesis: verum
end;
supposeA122: x <> y ; ::_thesis: x,y are_collinear
consider y1 being Function such that
A123: y1 = y and
A124: dom y1 = dom (Carrier A) and
A125: for a being set 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 set 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:_not_x1_._(indx_B)_=_y1_._(indx_B)
assume A131: x1 . (indx B) = y1 . (indx B) ; ::_thesis: contradiction
now__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_
x1_._i_=_y1_._i
let i be set ; ::_thesis: ( i in dom (Carrier A) implies x1 . b1 = y1 . b1 )
assume i in dom (Carrier A) ; ::_thesis: x1 . b1 = y1 . b1
percases ( i <> indx B or i = indx B ) ;
suppose i <> indx B ; ::_thesis: x1 . b1 = y1 . b1
hence x1 . i = y1 . i by A116, A120, A121, A127, A123, Th23; ::_thesis: verum
end;
suppose i = indx B ; ::_thesis: x1 . b1 = y1 . b1
hence x1 . i = y1 . i by A131; ::_thesis: verum
end;
end;
end;
hence contradiction by A122, A127, A128, A123, A124, FUNCT_1:2; ::_thesis: verum
end;
B c= Carrier A by PBOOLE:def_18;
then B . (indx B) c= (Carrier A) . (indx B) by PBOOLE:def_2;
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, Def3;
then consider l being Block of (A . (indx B)) such that
A134: {x1i,y1i} c= l by A130, Def1;
A135: dom {x1} = I by PARTFUN1:def_2;
A136: for a being set st a in dom ({x1} +* ((indx B),l)) holds
y1 . a in ({x1} +* ((indx B),l)) . a
proof
let a be set ; ::_thesis: ( a in dom ({x1} +* ((indx B),l)) implies y1 . a in ({x1} +* ((indx B),l)) . a )
assume a in dom ({x1} +* ((indx B),l)) ; ::_thesis: y1 . a in ({x1} +* ((indx B),l)) . a
then A137: a in I by PARTFUN1:def_2;
percases ( a = indx B or a <> indx B ) ;
supposeA138: a = indx B ; ::_thesis: y1 . a in ({x1} +* ((indx B),l)) . a
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: verum
end;
supposeA139: a <> indx B ; ::_thesis: y1 . a in ({x1} +* ((indx B),l)) . a
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: verum
end;
end;
end;
{x1} +* ((indx B),l) c= Carrier A
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ({x1} +* ((indx B),l)) . i c= (Carrier A) . i )
assume A140: i in I ; ::_thesis: ({x1} +* ((indx B),l)) . i c= (Carrier A) . i
then reconsider i1 = i as Element of I ;
thus ({x1} +* ((indx B),l)) . i c= (Carrier A) . i ::_thesis: verum
proof
percases ( i = indx B or i <> indx B ) ;
supposeA141: i = indx B ; ::_thesis: ({x1} +* ((indx B),l)) . i c= (Carrier A) . i
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: verum
end;
supposeA142: i <> indx B ; ::_thesis: ({x1} +* ((indx B),l)) . i c= (Carrier A) . i
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: verum
end;
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; ::_thesis: ( i <> indx B implies ({x1} +* ((indx B),l)) . i is 1 -element )
assume i <> indx B ; ::_thesis: ({x1} +* ((indx B),l)) . i is 1 -element
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: verum
end;
then A145: {x1} +* ((indx B),l) is Segre-like by Def20;
A146: for a being set st a in dom ({x1} +* ((indx B),l)) holds
x1 . a in ({x1} +* ((indx B),l)) . a
proof
let a be set ; ::_thesis: ( a in dom ({x1} +* ((indx B),l)) implies x1 . a in ({x1} +* ((indx B),l)) . a )
assume a in dom ({x1} +* ((indx B),l)) ; ::_thesis: x1 . a in ({x1} +* ((indx B),l)) . a
then A147: a in I by PARTFUN1:def_2;
percases ( a = indx B or a <> indx B ) ;
supposeA148: a = indx B ; ::_thesis: x1 . a in ({x1} +* ((indx B),l)) . a
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: verum
end;
supposeA149: a <> indx B ; ::_thesis: x1 . a in ({x1} +* ((indx B),l)) . a
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: verum
end;
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 x,y are_collinear by Def1; ::_thesis: verum
end;
end;
end;
thus S is closed_under_lines ::_thesis: verum
proof
let l be Block of (Segre_Product A); :: according to PENCIL_1:def_2 ::_thesis: ( 2 c= card (l /\ S) implies l c= S )
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: l c= S
then consider a, b being set 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, XBOOLE_1:1;
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 set st a in dom L holds
L . a c= B . a
proof
let a be set ; ::_thesis: ( a in dom L implies L . a c= B . a )
assume a in dom L ; ::_thesis: L . a c= B . a
percases ( a <> indx B or a = indx B ) ;
suppose a <> indx B ; ::_thesis: L . a c= B . a
hence L . a c= B . a by A116, A153, A151, Th26; ::_thesis: verum
end;
supposeA159: a = indx B ; ::_thesis: L . a c= B . a
B c= Carrier A by PBOOLE:def_18;
then B . (indx B) c= (Carrier A) . (indx B) by PBOOLE:def_2;
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:_not_a1_._(indx_B)_=_b1_._(indx_B)
assume A168: a1 . (indx B) = b1 . (indx B) ; ::_thesis: contradiction
A169: for o being set st o in dom a1 holds
a1 . o = b1 . o
proof
let o be set ; ::_thesis: ( o in dom a1 implies a1 . o = b1 . o )
assume o in dom a1 ; ::_thesis: a1 . o = b1 . o
percases ( o <> indx B or o = indx B ) ;
suppose o <> indx B ; ::_thesis: a1 . o = b1 . o
hence a1 . o = b1 . o by A166, A164, Th23; ::_thesis: verum
end;
suppose o = indx B ; ::_thesis: a1 . o = b1 . o
hence a1 . o = b1 . o by A168; ::_thesis: verum
end;
end;
end;
dom a1 = I by PARTFUN1:def_2
.= dom b1 by PARTFUN1:def_2 ;
hence contradiction by A156, A169, FUNCT_1:2; ::_thesis: verum
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, Def2; ::_thesis: verum
end;
end;
end;
hence l c= S by A116, A151, A157, CARD_3:27; ::_thesis: verum
end;
end;