:: PENCIL_3 semantic presentation begin theorem Th1: :: PENCIL_3:1 for S being non empty non void TopStruct for f being Collineation of S for p, q being Point of S st p,q are_collinear holds f . p,f . q are_collinear proof let S be non empty non void TopStruct ; ::_thesis: for f being Collineation of S for p, q being Point of S st p,q are_collinear holds f . p,f . q are_collinear let f be Collineation of S; ::_thesis: for p, q being Point of S st p,q are_collinear holds f . p,f . q are_collinear A1: dom f = the carrier of S by FUNCT_2:def_1; let p, q be Point of S; ::_thesis: ( p,q are_collinear implies f . p,f . q are_collinear ) assume A2: p,q are_collinear ; ::_thesis: f . p,f . q are_collinear percases ( p = q or p <> q ) ; suppose p = q ; ::_thesis: f . p,f . q are_collinear hence f . p,f . q are_collinear by PENCIL_1:def_1; ::_thesis: verum end; suppose p <> q ; ::_thesis: f . p,f . q are_collinear then consider B being Block of S such that A3: {p,q} c= B by A2, PENCIL_1:def_1; q in B by A3, ZFMISC_1:32; then A4: f . q in f .: B by A1, FUNCT_1:def_6; p in B by A3, ZFMISC_1:32; then f . p in f .: B by A1, FUNCT_1:def_6; then {(f . p),(f . q)} c= f .: B by A4, ZFMISC_1:32; hence f . p,f . q are_collinear by PENCIL_1:def_1; ::_thesis: verum end; end; end; theorem Th2: :: PENCIL_3:2 for I being non empty set for i being Element of I for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial proof let I be non empty set ; ::_thesis: for i being Element of I for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial let i be Element of I; ::_thesis: for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: not A . i is trivial dom A = I by PARTFUN1:def_2; then A . i in rng A by FUNCT_1:3; hence not A . i is trivial by PENCIL_1:def_17; ::_thesis: verum end; theorem Th3: :: PENCIL_3:3 for S being non void identifying_close_blocks TopStruct st S is strongly_connected holds S is without_isolated_points proof let S be non void identifying_close_blocks TopStruct ; ::_thesis: ( S is strongly_connected implies S is without_isolated_points ) assume A1: S is strongly_connected ; ::_thesis: S is without_isolated_points now__::_thesis:_for_x_being_Point_of_S_ex_l_being_Block_of_S_st_x_in_l consider X being set such that A2: X in the topology of S by XBOOLE_0:def_1; reconsider X = X as Block of S by A2; reconsider X1 = X as Subset of S by A2; let x be Point of S; ::_thesis: ex l being Block of S st l in b2 ( X1 is closed_under_lines & X1 is strong ) by PENCIL_1:20, PENCIL_1:21; then consider f being FinSequence of bool the carrier of S such that A3: X = f . 1 and A4: x in f . (len f) and A5: for W being Subset of S st W in rng f holds ( W is closed_under_lines & W is strong ) and A6: for i being Nat st 1 <= i & i < len f holds 2 c= card ((f . i) /\ (f . (i + 1))) by A1, PENCIL_1:def_11; A7: len f in dom f by A4, FUNCT_1:def_2; then reconsider l = (len f) - 1 as Nat by FINSEQ_3:26; A8: f . (len f) in rng f by A7, FUNCT_1:3; then reconsider W = f . (len f) as Subset of S ; A9: ( W is closed_under_lines & W is strong ) by A5, A8; percases ( x in X or not x in X ) ; suppose x in X ; ::_thesis: ex l being Block of S st l in b2 hence ex l being Block of S st x in l ; ::_thesis: verum end; supposeA10: not x in X ; ::_thesis: ex l being Block of S st l in b2 1 <= len f by A7, FINSEQ_3:25; then 1 < ((len f) - 1) + 1 by A3, A4, A10, XXREAL_0:1; then ( 1 <= l & l < len f ) by NAT_1:13; then 2 c= card ((f . l) /\ (f . (l + 1))) by A6; then consider a being set such that A11: a in (f . l) /\ (f . (len f)) and A12: a <> x by PENCIL_1:3; A13: a in W by A11, XBOOLE_0:def_4; then reconsider a = a as Point of S ; x,a are_collinear by A4, A9, A13, PENCIL_1:def_3; then consider l being Block of S such that A14: {x,a} c= l by A12, PENCIL_1:def_1; x in l by A14, ZFMISC_1:32; hence ex l being Block of S st x in l ; ::_thesis: verum end; end; end; hence S is without_isolated_points by PENCIL_1:def_9; ::_thesis: verum end; theorem Th4: :: PENCIL_3:4 for S being non empty non void identifying_close_blocks TopStruct st S is strongly_connected holds S is connected proof let S be non empty non void identifying_close_blocks TopStruct ; ::_thesis: ( S is strongly_connected implies S is connected ) assume A1: S is strongly_connected ; ::_thesis: S is connected then S is without_isolated_points by Th3; hence S is connected by A1, PENCIL_1:28; ::_thesis: verum end; theorem :: PENCIL_3:5 for S being non void non degenerated TopStruct for L being Block of S holds not for x being Point of S holds x in L proof let S be non void non degenerated TopStruct ; ::_thesis: for L being Block of S holds not for x being Point of S holds x in L let L be Block of S; ::_thesis: not for x being Point of S holds x in L A1: L in the topology of S ; now__::_thesis:_not_[#]_S_c=_L assume [#] S c= L ; ::_thesis: contradiction then [#] S = L by A1, XBOOLE_0:def_10; hence contradiction by PENCIL_1:def_5; ::_thesis: verum end; then consider x being set such that A2: x in [#] S and A3: not x in L by TARSKI:def_3; reconsider x = x as Point of S by A2; take x ; ::_thesis: not x in L thus not x in L by A3; ::_thesis: verum end; theorem Th6: :: PENCIL_3:6 for I being non empty set for A being non-Empty TopStruct-yielding ManySortedSet of I for p being Point of (Segre_Product A) holds p is Element of Carrier A proof let I be non empty set ; ::_thesis: for A being non-Empty TopStruct-yielding ManySortedSet of I for p being Point of (Segre_Product A) holds p is Element of Carrier A let A be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for p being Point of (Segre_Product A) holds p is Element of Carrier A let p be Point of (Segre_Product A); ::_thesis: p is Element of Carrier A Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23; then consider f being Function such that A1: f = p and A2: dom f = dom (Carrier A) and A3: for x being set st x in dom (Carrier A) holds f . x in (Carrier A) . x by CARD_3:def_5; A4: dom f = I by A2, PARTFUN1:def_2; then reconsider f = f as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; for i being set st i in I holds f . i is Element of (Carrier A) . i by A2, A3, A4; hence p is Element of Carrier A by A1, PBOOLE:def_14; ::_thesis: verum end; theorem Th7: :: PENCIL_3:7 for I being non empty set for A being 1-sorted-yielding ManySortedSet of I for x being Element of I holds (Carrier A) . x = [#] (A . x) proof let I be non empty set ; ::_thesis: for A being 1-sorted-yielding ManySortedSet of I for x being Element of I holds (Carrier A) . x = [#] (A . x) let A be 1-sorted-yielding ManySortedSet of I; ::_thesis: for x being Element of I holds (Carrier A) . x = [#] (A . x) let x be Element of I; ::_thesis: (Carrier A) . x = [#] (A . x) ex R being 1-sorted st ( R = A . x & (Carrier A) . x = the carrier of R ) by PRALG_1:def_13; hence (Carrier A) . x = [#] (A . x) ; ::_thesis: verum end; theorem Th8: :: PENCIL_3:8 for I being non empty set for i being Element of I for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = i & product L is Segre-Coset of A ) proof let I be non empty set ; ::_thesis: for i being Element of I for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = i & product L is Segre-Coset of A ) let x be Element of I; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = x & product L is Segre-Coset of A ) let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = x & product L is Segre-Coset of A ) set p0 = the Point of (Segre_Product A); dom A = I by PARTFUN1:def_2; then A . x in rng A by FUNCT_1:3; then not A . x is trivial by PENCIL_1:def_18; then reconsider C = [#] (A . x) as non trivial set ; reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6; reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11; reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7; take b ; ::_thesis: ( indx b = x & product b is Segre-Coset of A ) dom p = I by PARTFUN1:def_2; then A1: b . x = C by FUNCT_7:31; hence A2: indx b = x by PENCIL_1:def_21; ::_thesis: product b is Segre-Coset of A product b c= the carrier of (Segre_Product A) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product b or a in the carrier of (Segre_Product A) ) assume a in product b ; ::_thesis: a in the carrier of (Segre_Product A) then consider f being Function such that A3: a = f and A4: dom f = dom b and A5: for x being set st x in dom b holds f . x in b . x by CARD_3:def_5; dom (Carrier A) = I by PARTFUN1:def_2; then A6: dom f = dom (Carrier A) by A4, PARTFUN1:def_2; A7: now__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_ f_._i_in_(Carrier_A)_._i let i be set ; ::_thesis: ( i in dom (Carrier A) implies f . b1 in (Carrier A) . b1 ) assume A8: i in dom (Carrier A) ; ::_thesis: f . b1 in (Carrier A) . b1 then reconsider i1 = i as Element of I ; A9: f . i in b . i by A4, A5, A6, A8; percases ( i1 = x or i1 <> x ) ; suppose i1 = x ; ::_thesis: f . b1 in (Carrier A) . b1 hence f . i in (Carrier A) . i by A1, A9, Th7; ::_thesis: verum end; supposeA10: i1 <> x ; ::_thesis: f . b1 in (Carrier A) . b1 I = dom A by PARTFUN1:def_2; then A . i1 in rng A by FUNCT_1:3; then not A . i1 is trivial by PENCIL_1:def_18; then reconsider AA = the carrier of (A . i1) as non trivial set ; f . i1 in p . i1 by A9, A10, FUNCT_7:32; then f . i1 in {(p0 . i1)} by PZFMISC1:def_1; then f . i1 = p0 . i1 by TARSKI:def_1; then A11: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def_14; not AA is empty ; then not [#] (A . i1) is empty ; then not (Carrier A) . i1 is empty by Th7; hence f . i in (Carrier A) . i by A11; ::_thesis: verum end; end; end; Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23; hence a in the carrier of (Segre_Product A) by A3, A6, A7, CARD_3:def_5; ::_thesis: verum end; hence product b is Segre-Coset of A by A1, A2, PENCIL_2:def_2; ::_thesis: verum end; theorem Th9: :: PENCIL_3:9 for I being non empty set for i being Element of I for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = i & product L is Segre-Coset of A & p in product L ) proof let I be non empty set ; ::_thesis: for i being Element of I for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = i & product L is Segre-Coset of A & p in product L ) let x be Element of I; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = x & product L is Segre-Coset of A & p in product L ) let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = x & product L is Segre-Coset of A & p in product L ) let p0 be Point of (Segre_Product A); ::_thesis: ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st ( indx L = x & product L is Segre-Coset of A & p0 in product L ) dom A = I by PARTFUN1:def_2; then A . x in rng A by FUNCT_1:3; then not A . x is trivial by PENCIL_1:def_18; then reconsider C = [#] (A . x) as non trivial set ; reconsider p09 = p0 as Element of Carrier A by Th6; reconsider p = {p09} as ManySortedSubset of Carrier A by PENCIL_1:11; reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7; take b ; ::_thesis: ( indx b = x & product b is Segre-Coset of A & p0 in product b ) dom p = I by PARTFUN1:def_2; then A1: b . x = C by FUNCT_7:31; hence A2: indx b = x by PENCIL_1:def_21; ::_thesis: ( product b is Segre-Coset of A & p0 in product b ) product b c= the carrier of (Segre_Product A) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product b or a in the carrier of (Segre_Product A) ) assume a in product b ; ::_thesis: a in the carrier of (Segre_Product A) then consider f being Function such that A3: a = f and A4: dom f = dom b and A5: for x being set st x in dom b holds f . x in b . x by CARD_3:def_5; dom (Carrier A) = I by PARTFUN1:def_2; then A6: dom f = dom (Carrier A) by A4, PARTFUN1:def_2; A7: now__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_ f_._i_in_(Carrier_A)_._i let i be set ; ::_thesis: ( i in dom (Carrier A) implies f . b1 in (Carrier A) . b1 ) assume A8: i in dom (Carrier A) ; ::_thesis: f . b1 in (Carrier A) . b1 then reconsider i1 = i as Element of I ; A9: f . i in b . i by A4, A5, A6, A8; percases ( i1 = x or i1 <> x ) ; suppose i1 = x ; ::_thesis: f . b1 in (Carrier A) . b1 hence f . i in (Carrier A) . i by A1, A9, Th7; ::_thesis: verum end; supposeA10: i1 <> x ; ::_thesis: f . b1 in (Carrier A) . b1 I = dom A by PARTFUN1:def_2; then A . i1 in rng A by FUNCT_1:3; then not A . i1 is trivial by PENCIL_1:def_18; then reconsider AA = the carrier of (A . i1) as non trivial set ; f . i1 in p . i1 by A9, A10, FUNCT_7:32; then f . i1 in {(p09 . i1)} by PZFMISC1:def_1; then f . i1 = p09 . i1 by TARSKI:def_1; then A11: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def_14; not AA is empty ; then not [#] (A . i1) is empty ; then not (Carrier A) . i1 is empty by Th7; hence f . i in (Carrier A) . i by A11; ::_thesis: verum end; end; end; Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23; hence a in the carrier of (Segre_Product A) by A3, A6, A7, CARD_3:def_5; ::_thesis: verum end; hence product b is Segre-Coset of A by A1, A2, PENCIL_2:def_2; ::_thesis: p0 in product b A12: dom p = I by PARTFUN1:def_2; A13: now__::_thesis:_for_z_being_set_st_z_in_I_holds_ p09_._z_in_(p_+*_(x,C))_._z let z be set ; ::_thesis: ( z in I implies p09 . b1 in (p +* (x,C)) . b1 ) assume A14: z in I ; ::_thesis: p09 . b1 in (p +* (x,C)) . b1 then reconsider z1 = z as Element of I ; dom A = I by PARTFUN1:def_2; then A . z in rng A by A14, FUNCT_1:def_3; then A . z is non trivial 1-sorted by PENCIL_1:def_18; then reconsider tc = the carrier of (A . z1) as non trivial set ; A15: not tc is empty ; percases ( z = x or z <> x ) ; supposeA16: z = x ; ::_thesis: p09 . b1 in (p +* (x,C)) . b1 p09 . z1 is Element of (Carrier A) . z1 by PBOOLE:def_14; then p09 . z1 is Element of [#] (A . z1) by Th7; then p09 . z1 in the carrier of (A . z1) by A15; hence p09 . z in (p +* (x,C)) . z by A12, A16, FUNCT_7:31; ::_thesis: verum end; suppose z <> x ; ::_thesis: p09 . b1 in (p +* (x,C)) . b1 then (p +* (x,C)) . z = p . z by FUNCT_7:32; then (p +* (x,C)) . z = {(p09 . z)} by A14, PZFMISC1:def_1; hence p09 . z in (p +* (x,C)) . z by TARSKI:def_1; ::_thesis: verum end; end; end; ( dom p09 = I & dom (p +* (x,C)) = I ) by PARTFUN1:def_2; hence p0 in product b by A13, CARD_3:9; ::_thesis: verum end; theorem Th10: :: PENCIL_3:10 for I being non empty set for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A holds b . (indx b) = [#] (A . (indx b)) proof let I be non empty set ; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A holds b . (indx b) = [#] (A . (indx b)) let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A holds b . (indx b) = [#] (A . (indx b)) let b be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b is Segre-Coset of A implies b . (indx b) = [#] (A . (indx b)) ) assume product b is Segre-Coset of A ; ::_thesis: b . (indx b) = [#] (A . (indx b)) then consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A1: product b = product L and A2: L . (indx L) = [#] (A . (indx L)) by PENCIL_2:def_2; b = L by A1, PUA2MSS1:2; hence b . (indx b) = [#] (A . (indx b)) by A2; ::_thesis: verum end; theorem Th11: :: PENCIL_3:11 for I being non empty set for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for L1, L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 holds L1 = L2 proof let I be non empty set ; ::_thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I for L1, L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 holds L1 = L2 let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; ::_thesis: for L1, L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 holds L1 = L2 let L1, L2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 implies L1 = L2 ) assume that A1: ( product L1 is Segre-Coset of A & product L2 is Segre-Coset of A ) and A2: indx L1 = indx L2 and A3: product L1 meets product L2 ; ::_thesis: L1 = L2 reconsider B1 = product L1, B2 = product L2 as Segre-Coset of A by A1; B1 /\ B2 <> {} by A3, XBOOLE_0:def_7; then consider x being set such that A4: x in B1 /\ B2 by XBOOLE_0:def_1; A5: x in B2 by A4, XBOOLE_0:def_4; A6: x in B1 by A4, XBOOLE_0:def_4; reconsider x = x as Element of Carrier A by A4, Th6; consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A7: B1 = product b1 and A8: b1 . (indx b1) = [#] (A . (indx b1)) by PENCIL_2:def_2; consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A9: B2 = product b2 and A10: b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def_2; A11: b2 = L2 by A9, PUA2MSS1:2; A12: dom L1 = I by PARTFUN1:def_2 .= dom L2 by PARTFUN1:def_2 ; A13: b1 = L1 by A7, PUA2MSS1:2; now__::_thesis:_for_a_being_set_st_a_in_dom_L1_holds_ L1_._a_=_L2_._a let a be set ; ::_thesis: ( a in dom L1 implies L1 . b1 = L2 . b1 ) assume A14: a in dom L1 ; ::_thesis: L1 . b1 = L2 . b1 then reconsider i = a as Element of I ; percases ( i = indx L1 or i <> indx L1 ) ; suppose i = indx L1 ; ::_thesis: L1 . b1 = L2 . b1 hence L1 . a = L2 . a by A2, A8, A10, A13, A11; ::_thesis: verum end; supposeA15: i <> indx L1 ; ::_thesis: L1 . b1 = L2 . b1 then ( not L1 . i is empty & L1 . i is trivial ) by PENCIL_1:def_21; then L1 . i is 1 -element ; then consider o1 being set such that A16: L1 . i = {o1} by ZFMISC_1:131; ( not L2 . i is empty & L2 . i is trivial ) by A2, A15, PENCIL_1:def_21; then L2 . i is 1 -element ; then consider o2 being set such that A17: L2 . i = {o2} by ZFMISC_1:131; A18: x . i in L2 . i by A5, A12, A14, CARD_3:9; x . i in L1 . i by A6, A14, CARD_3:9; then o1 = x . i by A16, TARSKI:def_1 .= o2 by A17, A18, TARSKI:def_1 ; hence L1 . a = L2 . a by A16, A17; ::_thesis: verum end; end; end; hence L1 = L2 by A12, FUNCT_1:2; ::_thesis: verum end; theorem Th12: :: PENCIL_3:12 for I being non empty set for A being PLS-yielding ManySortedSet of I for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of (Segre_Product A) proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of (Segre_Product A) let A be PLS-yielding ManySortedSet of I; ::_thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of (Segre_Product A) let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of (Segre_Product A) let B be Block of (A . (indx L)); ::_thesis: product (L +* ((indx L),B)) is Block of (Segre_Product A) B in the topology of (A . (indx L)) ; then reconsider B1 = B as Subset of (A . (indx L)) ; A1: now__::_thesis:_for_i_being_Element_of_I_st_i_<>_indx_L_holds_ (L_+*_((indx_L),B1))_._i_is_1_-element let i be Element of I; ::_thesis: ( i <> indx L implies (L +* ((indx L),B1)) . i is 1 -element ) assume A2: i <> indx L ; ::_thesis: (L +* ((indx L),B1)) . i is 1 -element then (L +* ((indx L),B1)) . i = L . i by FUNCT_7:32; hence (L +* ((indx L),B1)) . i is 1 -element by A2, PENCIL_1:12; ::_thesis: verum end; 2 c= card B by PENCIL_1:def_6; then not B1 is trivial by PENCIL_1:4; then reconsider S = L +* ((indx L),B1) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A1, PENCIL_1:9, PENCIL_1:def_20, PENCIL_2:7; A3: now__::_thesis:_not_indx_S_<>_indx_L assume indx S <> indx L ; ::_thesis: contradiction then S . (indx S) is 1 -element by A1; hence contradiction by PENCIL_1:def_21; ::_thesis: verum end; dom L = I by PARTFUN1:def_2; then S . (indx S) = B1 by A3, FUNCT_7:31; hence product (L +* ((indx L),B)) is Block of (Segre_Product A) by A3, PENCIL_1:24; ::_thesis: verum end; theorem Th13: :: PENCIL_3:13 for I being non empty set for A being PLS-yielding ManySortedSet of I for i being Element of I for p being Point of (A . i) for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I for i being Element of I for p being Point of (A . i) for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A let A be PLS-yielding ManySortedSet of I; ::_thesis: for i being Element of I for p being Point of (A . i) for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A let i be Element of I; ::_thesis: for p being Point of (A . i) for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A let p be Point of (A . i); ::_thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( i <> indx L implies L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A ) A1: now__::_thesis:_for_j_being_Element_of_I_st_j_<>_indx_L_holds_ (L_+*_(i,{p}))_._j_is_1_-element let j be Element of I; ::_thesis: ( j <> indx L implies (L +* (i,{p})) . b1 is 1 -element ) A2: dom L = I by PARTFUN1:def_2; assume A3: j <> indx L ; ::_thesis: (L +* (i,{p})) . b1 is 1 -element percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: (L +* (i,{p})) . b1 is 1 -element hence (L +* (i,{p})) . j is 1 -element by A2, FUNCT_7:31; ::_thesis: verum end; suppose j <> i ; ::_thesis: (L +* (i,{p})) . b1 is 1 -element then (L +* (i,{p})) . j = L . j by FUNCT_7:32; hence (L +* (i,{p})) . j is 1 -element by A3, PENCIL_1:12; ::_thesis: verum end; end; end; A4: L +* (i,{p}) c= Carrier A proof let a be set ; :: according to PBOOLE:def_2 ::_thesis: ( not a in I or (L +* (i,{p})) . a c= (Carrier A) . a ) assume A5: a in I ; ::_thesis: (L +* (i,{p})) . a c= (Carrier A) . a then reconsider a1 = a as Element of I ; A6: a1 in dom L by A5, PARTFUN1:def_2; percases ( a = i or a <> i ) ; supposeA7: a = i ; ::_thesis: (L +* (i,{p})) . a c= (Carrier A) . a then (L +* (i,{p})) . a1 = {p} by A6, FUNCT_7:31; then (L +* (i,{p})) . a1 c= [#] (A . a1) by A7; hence (L +* (i,{p})) . a c= (Carrier A) . a by Th7; ::_thesis: verum end; supposeA8: a <> i ; ::_thesis: (L +* (i,{p})) . a c= (Carrier A) . a A9: L c= Carrier A by PBOOLE:def_18; (L +* (i,{p})) . a1 = L . a1 by A8, FUNCT_7:32; hence (L +* (i,{p})) . a c= (Carrier A) . a by A9, PBOOLE:def_2; ::_thesis: verum end; end; end; assume i <> indx L ; ::_thesis: L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A then (L +* (i,{p})) . (indx L) = L . (indx L) by FUNCT_7:32; then A10: not (L +* (i,{p})) . (indx L) is trivial by PENCIL_1:def_21; dom (L +* (i,{p})) = I by PARTFUN1:def_2; then (L +* (i,{p})) . (indx L) in rng (L +* (i,{p})) by FUNCT_1:3; hence L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A by A4, A1, A10, PBOOLE:def_18, PENCIL_1:def_16, PENCIL_1:def_20; ::_thesis: verum end; theorem Th14: :: PENCIL_3:14 for I being non empty set for A being PLS-yielding ManySortedSet of I for i being Element of I for S being Subset of (A . i) for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A) proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I for i being Element of I for S being Subset of (A . i) for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A) let A be PLS-yielding ManySortedSet of I; ::_thesis: for i being Element of I for S being Subset of (A . i) for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A) let i be Element of I; ::_thesis: for S being Subset of (A . i) for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A) let S be Subset of (A . i); ::_thesis: for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A holds product (L +* (i,S)) is Subset of (Segre_Product A) let L be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: product (L +* (i,S)) is Subset of (Segre_Product A) A1: dom (L +* (i,S)) = I by PARTFUN1:def_2 .= dom (Carrier A) by PARTFUN1:def_2 ; A2: now__::_thesis:_for_a_being_set_st_a_in_dom_(L_+*_(i,S))_holds_ (L_+*_(i,S))_._a_c=_(Carrier_A)_._a let a be set ; ::_thesis: ( a in dom (L +* (i,S)) implies (L +* (i,S)) . b1 c= (Carrier A) . b1 ) assume a in dom (L +* (i,S)) ; ::_thesis: (L +* (i,S)) . b1 c= (Carrier A) . b1 then A3: a in I ; then A4: a in dom L by PARTFUN1:def_2; percases ( a = i or a <> i ) ; supposeA5: a = i ; ::_thesis: (L +* (i,S)) . b1 c= (Carrier A) . b1 then (L +* (i,S)) . a = S by A4, FUNCT_7:31; then (L +* (i,S)) . a c= [#] (A . i) ; hence (L +* (i,S)) . a c= (Carrier A) . a by A5, Th7; ::_thesis: verum end; supposeA6: a <> i ; ::_thesis: (L +* (i,S)) . b1 c= (Carrier A) . b1 A7: L c= Carrier A by PBOOLE:def_18; (L +* (i,S)) . a = L . a by A6, FUNCT_7:32; hence (L +* (i,S)) . a c= (Carrier A) . a by A3, A7, PBOOLE:def_2; ::_thesis: verum end; end; end; Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23; hence product (L +* (i,S)) is Subset of (Segre_Product A) by A1, A2, CARD_3:27; ::_thesis: verum end; theorem Th15: :: PENCIL_3:15 for I being non empty set for P being ManySortedSet of I for i being Element of I holds {P} . i is 1 -element proof let I be non empty set ; ::_thesis: for P being ManySortedSet of I for i being Element of I holds {P} . i is 1 -element let P be ManySortedSet of I; ::_thesis: for i being Element of I holds {P} . i is 1 -element let i be Element of I; ::_thesis: {P} . i is 1 -element {P} . i = {(P . i)} by PZFMISC1:def_1; hence {P} . i is 1 -element ; ::_thesis: verum end; theorem Th16: :: PENCIL_3:16 for I being non empty set for i being Element of I for A being PLS-yielding ManySortedSet of I for B being Block of (A . i) for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of (Segre_Product A) proof let I be non empty set ; ::_thesis: for i being Element of I for A being PLS-yielding ManySortedSet of I for B being Block of (A . i) for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of (Segre_Product A) let i be Element of I; ::_thesis: for A being PLS-yielding ManySortedSet of I for B being Block of (A . i) for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of (Segre_Product A) let A be PLS-yielding ManySortedSet of I; ::_thesis: for B being Block of (A . i) for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of (Segre_Product A) let B be Block of (A . i); ::_thesis: for P being Element of Carrier A holds product ({P} +* (i,B)) is Block of (Segre_Product A) let P be Element of Carrier A; ::_thesis: product ({P} +* (i,B)) is Block of (Segre_Product A) reconsider PP = {P} as ManySortedSubset of Carrier A by PENCIL_1:11; B in the topology of (A . i) ; then reconsider B1 = B as Subset of (A . i) ; A1: now__::_thesis:_for_j_being_Element_of_I_st_j_<>_i_holds_ ({P}_+*_(i,B1))_._j_is_1_-element let j be Element of I; ::_thesis: ( j <> i implies ({P} +* (i,B1)) . j is 1 -element ) assume j <> i ; ::_thesis: ({P} +* (i,B1)) . j is 1 -element then ({P} +* (i,B1)) . j = {P} . j by FUNCT_7:32; hence ({P} +* (i,B1)) . j is 1 -element by Th15; ::_thesis: verum end; 2 c= card B by PENCIL_1:def_6; then not B1 is trivial by PENCIL_1:4; then reconsider S = PP +* (i,B1) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A1, PENCIL_1:9, PENCIL_1:def_20, PENCIL_2:7; A2: now__::_thesis:_not_indx_S_<>_i assume indx S <> i ; ::_thesis: contradiction then S . (indx S) is 1 -element by A1; hence contradiction by PENCIL_1:def_21; ::_thesis: verum end; dom {P} = I by PARTFUN1:def_2; then S . (indx S) = B1 by A2, FUNCT_7:31; hence product ({P} +* (i,B)) is Block of (Segre_Product A) by A2, PENCIL_1:24; ::_thesis: verum end; theorem Th17: :: PENCIL_3:17 for I being non empty set for A being PLS-yielding ManySortedSet of I for p, q being Point of (Segre_Product A) st p <> q holds ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ) proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I for p, q being Point of (Segre_Product A) st p <> q holds ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ) let A be PLS-yielding ManySortedSet of I; ::_thesis: for p, q being Point of (Segre_Product A) st p <> q holds ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ) let p, q be Point of (Segre_Product A); ::_thesis: ( p <> q implies ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ) ) assume A1: p <> q ; ::_thesis: ( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ) thus ( p,q are_collinear implies for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ) ::_thesis: ( ( for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ) implies p,q are_collinear ) proof assume p,q are_collinear ; ::_thesis: for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) then consider l being Block of (Segre_Product A) such that A2: {p,q} c= l by A1, PENCIL_1:def_1; let p1, q1 be ManySortedSet of I; ::_thesis: ( p1 = p & q1 = q implies ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ) assume that A3: p1 = p and A4: q1 = q ; ::_thesis: ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) A5: q1 in l by A2, A4, ZFMISC_1:32; consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A6: l = product L and A7: L . (indx L) is Block of (A . (indx L)) by PENCIL_1:24; take i = indx L; ::_thesis: ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) A8: p1 in l by A2, A3, ZFMISC_1:32; thus for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ::_thesis: for j being Element of I st j <> i holds p1 . j = q1 . j proof reconsider LI = L . (indx L) as Block of (A . (indx L)) by A7; let a, b be Point of (A . i); ::_thesis: ( a = p1 . i & b = q1 . i implies ( a <> b & a,b are_collinear ) ) A9: ex p0 being Function st ( p0 = p1 & dom p0 = dom L & ( for o being set st o in dom L holds p0 . o in L . o ) ) by A6, A8, CARD_3:def_5; A10: ex q0 being Function st ( q0 = q1 & dom q0 = dom L & ( for o being set st o in dom L holds q0 . o in L . o ) ) by A6, A5, CARD_3:def_5; assume A11: ( a = p1 . i & b = q1 . i ) ; ::_thesis: ( a <> b & a,b are_collinear ) now__::_thesis:_not_a_=_b assume A12: a = b ; ::_thesis: contradiction A13: now__::_thesis:_for_o_being_set_st_o_in_dom_p1_holds_ p1_._o_=_q1_._o let o be set ; ::_thesis: ( o in dom p1 implies p1 . b1 = q1 . b1 ) assume A14: o in dom p1 ; ::_thesis: p1 . b1 = q1 . b1 then reconsider o1 = o as Element of I ; percases ( o1 = i or o1 <> i ) ; suppose o1 = i ; ::_thesis: p1 . b1 = q1 . b1 hence p1 . o = q1 . o by A11, A12; ::_thesis: verum end; suppose o1 <> i ; ::_thesis: p1 . b1 = q1 . b1 then L . o1 is 1 -element by PENCIL_1:12; then consider s being set such that A15: L . o1 = {s} by ZFMISC_1:131; p1 . o in {s} by A9, A14, A15; then A16: p1 . o = s by TARSKI:def_1; q1 . o in {s} by A9, A10, A14, A15; hence p1 . o = q1 . o by A16, TARSKI:def_1; ::_thesis: verum end; end; end; dom p1 = I by PARTFUN1:def_2 .= dom q1 by PARTFUN1:def_2 ; hence contradiction by A1, A3, A4, A13, FUNCT_1:2; ::_thesis: verum end; hence a <> b ; ::_thesis: a,b are_collinear A17: dom L = I by PARTFUN1:def_2; then A18: q1 . i in LI by A10; p1 . i in LI by A9, A17; then {a,b} c= LI by A11, A18, ZFMISC_1:32; hence a,b are_collinear by PENCIL_1:def_1; ::_thesis: verum end; let j be Element of I; ::_thesis: ( j <> i implies p1 . j = q1 . j ) assume j <> i ; ::_thesis: p1 . j = q1 . j hence p1 . j = q1 . j by A6, A8, A5, PENCIL_1:23; ::_thesis: verum end; reconsider p1 = p, q1 = q as Element of Carrier A by Th6; assume for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds ex i being Element of I st ( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds p1 . j = q1 . j ) ) ; ::_thesis: p,q are_collinear then consider i being Element of I such that A19: for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds ( a <> b & a,b are_collinear ) and A20: for j being Element of I st j <> i holds p1 . j = q1 . j ; q1 . i is Element of (Carrier A) . i by PBOOLE:def_14; then q1 . i is Element of [#] (A . i) by Th7; then reconsider b = q1 . i as Point of (A . i) ; p1 . i is Element of (Carrier A) . i by PBOOLE:def_14; then p1 . i is Element of [#] (A . i) by Th7; then reconsider a = p1 . i as Point of (A . i) ; A21: a,b are_collinear by A19; percases ( a = b or ex l being Block of (A . i) st {a,b} c= l ) by A21, PENCIL_1:def_1; suppose a = b ; ::_thesis: p,q are_collinear hence p,q are_collinear by A19; ::_thesis: verum end; suppose ex l being Block of (A . i) st {a,b} c= l ; ::_thesis: p,q are_collinear then consider l being Block of (A . i) such that A22: {a,b} c= l ; reconsider L = product ({p1} +* (i,l)) as Block of (Segre_Product A) by Th16; A23: dom ({p1} +* (i,l)) = I by PARTFUN1:def_2; then A24: dom {p1} = dom ({p1} +* (i,l)) by PARTFUN1:def_2; A25: for o being set st o in dom ({p1} +* (i,l)) holds q1 . o in ({p1} +* (i,l)) . o proof let o be set ; ::_thesis: ( o in dom ({p1} +* (i,l)) implies q1 . o in ({p1} +* (i,l)) . o ) assume A26: o in dom ({p1} +* (i,l)) ; ::_thesis: q1 . o in ({p1} +* (i,l)) . o then reconsider o1 = o as Element of I ; percases ( o1 = i or o1 <> i ) ; supposeA27: o1 = i ; ::_thesis: q1 . o in ({p1} +* (i,l)) . o then ({p1} +* (i,l)) . o = l by A24, A26, FUNCT_7:31; hence q1 . o in ({p1} +* (i,l)) . o by A22, A27, ZFMISC_1:32; ::_thesis: verum end; supposeA28: o1 <> i ; ::_thesis: q1 . o in ({p1} +* (i,l)) . o then ({p1} +* (i,l)) . o = {p1} . o by FUNCT_7:32; then ({p1} +* (i,l)) . o = {(p1 . o)} by A26, PZFMISC1:def_1; then ({p1} +* (i,l)) . o = {(q1 . o1)} by A20, A28; hence q1 . o in ({p1} +* (i,l)) . o by TARSKI:def_1; ::_thesis: verum end; end; end; A29: for o being set st o in dom ({p1} +* (i,l)) holds p1 . o in ({p1} +* (i,l)) . o proof let o be set ; ::_thesis: ( o in dom ({p1} +* (i,l)) implies p1 . o in ({p1} +* (i,l)) . o ) assume A30: o in dom ({p1} +* (i,l)) ; ::_thesis: p1 . o in ({p1} +* (i,l)) . o percases ( o = i or o <> i ) ; supposeA31: o = i ; ::_thesis: p1 . o in ({p1} +* (i,l)) . o then ({p1} +* (i,l)) . o = l by A24, A30, FUNCT_7:31; hence p1 . o in ({p1} +* (i,l)) . o by A22, A31, ZFMISC_1:32; ::_thesis: verum end; suppose o <> i ; ::_thesis: p1 . o in ({p1} +* (i,l)) . o then ({p1} +* (i,l)) . o = {p1} . o by FUNCT_7:32; then ({p1} +* (i,l)) . o = {(p1 . o)} by A30, PZFMISC1:def_1; hence p1 . o in ({p1} +* (i,l)) . o by TARSKI:def_1; ::_thesis: verum end; end; end; dom q1 = dom ({p1} +* (i,l)) by A23, PARTFUN1:def_2; then A32: q in L by A25, CARD_3:def_5; dom p1 = dom ({p1} +* (i,l)) by A23, PARTFUN1:def_2; then p in L by A29, CARD_3:def_5; then {p,q} c= L by A32, ZFMISC_1:32; hence p,q are_collinear by PENCIL_1:def_1; ::_thesis: verum end; end; end; theorem Th18: :: PENCIL_3:18 for I being non empty set for A being PLS-yielding ManySortedSet of I for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A for x being Point of (A . (indx b)) ex p being ManySortedSet of I st ( p in product b & {(p +* ((indx b),x))} = product (b +* ((indx b),{x})) ) proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A for x being Point of (A . (indx b)) ex p being ManySortedSet of I st ( p in product b & {(p +* ((indx b),x))} = product (b +* ((indx b),{x})) ) let A be PLS-yielding ManySortedSet of I; ::_thesis: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A for x being Point of (A . (indx b)) ex p being ManySortedSet of I st ( p in product b & {(p +* ((indx b),x))} = product (b +* ((indx b),{x})) ) let b1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: for x being Point of (A . (indx b1)) ex p being ManySortedSet of I st ( p in product b1 & {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) ) set i = indx b1; let x be Point of (A . (indx b1)); ::_thesis: ex p being ManySortedSet of I st ( p in product b1 & {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) ) consider bb being set such that A1: bb in product b1 by XBOOLE_0:def_1; A2: ex bf being Function st ( bf = bb & dom bf = dom b1 & ( for o being set st o in dom b1 holds bf . o in b1 . o ) ) by A1, CARD_3:def_5; A3: dom b1 = I by PARTFUN1:def_2; then reconsider bb = bb as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18; take p = bb; ::_thesis: ( p in product b1 & {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) ) thus p in product b1 by A1; ::_thesis: {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) set bbx = bb +* ((indx b1),x); thus {(p +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) ::_thesis: verum proof thus {(p +* ((indx b1),x))} c= product (b1 +* ((indx b1),{x})) :: according to XBOOLE_0:def_10 ::_thesis: product (b1 +* ((indx b1),{x})) c= {(p +* ((indx b1),x))} proof A4: now__::_thesis:_for_z_being_set_st_z_in_dom_(b1_+*_((indx_b1),{x}))_holds_ (bb_+*_((indx_b1),x))_._z_in_(b1_+*_((indx_b1),{x}))_._z let z be set ; ::_thesis: ( z in dom (b1 +* ((indx b1),{x})) implies (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 ) assume z in dom (b1 +* ((indx b1),{x})) ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 then A5: z in I ; then A6: z in dom bb by PARTFUN1:def_2; percases ( z = indx b1 or z <> indx b1 ) ; supposeA7: z = indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 then (bb +* ((indx b1),x)) . z = x by A6, FUNCT_7:31; then (bb +* ((indx b1),x)) . z in {x} by TARSKI:def_1; hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A3, A7, FUNCT_7:31; ::_thesis: verum end; supposeA8: z <> indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 then (bb +* ((indx b1),x)) . z = bb . z by FUNCT_7:32; then (bb +* ((indx b1),x)) . z in b1 . z by A1, A3, A5, CARD_3:9; hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A8, FUNCT_7:32; ::_thesis: verum end; end; end; let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in {(p +* ((indx b1),x))} or o in product (b1 +* ((indx b1),{x})) ) assume o in {(p +* ((indx b1),x))} ; ::_thesis: o in product (b1 +* ((indx b1),{x})) then A9: o = bb +* ((indx b1),x) by TARSKI:def_1; dom (bb +* ((indx b1),x)) = I by PARTFUN1:def_2 .= dom (b1 +* ((indx b1),{x})) by PARTFUN1:def_2 ; hence o in product (b1 +* ((indx b1),{x})) by A9, A4, CARD_3:9; ::_thesis: verum end; let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in product (b1 +* ((indx b1),{x})) or o in {(p +* ((indx b1),x))} ) assume o in product (b1 +* ((indx b1),{x})) ; ::_thesis: o in {(p +* ((indx b1),x))} then consider u being Function such that A10: u = o and A11: dom u = dom (b1 +* ((indx b1),{x})) and A12: for z being set st z in dom (b1 +* ((indx b1),{x})) holds u . z in (b1 +* ((indx b1),{x})) . z by CARD_3:def_5; A13: now__::_thesis:_for_z_being_set_st_z_in_dom_u_holds_ u_._z_=_(bb_+*_((indx_b1),x))_._z let z be set ; ::_thesis: ( z in dom u implies u . b1 = (bb +* ((indx b1),x)) . b1 ) assume A14: z in dom u ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1 then A15: z in I by A11; reconsider zz = z as Element of I by A11, A14; A16: u . z in (b1 +* ((indx b1),{x})) . z by A11, A12, A14; percases ( zz = indx b1 or zz <> indx b1 ) ; supposeA17: zz = indx b1 ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1 then u . z in {x} by A3, A16, FUNCT_7:31; then u . z = x by TARSKI:def_1; hence u . z = (bb +* ((indx b1),x)) . z by A2, A3, A17, FUNCT_7:31; ::_thesis: verum end; supposeA18: zz <> indx b1 ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1 then ( not b1 . zz is empty & b1 . zz is trivial ) by PENCIL_1:def_21; then b1 . zz is 1 -element ; then consider o being set such that A19: b1 . z = {o} by ZFMISC_1:131; u . z in b1 . z by A16, A18, FUNCT_7:32; then A20: u . z = o by A19, TARSKI:def_1; (bb +* ((indx b1),x)) . z = bb . z by A18, FUNCT_7:32; then (bb +* ((indx b1),x)) . z in {o} by A2, A3, A15, A19; hence u . z = (bb +* ((indx b1),x)) . z by A20, TARSKI:def_1; ::_thesis: verum end; end; end; dom u = I by A11, PARTFUN1:def_2 .= dom (bb +* ((indx b1),x)) by PARTFUN1:def_2 ; then u = bb +* ((indx b1),x) by A13, FUNCT_1:2; hence o in {(p +* ((indx b1),x))} by A10, TARSKI:def_1; ::_thesis: verum end; end; definition let I be non empty finite set ; let b1, b2 be ManySortedSet of I; func diff (b1,b2) -> Nat equals :: PENCIL_3:def 1 card { i where i is Element of I : b1 . i <> b2 . i } ; correctness coherence card { i where i is Element of I : b1 . i <> b2 . i } is Nat; proof { i where i is Element of I : b1 . i <> b2 . i } c= I proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of I : b1 . i <> b2 . i } or a in I ) assume a in { i where i is Element of I : b1 . i <> b2 . i } ; ::_thesis: a in I then ex i being Element of I st ( a = i & b1 . i <> b2 . i ) ; hence a in I ; ::_thesis: verum end; then reconsider F = { i where i is Element of I : b1 . i <> b2 . i } as finite set by FINSET_1:1; card F = card F ; hence card { i where i is Element of I : b1 . i <> b2 . i } is Nat ; ::_thesis: verum end; end; :: deftheorem defines diff PENCIL_3:def_1_:_ for I being non empty finite set for b1, b2 being ManySortedSet of I holds diff (b1,b2) = card { i where i is Element of I : b1 . i <> b2 . i } ; theorem Th19: :: PENCIL_3:19 for I being non empty finite set for b1, b2 being ManySortedSet of I for i being Element of I st b1 . i <> b2 . i holds diff (b1,b2) = (diff (b1,(b2 +* (i,(b1 . i))))) + 1 proof let I be non empty finite set ; ::_thesis: for b1, b2 being ManySortedSet of I for i being Element of I st b1 . i <> b2 . i holds diff (b1,b2) = (diff (b1,(b2 +* (i,(b1 . i))))) + 1 let b1, b2 be ManySortedSet of I; ::_thesis: for i being Element of I st b1 . i <> b2 . i holds diff (b1,b2) = (diff (b1,(b2 +* (i,(b1 . i))))) + 1 let j be Element of I; ::_thesis: ( b1 . j <> b2 . j implies diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1 ) set b3 = b2 +* (j,(b1 . j)); { i where i is Element of I : b1 . i <> b2 . i } c= I proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of I : b1 . i <> b2 . i } or a in I ) assume a in { i where i is Element of I : b1 . i <> b2 . i } ; ::_thesis: a in I then ex i being Element of I st ( a = i & b1 . i <> b2 . i ) ; hence a in I ; ::_thesis: verum end; then reconsider F = { i where i is Element of I : b1 . i <> b2 . i } as finite set by FINSET_1:1; { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } c= I proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } or a in I ) assume a in { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } ; ::_thesis: a in I then ex i being Element of I st ( a = i & b1 . i <> (b2 +* (j,(b1 . j))) . i ) ; hence a in I ; ::_thesis: verum end; then reconsider G = { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } as finite set by FINSET_1:1; assume A1: b1 . j <> b2 . j ; ::_thesis: diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1 A2: F = G \/ {j} proof thus F c= G \/ {j} :: according to XBOOLE_0:def_10 ::_thesis: G \/ {j} c= F proof let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in F or o in G \/ {j} ) assume o in F ; ::_thesis: o in G \/ {j} then consider i being Element of I such that A3: o = i and A4: b1 . i <> b2 . i ; percases ( i = j or i <> j ) ; suppose i = j ; ::_thesis: o in G \/ {j} then o in {j} by A3, TARSKI:def_1; hence o in G \/ {j} by XBOOLE_0:def_3; ::_thesis: verum end; suppose i <> j ; ::_thesis: o in G \/ {j} then (b2 +* (j,(b1 . j))) . i = b2 . i by FUNCT_7:32; then i in G by A4; hence o in G \/ {j} by A3, XBOOLE_0:def_3; ::_thesis: verum end; end; end; let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in G \/ {j} or o in F ) assume A5: o in G \/ {j} ; ::_thesis: o in F percases ( o in G or o in {j} ) by A5, XBOOLE_0:def_3; suppose o in G ; ::_thesis: o in F then consider i being Element of I such that A6: o = i and A7: b1 . i <> (b2 +* (j,(b1 . j))) . i ; now__::_thesis:_not_b1_._i_=_b2_._i assume A8: b1 . i = b2 . i ; ::_thesis: contradiction then i = j by A7, FUNCT_7:32; hence contradiction by A1, A8; ::_thesis: verum end; hence o in F by A6; ::_thesis: verum end; suppose o in {j} ; ::_thesis: o in F then o = j by TARSKI:def_1; hence o in F by A1; ::_thesis: verum end; end; end; now__::_thesis:_not_j_in_G assume j in G ; ::_thesis: contradiction then A9: ex jj being Element of I st ( jj = j & b1 . jj <> (b2 +* (j,(b1 . j))) . jj ) ; dom b2 = I by PARTFUN1:def_2; hence contradiction by A9, FUNCT_7:31; ::_thesis: verum end; hence diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1 by A2, CARD_2:41; ::_thesis: verum end; begin definition let I be non empty set ; let A be PLS-yielding ManySortedSet of I; let B1, B2 be Segre-Coset of A; predB1 '||' B2 means :Def2: :: PENCIL_3:def 2 for x being Point of (Segre_Product A) st x in B1 holds ex y being Point of (Segre_Product A) st ( y in B2 & x,y are_collinear ); end; :: deftheorem Def2 defines '||' PENCIL_3:def_2_:_ for I being non empty set for A being PLS-yielding ManySortedSet of I for B1, B2 being Segre-Coset of A holds ( B1 '||' B2 iff for x being Point of (Segre_Product A) st x in B1 holds ex y being Point of (Segre_Product A) st ( y in B2 & x,y are_collinear ) ); theorem Th20: :: PENCIL_3:20 for I being non empty set for A being PLS-yielding ManySortedSet of I for B1, B2 being Segre-Coset of A st B1 '||' B2 holds for f being Collineation of (Segre_Product A) for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds C1 '||' C2 proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I for B1, B2 being Segre-Coset of A st B1 '||' B2 holds for f being Collineation of (Segre_Product A) for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds C1 '||' C2 let A be PLS-yielding ManySortedSet of I; ::_thesis: for B1, B2 being Segre-Coset of A st B1 '||' B2 holds for f being Collineation of (Segre_Product A) for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds C1 '||' C2 let B1, B2 be Segre-Coset of A; ::_thesis: ( B1 '||' B2 implies for f being Collineation of (Segre_Product A) for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds C1 '||' C2 ) assume A1: B1 '||' B2 ; ::_thesis: for f being Collineation of (Segre_Product A) for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds C1 '||' C2 let f be Collineation of (Segre_Product A); ::_thesis: for C1, C2 being Segre-Coset of A st C1 = f .: B1 & C2 = f .: B2 holds C1 '||' C2 let C1, C2 be Segre-Coset of A; ::_thesis: ( C1 = f .: B1 & C2 = f .: B2 implies C1 '||' C2 ) assume that A2: C1 = f .: B1 and A3: C2 = f .: B2 ; ::_thesis: C1 '||' C2 let x be Point of (Segre_Product A); :: according to PENCIL_3:def_2 ::_thesis: ( x in C1 implies ex y being Point of (Segre_Product A) st ( y in C2 & x,y are_collinear ) ) assume x in C1 ; ::_thesis: ex y being Point of (Segre_Product A) st ( y in C2 & x,y are_collinear ) then consider a being set such that A4: a in dom f and A5: a in B1 and A6: x = f . a by A2, FUNCT_1:def_6; reconsider a = a as Point of (Segre_Product A) by A4; consider b being Point of (Segre_Product A) such that A7: b in B2 and A8: a,b are_collinear by A1, A5, Def2; take y = f . b; ::_thesis: ( y in C2 & x,y are_collinear ) A9: dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1; hence y in C2 by A3, A7, FUNCT_1:def_6; ::_thesis: x,y are_collinear percases ( a = b or a <> b ) ; suppose a = b ; ::_thesis: x,y are_collinear hence x,y are_collinear by A6, PENCIL_1:def_1; ::_thesis: verum end; suppose a <> b ; ::_thesis: x,y are_collinear then consider l being Block of (Segre_Product A) such that A10: {a,b} c= l by A8, PENCIL_1:def_1; reconsider k = f .: l as Block of (Segre_Product A) ; b in l by A10, ZFMISC_1:32; then A11: y in k by A9, FUNCT_1:def_6; a in l by A10, ZFMISC_1:32; then x in k by A4, A6, FUNCT_1:def_6; then {x,y} c= k by A11, ZFMISC_1:32; hence x,y are_collinear by PENCIL_1:def_1; ::_thesis: verum end; end; end; theorem Th21: :: PENCIL_3:21 for I being non empty set for A being PLS-yielding ManySortedSet of I for B1, B2 being Segre-Coset of A st B1 misses B2 holds ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ) proof let I be non empty set ; ::_thesis: for A being PLS-yielding ManySortedSet of I for B1, B2 being Segre-Coset of A st B1 misses B2 holds ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ) let A be PLS-yielding ManySortedSet of I; ::_thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 holds ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ) let B1, B2 be Segre-Coset of A; ::_thesis: ( B1 misses B2 implies ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ) ) consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A1: B1 = product L1 and L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def_2; assume A2: B1 misses B2 ; ::_thesis: ( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ) thus ( B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ) ::_thesis: ( ( for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ) implies B1 '||' B2 ) proof assume A3: B1 '||' B2 ; ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A4: B2 = product L2 and A5: L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def_2; consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A6: B1 = product L1 and A7: L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def_2; let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & B2 = product b2 implies ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ) assume that A8: B1 = product b1 and A9: B2 = product b2 ; ::_thesis: ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) A10: b1 = L1 by A8, A6, PUA2MSS1:2; thus A11: indx b1 = indx b2 ::_thesis: ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) proof assume indx b1 <> indx b2 ; ::_thesis: contradiction then b2 . (indx b1) is 1 -element by PENCIL_1:12; then consider c2 being set such that A12: b2 . (indx b1) = {c2} by ZFMISC_1:131; set bl = the Block of (A . (indx b1)); consider p0 being set such that A13: p0 in B1 by A8, XBOOLE_0:def_1; reconsider p0 = p0 as Point of (Segre_Product A) by A13; reconsider p = p0 as Element of Carrier A by Th6; the Block of (A . (indx b1)) in the topology of (A . (indx b1)) ; then ( 2 c= card the Block of (A . (indx b1)) & card the Block of (A . (indx b1)) c= card the carrier of (A . (indx b1)) ) by CARD_1:11, PENCIL_1:def_6; then consider a being set such that A14: a in the carrier of (A . (indx b1)) and A15: a <> c2 by PENCIL_1:3, XBOOLE_1:1; reconsider a = a as Point of (A . (indx b1)) by A14; reconsider x = p +* ((indx b1),a) as Point of (Segre_Product A) by PENCIL_1:25; reconsider x1 = x as Element of Carrier A by Th6; A16: dom x1 = I by PARTFUN1:def_2 .= dom b1 by PARTFUN1:def_2 ; now__::_thesis:_for_i_being_set_st_i_in_dom_x1_holds_ x1_._i_in_b1_._i let i be set ; ::_thesis: ( i in dom x1 implies x1 . b1 in b1 . b1 ) assume A17: i in dom x1 ; ::_thesis: x1 . b1 in b1 . b1 then i in I ; then A18: i in dom p by PARTFUN1:def_2; percases ( i = indx b1 or i <> indx b1 ) ; supposeA19: i = indx b1 ; ::_thesis: x1 . b1 in b1 . b1 then x1 . i = a by A18, FUNCT_7:31; hence x1 . i in b1 . i by A7, A10, A19; ::_thesis: verum end; suppose i <> indx b1 ; ::_thesis: x1 . b1 in b1 . b1 then A20: x1 . i = p . i by FUNCT_7:32; ex f being Function st ( f = p & dom f = dom b1 & ( for a being set st a in dom b1 holds f . a in b1 . a ) ) by A8, A13, CARD_3:def_5; hence x1 . i in b1 . i by A16, A17, A20; ::_thesis: verum end; end; end; then A21: x in B1 by A8, A16, CARD_3:def_5; then consider y being Point of (Segre_Product A) such that A22: y in B2 and A23: x,y are_collinear by A3, Def2; reconsider y1 = y as Element of Carrier A by Th6; percases ( y = x or y <> x ) ; suppose y = x ; ::_thesis: contradiction then y in B1 /\ B2 by A21, A22, XBOOLE_0:def_4; hence contradiction by A2, XBOOLE_0:def_7; ::_thesis: verum end; suppose y <> x ; ::_thesis: contradiction then consider i0 being Element of I such that for a, b being Point of (A . i0) st a = x1 . i0 & b = y1 . i0 holds ( a <> b & a,b are_collinear ) and A24: for j being Element of I st j <> i0 holds x1 . j = y1 . j by A23, Th17; A25: dom y1 = I by PARTFUN1:def_2 .= dom b1 by PARTFUN1:def_2 ; now__::_thesis:_for_i_being_set_st_i_in_dom_y1_holds_ y1_._i_in_b1_._i let i be set ; ::_thesis: ( i in dom y1 implies y1 . b1 in b1 . b1 ) assume A26: i in dom y1 ; ::_thesis: y1 . b1 in b1 . b1 then reconsider i5 = i as Element of I ; percases ( i = indx b1 or i <> indx b1 ) ; supposeA27: i = indx b1 ; ::_thesis: y1 . b1 in b1 . b1 reconsider i1 = i as Element of I by A26; y1 . i1 is Element of (Carrier A) . i1 by PBOOLE:def_14; then y1 . i1 is Element of [#] (A . i1) by Th7; hence y1 . i in b1 . i by A7, A10, A27; ::_thesis: verum end; supposeA28: i <> indx b1 ; ::_thesis: y1 . b1 in b1 . b1 ( ex g being Function st ( g = y1 & dom g = dom b2 & ( for a being set st a in dom b2 holds g . a in b2 . a ) ) & dom b2 = I ) by A9, A22, CARD_3:def_5, PARTFUN1:def_2; then y1 . (indx b1) in b2 . (indx b1) ; then A29: y1 . (indx b1) = c2 by A12, TARSKI:def_1; dom p = I by PARTFUN1:def_2; then x1 . (indx b1) = a by FUNCT_7:31; then i0 = indx b1 by A15, A24, A29; then A30: y1 . i5 = x1 . i5 by A24, A28; A31: x1 . i = p . i by A28, FUNCT_7:32; ex f being Function st ( f = p & dom f = dom b1 & ( for a being set st a in dom b1 holds f . a in b1 . a ) ) by A8, A13, CARD_3:def_5; hence y1 . i in b1 . i by A25, A26, A30, A31; ::_thesis: verum end; end; end; then y in B1 by A8, A25, CARD_3:def_5; then y in B1 /\ B2 by A22, XBOOLE_0:def_4; hence contradiction by A2, XBOOLE_0:def_7; ::_thesis: verum end; end; end; A32: b2 = L2 by A9, A4, PUA2MSS1:2; thus ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ::_thesis: verum proof consider x being set such that A33: x in B1 by A8, XBOOLE_0:def_1; reconsider x = x as Point of (Segre_Product A) by A33; consider y being Point of (Segre_Product A) such that A34: y in B2 and A35: x,y are_collinear by A3, A33, Def2; reconsider y1 = y as Element of Carrier A by Th6; reconsider x1 = x as Element of Carrier A by Th6; now__::_thesis:_not_x_=_y assume x = y ; ::_thesis: contradiction then B1 /\ B2 <> {} by A33, A34, XBOOLE_0:def_4; hence contradiction by A2, XBOOLE_0:def_7; ::_thesis: verum end; then consider r being Element of I such that A36: for a, b being Point of (A . r) st a = x1 . r & b = y1 . r holds ( a <> b & a,b are_collinear ) and A37: for j being Element of I st j <> r holds x1 . j = y1 . j by A35, Th17; take r ; ::_thesis: ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) now__::_thesis:_not_r_=_indx_b1 assume A38: r = indx b1 ; ::_thesis: contradiction A39: now__::_thesis:_for_o_being_set_st_o_in_dom_b1_holds_ y1_._o_in_b1_._o let o be set ; ::_thesis: ( o in dom b1 implies y1 . b1 in b1 . b1 ) assume A40: o in dom b1 ; ::_thesis: y1 . b1 in b1 . b1 then reconsider o1 = o as Element of I ; percases ( o1 = r or o1 <> r ) ; supposeA41: o1 = r ; ::_thesis: y1 . b1 in b1 . b1 y1 . o1 is Element of (Carrier A) . o1 by PBOOLE:def_14; then y1 . o1 is Element of [#] (A . o1) by Th7; hence y1 . o in b1 . o by A7, A10, A38, A41; ::_thesis: verum end; supposeA42: o1 <> r ; ::_thesis: y1 . b1 in b1 . b1 then b1 . o1 is 1 -element by A38, PENCIL_1:12; then consider c being set such that A43: b1 . o1 = {c} by ZFMISC_1:131; x1 . o1 in b1 . o1 by A8, A33, A40, CARD_3:9; then c = x1 . o1 by A43, TARSKI:def_1 .= y1 . o1 by A37, A42 ; hence y1 . o in b1 . o by A43, TARSKI:def_1; ::_thesis: verum end; end; end; dom y1 = I by PARTFUN1:def_2 .= dom b1 by PARTFUN1:def_2 ; then y1 in B1 by A8, A39, CARD_3:9; then B1 /\ B2 <> {} by A34, XBOOLE_0:def_4; hence contradiction by A2, XBOOLE_0:def_7; ::_thesis: verum end; hence r <> indx b1 ; ::_thesis: ( ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) thus for i being Element of I st i <> r holds b1 . i = b2 . i ::_thesis: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear proof let i be Element of I; ::_thesis: ( i <> r implies b1 . i = b2 . i ) assume A44: i <> r ; ::_thesis: b1 . i = b2 . i percases ( i = indx b1 or i <> indx b1 ) ; suppose i = indx b1 ; ::_thesis: b1 . i = b2 . i hence b1 . i = b2 . i by A7, A5, A10, A32, A11; ::_thesis: verum end; supposeA45: i <> indx b1 ; ::_thesis: b1 . i = b2 . i then b2 . i is 1 -element by A11, PENCIL_1:12; then A46: ex d being set st b2 . i = {d} by ZFMISC_1:131; dom b2 = I by PARTFUN1:def_2; then A47: y1 . i in b2 . i by A9, A34, CARD_3:9; b1 . i is 1 -element by A45, PENCIL_1:12; then consider c being set such that A48: b1 . i = {c} by ZFMISC_1:131; dom b1 = I by PARTFUN1:def_2; then x1 . i in b1 . i by A8, A33, CARD_3:9; then c = x1 . i by A48, TARSKI:def_1 .= y1 . i by A37, A44 ; hence b1 . i = b2 . i by A48, A46, A47, TARSKI:def_1; ::_thesis: verum end; end; end; let c1, c2 be Point of (A . r); ::_thesis: ( b1 . r = {c1} & b2 . r = {c2} implies c1,c2 are_collinear ) assume that A49: b1 . r = {c1} and A50: b2 . r = {c2} ; ::_thesis: c1,c2 are_collinear dom L2 = I by PARTFUN1:def_2; then y1 . r in b2 . r by A4, A32, A34, CARD_3:9; then A51: c2 = y1 . r by A50, TARSKI:def_1; dom L1 = I by PARTFUN1:def_2; then x1 . r in b1 . r by A6, A10, A33, CARD_3:9; then c1 = x1 . r by A49, TARSKI:def_1; hence c1,c2 are_collinear by A36, A51; ::_thesis: verum end; end; consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A52: B2 = product L2 and L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def_2; assume A53: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 & ex r being Element of I st ( r <> indx b1 & ( for i being Element of I st i <> r holds b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear ) ) ) ; ::_thesis: B1 '||' B2 then consider r being Element of I such that A54: r <> indx L1 and A55: for i being Element of I st i <> r holds L1 . i = L2 . i and A56: for c1, c2 being Point of (A . r) st L1 . r = {c1} & L2 . r = {c2} holds c1,c2 are_collinear by A1, A52; indx L1 = indx L2 by A53, A1, A52; then L2 . r is 1 -element by A54, PENCIL_1:12; then consider c2 being set such that A57: L2 . r = {c2} by ZFMISC_1:131; L2 c= Carrier A by PBOOLE:def_18; then L2 . r c= (Carrier A) . r by PBOOLE:def_2; then {c2} c= [#] (A . r) by A57, Th7; then reconsider c2 = c2 as Point of (A . r) by ZFMISC_1:31; L1 . r is 1 -element by A54, PENCIL_1:12; then consider c1 being set such that A58: L1 . r = {c1} by ZFMISC_1:131; L1 c= Carrier A by PBOOLE:def_18; then L1 . r c= (Carrier A) . r by PBOOLE:def_2; then {c1} c= [#] (A . r) by A58, Th7; then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31; A59: now__::_thesis:_not_c1_=_c2 assume A60: c1 = c2 ; ::_thesis: contradiction A61: now__::_thesis:_for_s_being_set_st_s_in_dom_L1_holds_ L1_._s_=_L2_._s let s be set ; ::_thesis: ( s in dom L1 implies L1 . b1 = L2 . b1 ) assume s in dom L1 ; ::_thesis: L1 . b1 = L2 . b1 then reconsider s1 = s as Element of I ; percases ( s1 = r or s1 <> r ) ; suppose s1 = r ; ::_thesis: L1 . b1 = L2 . b1 hence L1 . s = L2 . s by A58, A57, A60; ::_thesis: verum end; suppose s1 <> r ; ::_thesis: L1 . b1 = L2 . b1 hence L1 . s = L2 . s by A55; ::_thesis: verum end; end; end; dom L1 = I by PARTFUN1:def_2 .= dom L2 by PARTFUN1:def_2 ; then L1 = L2 by A61, FUNCT_1:2; then B1 /\ B1 = {} by A2, A1, A52, XBOOLE_0:def_7; hence contradiction by A1; ::_thesis: verum end; c1,c2 are_collinear by A56, A58, A57; then consider bb being Block of (A . r) such that A62: {c1,c2} c= bb by A59, PENCIL_1:def_1; let x be Point of (Segre_Product A); :: according to PENCIL_3:def_2 ::_thesis: ( x in B1 implies ex y being Point of (Segre_Product A) st ( y in B2 & x,y are_collinear ) ) reconsider x1 = x as Element of Carrier A by Th6; reconsider y = x1 +* (r,c2) as Point of (Segre_Product A) by PENCIL_1:25; reconsider y1 = y as ManySortedSet of I ; assume x in B1 ; ::_thesis: ex y being Point of (Segre_Product A) st ( y in B2 & x,y are_collinear ) then A63: ex x2 being Function st ( x2 = x & dom x2 = dom L1 & ( for o being set st o in dom L1 holds x2 . o in L1 . o ) ) by A1, CARD_3:def_5; A64: now__::_thesis:_for_a_being_set_st_a_in_dom_L2_holds_ y1_._a_in_L2_._a let a be set ; ::_thesis: ( a in dom L2 implies y1 . b1 in L2 . b1 ) assume a in dom L2 ; ::_thesis: y1 . b1 in L2 . b1 then reconsider a1 = a as Element of I ; percases ( a1 = r or a1 <> r ) ; supposeA65: a1 = r ; ::_thesis: y1 . b1 in L2 . b1 dom x1 = I by PARTFUN1:def_2; then y1 . a = c2 by A65, FUNCT_7:31; hence y1 . a in L2 . a by A57, A65, TARSKI:def_1; ::_thesis: verum end; supposeA66: a1 <> r ; ::_thesis: y1 . b1 in L2 . b1 then ( dom x1 = I & y1 . a1 = x1 . a1 ) by FUNCT_7:32, PARTFUN1:def_2; then y1 . a1 in L1 . a1 by A63; hence y1 . a in L2 . a by A55, A66; ::_thesis: verum end; end; end; take y ; ::_thesis: ( y in B2 & x,y are_collinear ) dom y1 = I by PARTFUN1:def_2 .= dom L2 by PARTFUN1:def_2 ; hence y in B2 by A52, A64, CARD_3:def_5; ::_thesis: x,y are_collinear reconsider B = product ({x1} +* (r,bb)) as Block of (Segre_Product A) by Th16; A67: now__::_thesis:_for_s_being_set_st_s_in_dom_y1_holds_ y1_._s_in_({x1}_+*_(r,bb))_._s let s be set ; ::_thesis: ( s in dom y1 implies y1 . b1 in ({x1} +* (r,bb)) . b1 ) assume s in dom y1 ; ::_thesis: y1 . b1 in ({x1} +* (r,bb)) . b1 then A68: s in I ; then A69: ( s in dom {x1} & s in dom x1 ) by PARTFUN1:def_2; percases ( s = r or s <> r ) ; suppose s = r ; ::_thesis: y1 . b1 in ({x1} +* (r,bb)) . b1 then ( y1 . s = c2 & bb = ({x1} +* (r,bb)) . s ) by A69, FUNCT_7:31; hence y1 . s in ({x1} +* (r,bb)) . s by A62, ZFMISC_1:32; ::_thesis: verum end; supposeA70: s <> r ; ::_thesis: y1 . b1 in ({x1} +* (r,bb)) . b1 then {x1} . s = ({x1} +* (r,bb)) . s by FUNCT_7:32; then A71: {(x1 . s)} = ({x1} +* (r,bb)) . s by A68, PZFMISC1:def_1; y1 . s = x1 . s by A70, FUNCT_7:32; hence y1 . s in ({x1} +* (r,bb)) . s by A71, TARSKI:def_1; ::_thesis: verum end; end; end; dom y1 = I by PARTFUN1:def_2 .= dom ({x1} +* (r,bb)) by PARTFUN1:def_2 ; then A72: y in B by A67, CARD_3:def_5; A73: now__::_thesis:_for_s_being_set_st_s_in_dom_x1_holds_ x1_._s_in_({x1}_+*_(r,bb))_._s let s be set ; ::_thesis: ( s in dom x1 implies x1 . b1 in ({x1} +* (r,bb)) . b1 ) assume A74: s in dom x1 ; ::_thesis: x1 . b1 in ({x1} +* (r,bb)) . b1 then A75: s in I ; then A76: s in dom {x1} by PARTFUN1:def_2; percases ( s = r or s <> r ) ; supposeA77: s = r ; ::_thesis: x1 . b1 in ({x1} +* (r,bb)) . b1 x1 . s in L1 . s by A63, A74; then A78: x1 . s = c1 by A58, A77, TARSKI:def_1; bb = ({x1} +* (r,bb)) . s by A76, A77, FUNCT_7:31; hence x1 . s in ({x1} +* (r,bb)) . s by A62, A78, ZFMISC_1:32; ::_thesis: verum end; suppose s <> r ; ::_thesis: x1 . b1 in ({x1} +* (r,bb)) . b1 then {x1} . s = ({x1} +* (r,bb)) . s by FUNCT_7:32; then {(x1 . s)} = ({x1} +* (r,bb)) . s by A75, PZFMISC1:def_1; hence x1 . s in ({x1} +* (r,bb)) . s by TARSKI:def_1; ::_thesis: verum end; end; end; dom x1 = I by PARTFUN1:def_2 .= dom ({x1} +* (r,bb)) by PARTFUN1:def_2 ; then x in B by A73, CARD_3:def_5; then {x,y} c= B by A72, ZFMISC_1:32; hence x,y are_collinear by PENCIL_1:def_1; ::_thesis: verum end; theorem Th22: :: PENCIL_3:22 for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds for i being Element of I for p being Point of (A . i) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) proof let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds for i being Element of I for p being Point of (A . i) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is connected ) implies for i being Element of I for p being Point of (A . i) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) assume A1: for i being Element of I holds A . i is connected ; ::_thesis: for i being Element of I for p being Point of (A . i) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) let i be Element of I; ::_thesis: for p being Point of (A . i) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) let p be Point of (A . i); ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i implies ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) assume that A2: product b2 is Segre-Coset of A and A3: b1 = b2 +* (i,{p}) and A4: not p in b2 . i ; ::_thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) defpred S1[ set , set ] means for a, b being Point of (A . i) st $1 = a & $2 = b holds a,b are_collinear ; A5: now__::_thesis:_not_i_=_indx_b2 assume i = indx b2 ; ::_thesis: contradiction then b2 . i = [#] (A . i) by A2, Th10; hence contradiction by A4; ::_thesis: verum end; then b2 . i is 1 -element by PENCIL_1:12; then consider q being set such that A6: b2 . i = {q} by ZFMISC_1:131; b2 c= Carrier A by PBOOLE:def_18; then b2 . i c= (Carrier A) . i by PBOOLE:def_2; then {q} c= [#] (A . i) by A6, Th7; then reconsider q = q as Point of (A . i) by ZFMISC_1:31; A . i is connected by A1; then consider f being FinSequence of the carrier of (A . i) such that A7: ( p = f . 1 & q = f . (len f) ) and A8: for j being Nat st 1 <= j & j < len f holds for a, b being Point of (A . i) st a = f . j & b = f . (j + 1) holds a,b are_collinear by PENCIL_1:def_10; A9: for j being Element of NAT for x, y being set st 1 <= j & j < len f & x = f . j & y = f . (j + 1) holds S1[x,y] by A8; consider F being one-to-one FinSequence of the carrier of (A . i) such that A10: ( p = F . 1 & q = F . (len F) & rng F c= rng f & ( for j being Element of NAT st 1 <= j & j < len F holds S1[F . j,F . (j + 1)] ) ) from PENCIL_2:sch_1(A7, A9); A11: now__::_thesis:_not_F_=_{} assume F = {} ; ::_thesis: contradiction then dom F = {} ; then ( F . 1 = {} & F . (len F) = {} ) by FUNCT_1:def_2; hence contradiction by A4, A6, A10, TARSKI:def_1; ::_thesis: verum end; deffunc H1( set ) -> set = product (b2 +* (i,{(F . $1)})); consider G being FinSequence such that A12: ( len G = len F & ( for j being Nat st j in dom G holds G . j = H1(j) ) ) from FINSEQ_1:sch_2(); rng G c= bool the carrier of (Segre_Product A) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng G or a in bool the carrier of (Segre_Product A) ) assume a in rng G ; ::_thesis: a in bool the carrier of (Segre_Product A) then consider o being set such that A13: o in dom G and A14: G . o = a by FUNCT_1:def_3; reconsider o = o as Element of NAT by A13; dom G = dom F by A12, FINSEQ_3:29; then F . o in rng F by A13, FUNCT_1:3; then {(F . o)} is Subset of (A . i) by ZFMISC_1:31; then A15: product (b2 +* (i,{(F . o)})) is Subset of (Segre_Product A) by Th14; G . o = product (b2 +* (i,{(F . o)})) by A12, A13; hence a in bool the carrier of (Segre_Product A) by A14, A15; ::_thesis: verum end; then reconsider D = G as FinSequence of bool the carrier of (Segre_Product A) by FINSEQ_1:def_4; take D ; ::_thesis: ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) A16: dom G = Seg (len F) by A12, FINSEQ_1:def_3; dom F = Seg (len F) by FINSEQ_1:def_3; hence D . 1 = product b1 by A3, A10, A12, A16, A11, FINSEQ_3:32; ::_thesis: ( D . (len D) = product b2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) D . (len D) = product (b2 +* (i,{(F . (len F))})) by A12, A16, A11, FINSEQ_1:3; hence D . (len D) = product b2 by A6, A10, FUNCT_7:35; ::_thesis: ( ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) thus for j being Nat st j in dom D holds D . j is Segre-Coset of A ::_thesis: for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) proof let j be Nat; ::_thesis: ( j in dom D implies D . j is Segre-Coset of A ) assume A17: j in dom D ; ::_thesis: D . j is Segre-Coset of A then j in Seg (len F) by A12, FINSEQ_1:def_3; then j in dom F by FINSEQ_1:def_3; then F . j in rng F by FUNCT_1:3; then reconsider Fj = F . j as Point of (A . i) ; reconsider BB = b2 +* (i,{Fj}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13; BB . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32; then not BB . (indx b2) is trivial by PENCIL_1:def_21; then A18: indx BB = indx b2 by PENCIL_1:def_21; then A19: BB . (indx BB) = b2 . (indx b2) by A5, FUNCT_7:32 .= [#] (A . (indx BB)) by A2, A18, Th10 ; A20: D . j = product BB by A12, A17; then D . j is Subset of (Segre_Product A) by Th14; hence D . j is Segre-Coset of A by A20, A19, PENCIL_2:def_2; ::_thesis: verum end; A21: dom b2 = I by PARTFUN1:def_2; thus for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ::_thesis: verum proof let j be Nat; ::_thesis: ( 1 <= j & j < len D implies for Di, Di1 being Segre-Coset of A st Di = D . j & Di1 = D . (j + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) assume A22: ( 1 <= j & j < len D ) ; ::_thesis: for Di, Di1 being Segre-Coset of A st Di = D . j & Di1 = D . (j + 1) holds ( Di misses Di1 & Di '||' Di1 ) let Di, Di1 be Segre-Coset of A; ::_thesis: ( Di = D . j & Di1 = D . (j + 1) implies ( Di misses Di1 & Di '||' Di1 ) ) assume that A23: Di = D . j and A24: Di1 = D . (j + 1) ; ::_thesis: ( Di misses Di1 & Di '||' Di1 ) reconsider j = j as Element of NAT by ORDINAL1:def_12; j in dom D by A22, FINSEQ_3:25; then j in Seg (len F) by A12, FINSEQ_1:def_3; then j in dom F by FINSEQ_1:def_3; then F . j in rng F by FUNCT_1:3; then reconsider Fj = F . j as Point of (A . i) ; reconsider BB1 = b2 +* (i,{Fj}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13; A25: j in dom D by A22, FINSEQ_3:25; then A26: D . j = product BB1 by A12; ( 1 <= j + 1 & j + 1 <= len D ) by A22, NAT_1:13; then j + 1 in dom D by FINSEQ_3:25; then j + 1 in Seg (len F) by A12, FINSEQ_1:def_3; then j + 1 in dom F by FINSEQ_1:def_3; then F . (j + 1) in rng F by FUNCT_1:3; then reconsider Fj2 = F . (j + 1) as Point of (A . i) ; reconsider BB2 = b2 +* (i,{Fj2}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13; ( 1 <= j + 1 & j + 1 <= len D ) by A22, NAT_1:13; then A27: j + 1 in dom D by FINSEQ_3:25; then A28: j + 1 in Seg (len F) by A12, FINSEQ_1:def_3; A29: D . (j + 1) = product BB2 by A12, A27; A30: j in Seg (len F) by A12, A25, FINSEQ_1:def_3; thus A31: Di misses Di1 ::_thesis: Di '||' Di1 proof A32: j <> j + 1 ; assume Di /\ Di1 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A33: x in Di /\ Di1 by XBOOLE_0:def_1; x in Di1 by A33, XBOOLE_0:def_4; then consider x2 being Function such that A34: x2 = x and dom x2 = dom (b2 +* (i,{(F . (j + 1))})) and A35: for o being set st o in dom (b2 +* (i,{(F . (j + 1))})) holds x2 . o in (b2 +* (i,{(F . (j + 1))})) . o by A24, A29, CARD_3:def_5; dom (b2 +* (i,{(F . (j + 1))})) = I by PARTFUN1:def_2; then x2 . i in (b2 +* (i,{(F . (j + 1))})) . i by A35; then x2 . i in {(F . (j + 1))} by A21, FUNCT_7:31; then A36: x2 . i = F . (j + 1) by TARSKI:def_1; x in Di by A33, XBOOLE_0:def_4; then consider x1 being Function such that A37: x1 = x and dom x1 = dom (b2 +* (i,{(F . j)})) and A38: for o being set st o in dom (b2 +* (i,{(F . j)})) holds x1 . o in (b2 +* (i,{(F . j)})) . o by A23, A26, CARD_3:def_5; dom (b2 +* (i,{(F . j)})) = I by PARTFUN1:def_2; then x1 . i in (b2 +* (i,{(F . j)})) . i by A38; then x1 . i in {(F . j)} by A21, FUNCT_7:31; then A39: x1 . i = F . j by TARSKI:def_1; ( j in dom F & j + 1 in dom F ) by A30, A28, FINSEQ_1:def_3; hence contradiction by A37, A34, A39, A36, A32, FUNCT_1:def_4; ::_thesis: verum end; now__::_thesis:_for_c1,_c2_being_non_trivial-yielding_Segre-like_ManySortedSubset_of_Carrier_A_st_Di_=_product_c1_&_Di1_=_product_c2_holds_ (_indx_c1_=_indx_c2_&_ex_r_being_Element_of_I_st_ (_r_<>_indx_c1_&_(_for_j_being_Element_of_I_st_j_<>_r_holds_ c1_._j_=_c2_._j_)_&_(_for_p1,_p2_being_Point_of_(A_._r)_st_c1_._r_=_{p1}_&_c2_._r_=_{p2}_holds_ p1,p2_are_collinear_)_)_) let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( Di = product c1 & Di1 = product c2 implies ( indx c1 = indx c2 & ex r being Element of I st ( r <> indx c1 & ( for j being Element of I st j <> r holds c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds p1,p2 are_collinear ) ) ) ) assume that A40: Di = product c1 and A41: Di1 = product c2 ; ::_thesis: ( indx c1 = indx c2 & ex r being Element of I st ( r <> indx c1 & ( for j being Element of I st j <> r holds c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds p1,p2 are_collinear ) ) ) A42: c2 = b2 +* (i,{(F . (j + 1))}) by A24, A29, A41, PUA2MSS1:2; then c2 . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32; then A43: not c2 . (indx b2) is trivial by PENCIL_1:def_21; A44: c1 = b2 +* (i,{(F . j)}) by A23, A26, A40, PUA2MSS1:2; then c1 . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32; then A45: not c1 . (indx b2) is trivial by PENCIL_1:def_21; then indx c1 = indx b2 by PENCIL_1:def_21; hence indx c1 = indx c2 by A43, PENCIL_1:def_21; ::_thesis: ex r being Element of I st ( r <> indx c1 & ( for j being Element of I st j <> r holds c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds p1,p2 are_collinear ) ) take r = i; ::_thesis: ( r <> indx c1 & ( for j being Element of I st j <> r holds c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds p1,p2 are_collinear ) ) thus r <> indx c1 by A5, A45, PENCIL_1:def_21; ::_thesis: ( ( for j being Element of I st j <> r holds c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds p1,p2 are_collinear ) ) thus for j being Element of I st j <> r holds c1 . j = c2 . j ::_thesis: for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds p1,p2 are_collinear proof let j be Element of I; ::_thesis: ( j <> r implies c1 . j = c2 . j ) assume A46: j <> r ; ::_thesis: c1 . j = c2 . j hence c1 . j = b2 . j by A44, FUNCT_7:32 .= c2 . j by A42, A46, FUNCT_7:32 ; ::_thesis: verum end; thus for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds p1,p2 are_collinear ::_thesis: verum proof let p1, p2 be Point of (A . r); ::_thesis: ( c1 . r = {p1} & c2 . r = {p2} implies p1,p2 are_collinear ) assume that A47: c1 . r = {p1} and A48: c2 . r = {p2} ; ::_thesis: p1,p2 are_collinear c2 . r = {(F . (j + 1))} by A21, A42, FUNCT_7:31; then A49: F . (j + 1) = p2 by A48, ZFMISC_1:3; c1 . r = {(F . j)} by A21, A44, FUNCT_7:31; then F . j = p1 by A47, ZFMISC_1:3; hence p1,p2 are_collinear by A10, A12, A22, A49; ::_thesis: verum end; end; hence Di '||' Di1 by A31, Th21; ::_thesis: verum end; end; theorem Th23: :: PENCIL_3:23 for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds for B1, B2 being Segre-Coset of A st B1 misses B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) proof let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds for B1, B2 being Segre-Coset of A st B1 misses B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is connected ) implies for B1, B2 being Segre-Coset of A st B1 misses B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) ) assume A1: for i being Element of I holds A . i is connected ; ::_thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) let B1, B2 be Segre-Coset of A; ::_thesis: ( B1 misses B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) ) assume A2: B1 misses B2 ; ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & B2 = product b2 implies ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) ) assume that A3: B1 = product b1 and A4: B2 = product b2 ; ::_thesis: ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) thus ( indx b1 = indx b2 implies ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) ::_thesis: ( ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) implies indx b1 = indx b2 ) proof defpred S1[ Nat] means for c1, c2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st indx c1 = indx c2 & product c1 is Segre-Coset of A & product c2 is Segre-Coset of A & product c1 misses product c2 & diff (c1,c2) = $1 holds ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ); A5: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( indx c1 = indx c2 & product c1 is Segre-Coset of A & product c2 is Segre-Coset of A & product c1 misses product c2 & diff (c1,c2) = k + 1 implies ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) assume that A7: indx c1 = indx c2 and A8: product c1 is Segre-Coset of A and A9: product c2 is Segre-Coset of A and product c1 misses product c2 and A10: diff (c1,c2) = k + 1 ; ::_thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) { i where i is Element of I : c1 . i <> c2 . i } <> {} by A10; then consider j0 being set such that A11: j0 in { i where i is Element of I : c1 . i <> c2 . i } by XBOOLE_0:def_1; consider j being Element of I such that j0 = j and A12: c1 . j <> c2 . j by A11; A13: c2 . (indx c1) = [#] (A . (indx c1)) by A7, A9, Th10; then A14: j <> indx c1 by A8, A12, Th10; then c1 . j is 1 -element by PENCIL_1:12; then consider p being set such that A15: c1 . j = {p} by ZFMISC_1:131; c1 c= Carrier A by PBOOLE:def_18; then {p} c= (Carrier A) . j by A15, PBOOLE:def_2; then p in (Carrier A) . j by ZFMISC_1:31; then p in [#] (A . j) by Th7; then reconsider p = p as Point of (A . j) ; reconsider c3 = c2 +* (j,{p}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A7, A14, Th13; A16: c3 . (indx c1) = [#] (A . (indx c1)) by A13, A14, FUNCT_7:32; c2 . j is 1 -element by A7, A14, PENCIL_1:12; then A17: ex r being set st c2 . j = {r} by ZFMISC_1:131; not A . (indx c1) is trivial by Th2; then A18: indx c3 = indx c1 by A16, PENCIL_1:def_21; product c3 is Subset of (Segre_Product A) by Th14; then A19: product c3 is Segre-Coset of A by A16, A18, PENCIL_2:def_2; percases ( product c1 misses product c3 or product c1 meets product c3 ) ; supposeA20: product c1 misses product c3 ; ::_thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) diff (c1,c2) = (diff (c1,c3)) + 1 by A12, A15, Th19; then consider E being FinSequence of bool the carrier of (Segre_Product A) such that A21: E . 1 = product c1 and A22: E . (len E) = product c3 and A23: for i being Nat st i in dom E holds E . i is Segre-Coset of A and A24: for i being Nat st 1 <= i & i < len E holds for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds ( Ei misses Ei1 & Ei '||' Ei1 ) by A6, A8, A10, A18, A19, A20; not p in c2 . j by A12, A15, A17, TARSKI:def_1; then consider F being FinSequence of bool the carrier of (Segre_Product A) such that A25: F . 1 = product c3 and A26: F . (len F) = product c2 and A27: for i being Nat st i in dom F holds F . i is Segre-Coset of A and A28: for i being Nat st 1 <= i & i < len F holds for Di, Di1 being Segre-Coset of A st Di = F . i & Di1 = F . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) by A1, A9, Th22; A29: now__::_thesis:_not_len_F_=_1 dom c2 = I by PARTFUN1:def_2; then A30: c3 . j = {p} by FUNCT_7:31; assume len F = 1 ; ::_thesis: contradiction hence contradiction by A12, A15, A25, A26, A30, PUA2MSS1:2; ::_thesis: verum end; reconsider D = E ^' F as FinSequence of bool the carrier of (Segre_Product A) ; take D ; ::_thesis: ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) 1 in dom E by A21, FUNCT_1:def_2; then 1 <= len E by FINSEQ_3:25; hence D . 1 = product c1 by A21, GRAPH_2:14; ::_thesis: ( D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) A31: 1 in dom F by A25, FUNCT_1:def_2; then 1 <= len F by FINSEQ_3:25; then A32: len F > 1 by A29, XXREAL_0:1; hence D . (len D) = product c2 by A26, GRAPH_2:16; ::_thesis: ( ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) thus for i being Nat st i in dom D holds D . i is Segre-Coset of A ::_thesis: for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) proof let i be Nat; ::_thesis: ( i in dom D implies D . i is Segre-Coset of A ) A33: rng D c= (rng E) \/ (rng F) by GRAPH_2:17; assume i in dom D ; ::_thesis: D . i is Segre-Coset of A then A34: D . i in rng D by FUNCT_1:3; percases ( D . i in rng E or D . i in rng F ) by A34, A33, XBOOLE_0:def_3; suppose D . i in rng E ; ::_thesis: D . i is Segre-Coset of A then consider i0 being set such that A35: i0 in dom E and A36: D . i = E . i0 by FUNCT_1:def_3; thus D . i is Segre-Coset of A by A23, A35, A36; ::_thesis: verum end; suppose D . i in rng F ; ::_thesis: D . i is Segre-Coset of A then consider i0 being set such that A37: i0 in dom F and A38: D . i = F . i0 by FUNCT_1:def_3; thus D . i is Segre-Coset of A by A27, A37, A38; ::_thesis: verum end; end; end; thus for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ::_thesis: verum proof let i be Nat; ::_thesis: ( 1 <= i & i < len D implies for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) assume that A39: 1 <= i and A40: i < len D ; ::_thesis: for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) let Di, Di1 be Segre-Coset of A; ::_thesis: ( Di = D . i & Di1 = D . (i + 1) implies ( Di misses Di1 & Di '||' Di1 ) ) assume that A41: Di = D . i and A42: Di1 = D . (i + 1) ; ::_thesis: ( Di misses Di1 & Di '||' Di1 ) reconsider i = i as Element of NAT by ORDINAL1:def_12; percases ( i < len E or i >= len E ) ; supposeA43: i < len E ; ::_thesis: ( Di misses Di1 & Di '||' Di1 ) then i + 1 <= len E by NAT_1:13; then A44: Di1 = E . (i + 1) by A42, GRAPH_2:14, NAT_1:11; Di = E . i by A39, A41, A43, GRAPH_2:14; hence ( Di misses Di1 & Di '||' Di1 ) by A24, A39, A43, A44; ::_thesis: verum end; suppose i >= len E ; ::_thesis: ( Di misses Di1 & Di '||' Di1 ) then consider k being Nat such that A45: i = (len E) + k by NAT_1:10; A46: F <> {} by A31; reconsider k = k as Element of NAT by ORDINAL1:def_12; percases ( k > 0 or k = 0 ) ; supposeA47: k > 0 ; ::_thesis: ( Di misses Di1 & Di '||' Di1 ) ((len E) + k) + 1 < (len D) + 1 by A40, A45, XREAL_1:6; then A48: (len E) + (k + 1) < (len E) + (len F) by A46, GRAPH_2:13; then A49: k + 1 < len F by XREAL_1:6; then A50: k < len F by NAT_1:13; Di1 = D . ((len E) + (k + 1)) by A42, A45; then A51: Di1 = F . ((k + 1) + 1) by A49, GRAPH_2:15, NAT_1:11; 0 + 1 <= k by A47, NAT_1:13; then A52: Di = F . (k + 1) by A41, A45, A50, GRAPH_2:15; ( 1 <= k + 1 & k + 1 < len F ) by A48, NAT_1:11, XREAL_1:6; hence ( Di misses Di1 & Di '||' Di1 ) by A28, A52, A51; ::_thesis: verum end; suppose k = 0 ; ::_thesis: ( Di misses Di1 & Di '||' Di1 ) then ( Di = F . 1 & Di1 = F . (1 + 1) ) by A22, A25, A32, A39, A41, A42, A45, GRAPH_2:14, GRAPH_2:15; hence ( Di misses Di1 & Di '||' Di1 ) by A28, A32; ::_thesis: verum end; end; end; end; end; end; supposeA53: product c1 meets product c3 ; ::_thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) not p in c2 . j by A12, A15, A17, TARSKI:def_1; hence ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) by A1, A8, A9, A18, A19, A53, Th11, Th22; ::_thesis: verum end; end; end; end; A54: S1[ 0 ] proof let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( indx c1 = indx c2 & product c1 is Segre-Coset of A & product c2 is Segre-Coset of A & product c1 misses product c2 & diff (c1,c2) = 0 implies ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) ) assume that indx c1 = indx c2 and product c1 is Segre-Coset of A and product c2 is Segre-Coset of A and A55: product c1 misses product c2 and A56: diff (c1,c2) = 0 ; ::_thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) A57: now__::_thesis:_for_a_being_set_st_a_in_dom_c1_holds_ not_c1_._a_<>_c2_._a let a be set ; ::_thesis: ( a in dom c1 implies not c1 . a <> c2 . a ) assume a in dom c1 ; ::_thesis: not c1 . a <> c2 . a then reconsider j = a as Element of I ; assume c1 . a <> c2 . a ; ::_thesis: contradiction then j in { i where i is Element of I : c1 . i <> c2 . i } ; hence contradiction by A56; ::_thesis: verum end; dom c1 = I by PARTFUN1:def_2 .= dom c2 by PARTFUN1:def_2 ; hence ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = product c1 & D . (len D) = product c2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) by A55, A57, FUNCT_1:2; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A54, A5); then A58: S1[ diff (b1,b2)] ; assume indx b1 = indx b2 ; ::_thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) then consider D being FinSequence of bool the carrier of (Segre_Product A) such that A59: ( D . 1 = product b1 & D . (len D) = product b2 ) and A60: ( ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) by A2, A3, A4, A58; take D ; ::_thesis: ( D . 1 = B1 & D . (len D) = B2 & ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) thus ( D . 1 = B1 & D . (len D) = B2 ) by A3, A4, A59; ::_thesis: ( ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) thus ( ( for i being Nat st i in dom D holds D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ) ) by A60; ::_thesis: verum end; given D being FinSequence of bool the carrier of (Segre_Product A) such that A61: D . 1 = B1 and A62: D . (len D) = B2 and A63: for i being Nat st i in dom D holds D . i is Segre-Coset of A and A64: for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) ; ::_thesis: indx b1 = indx b2 defpred S1[ Nat] means for bb being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product bb = D . $1 holds indx b1 = indx bb; A65: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A66: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product bb = D . (k + 1) implies indx b1 = indx bb ) assume A67: product bb = D . (k + 1) ; ::_thesis: indx b1 = indx bb A68: k + 1 in dom D by A67, FUNCT_1:def_2; then A69: k + 1 <= len D by FINSEQ_3:25; percases ( k = 0 or 0 < k ) ; suppose k = 0 ; ::_thesis: indx b1 = indx bb hence indx b1 = indx bb by A3, A61, A67, PUA2MSS1:2; ::_thesis: verum end; suppose 0 < k ; ::_thesis: indx b1 = indx bb then 0 + 1 < k + 1 by XREAL_1:6; then A70: 1 <= k by NAT_1:13; k <= len D by A69, NAT_1:13; then k in dom D by A70, FINSEQ_3:25; then reconsider B0 = D . k as Segre-Coset of A by A63; reconsider B3 = D . (k + 1) as Segre-Coset of A by A63, A68; consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A71: B0 = product b0 and b0 . (indx b0) = [#] (A . (indx b0)) by PENCIL_2:def_2; k < len D by A69, NAT_1:13; then A72: ( B0 misses B3 & B0 '||' B3 ) by A64, A70; indx b1 = indx b0 by A66, A71; hence indx b1 = indx bb by A67, A71, A72, Th21; ::_thesis: verum end; end; end; end; A73: S1[ 0 ] proof A74: not 0 in dom D by FINSEQ_3:24; let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product bb = D . 0 implies indx b1 = indx bb ) assume product bb = D . 0 ; ::_thesis: indx b1 = indx bb hence indx b1 = indx bb by A74, FUNCT_1:def_2; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A73, A65); hence indx b1 = indx b2 by A4, A62; ::_thesis: verum end; theorem Th24: :: PENCIL_3:24 for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for B1, B2 being Segre-Coset of A for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds indx b3 = indx b4 proof let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for B1, B2 being Segre-Coset of A for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds indx b3 = indx b4 let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) for B1, B2 being Segre-Coset of A for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds indx b3 = indx b4 ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A) for B1, B2 being Segre-Coset of A for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds indx b3 = indx b4 A2: now__::_thesis:_for_i_being_Element_of_I_holds_A_._i_is_connected let i be Element of I; ::_thesis: A . i is connected A . i is strongly_connected by A1; hence A . i is connected by Th4; ::_thesis: verum end; let f be Collineation of (Segre_Product A); ::_thesis: for B1, B2 being Segre-Coset of A for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds indx b3 = indx b4 let B1, B2 be Segre-Coset of A; ::_thesis: for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds indx b3 = indx b4 let b1, b2, b3, b4 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 implies indx b3 = indx b4 ) assume that A3: B1 = product b1 and A4: B2 = product b2 and A5: ( f .: B1 = product b3 & f .: B2 = product b4 ) ; ::_thesis: ( not indx b1 = indx b2 or indx b3 = indx b4 ) assume A6: indx b1 = indx b2 ; ::_thesis: indx b3 = indx b4 percases ( B1 misses B2 or B1 meets B2 ) ; supposeA7: B1 misses B2 ; ::_thesis: indx b3 = indx b4 reconsider fB1 = f .: B1, fB2 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24; f is bijective Function of the carrier of (Segre_Product A), the carrier of (Segre_Product A) by PENCIL_2:def_4; then A8: fB1 misses fB2 by A7, FUNCT_1:66; consider D being FinSequence of bool the carrier of (Segre_Product A) such that A9: D . 1 = B1 and A10: D . (len D) = B2 and A11: for i being Nat st i in dom D holds D . i is Segre-Coset of A and A12: for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) by A2, A3, A4, A6, A7, Th23; deffunc H1( Nat) -> Element of bool the carrier of (Segre_Product A) = f .: (D . $1); consider E being FinSequence of bool the carrier of (Segre_Product A) such that A13: ( len E = len D & ( for j being Nat st j in dom E holds E . j = H1(j) ) ) from FINSEQ_2:sch_1(); A14: dom E = Seg (len D) by A13, FINSEQ_1:def_3; A15: for i being Nat st 1 <= i & i < len E holds for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds ( Ei misses Ei1 & Ei '||' Ei1 ) proof let i be Nat; ::_thesis: ( 1 <= i & i < len E implies for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds ( Ei misses Ei1 & Ei '||' Ei1 ) ) A16: f is bijective Function of the carrier of (Segre_Product A), the carrier of (Segre_Product A) by PENCIL_2:def_4; assume A17: ( 1 <= i & i < len E ) ; ::_thesis: for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds ( Ei misses Ei1 & Ei '||' Ei1 ) then i in dom D by A13, FINSEQ_3:25; then reconsider Di = D . i as Segre-Coset of A by A11; ( 1 <= i + 1 & i + 1 <= len E ) by A17, NAT_1:13; then i + 1 in dom D by A13, FINSEQ_3:25; then reconsider Di1 = D . (i + 1) as Segre-Coset of A by A11; let Ei, Ei1 be Segre-Coset of A; ::_thesis: ( Ei = E . i & Ei1 = E . (i + 1) implies ( Ei misses Ei1 & Ei '||' Ei1 ) ) assume that A18: Ei = E . i and A19: Ei1 = E . (i + 1) ; ::_thesis: ( Ei misses Ei1 & Ei '||' Ei1 ) i in Seg (len D) by A13, A17, FINSEQ_1:1; then A20: Ei = f .: (D . i) by A13, A14, A18; ( 1 <= i + 1 & i + 1 <= len E ) by A17, NAT_1:13; then i + 1 in Seg (len D) by A13, FINSEQ_1:1; then A21: Ei1 = f .: (D . (i + 1)) by A13, A14, A19; Di misses Di1 by A12, A13, A17; hence Ei misses Ei1 by A20, A21, A16, FUNCT_1:66; ::_thesis: Ei '||' Ei1 Di '||' Di1 by A12, A13, A17; hence Ei '||' Ei1 by A20, A21, Th20; ::_thesis: verum end; A22: for i being Nat st i in dom E holds E . i is Segre-Coset of A proof let i be Nat; ::_thesis: ( i in dom E implies E . i is Segre-Coset of A ) assume A23: i in dom E ; ::_thesis: E . i is Segre-Coset of A then i in Seg (len D) by A13, FINSEQ_1:def_3; then i in dom D by FINSEQ_1:def_3; then reconsider di = D . i as Segre-Coset of A by A11; E . i = f .: di by A13, A23; hence E . i is Segre-Coset of A by A1, PENCIL_2:24; ::_thesis: verum end; len E in dom D by A4, A10, A13, FUNCT_1:def_2; then len E in Seg (len D) by FINSEQ_1:def_3; then A24: E . (len E) = f .: B2 by A10, A13, A14; 1 in dom D by A3, A9, FUNCT_1:def_2; then 1 in Seg (len D) by FINSEQ_1:def_3; then E . 1 = f .: B1 by A9, A13, A14; hence indx b3 = indx b4 by A2, A5, A24, A22, A15, A8, Th23; ::_thesis: verum end; suppose B1 meets B2 ; ::_thesis: indx b3 = indx b4 then B1 = B2 by A3, A4, A6, Th11; hence indx b3 = indx b4 by A5, PUA2MSS1:2; ::_thesis: verum end; end; end; theorem Th25: :: PENCIL_3:25 for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) ex s being Permutation of I st for i, j being Element of I holds ( s . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) proof let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) ex s being Permutation of I st for i, j being Element of I holds ( s . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) ex s being Permutation of I st for i, j being Element of I holds ( s . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A) ex s being Permutation of I st for i, j being Element of I holds ( s . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) let f be Collineation of (Segre_Product A); ::_thesis: ex s being Permutation of I st for i, j being Element of I holds ( s . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) defpred S1[ set , set ] means for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = $1 holds indx b2 = $2; A2: for x, y, x9 being Element of I st S1[x,y] & S1[x9,y] holds x = x9 proof reconsider ff = f " as Collineation of (Segre_Product A) by PENCIL_2:13; let x, y, x9 be Element of I; ::_thesis: ( S1[x,y] & S1[x9,y] implies x = x9 ) assume that A3: for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds indx b2 = y and A4: for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x9 holds indx b2 = y ; ::_thesis: x = x9 consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A5: indx b1 = x and A6: product b1 is Segre-Coset of A by Th8; reconsider B1 = product b1 as Segre-Coset of A by A6; reconsider fB1 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24; consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A7: fB1 = product L1 and L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def_2; consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A8: indx b2 = x9 and A9: product b2 is Segre-Coset of A by Th8; reconsider B2 = product b2 as Segre-Coset of A by A9; reconsider fB2 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24; consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A10: fB2 = product L2 and L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def_2; A11: indx L2 = y by A4, A8, A10; A12: f is bijective by PENCIL_2:def_4; A13: ff = f " by A12, TOPS_2:def_4; then A14: ff .: fB2 = f " fB2 by A12, FUNCT_1:85; A15: ff .: fB1 = f " fB1 by A12, A13, FUNCT_1:85; dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1; then A16: B2 c= ff .: fB2 by A14, FUNCT_1:76; ff .: fB2 c= B2 by A12, A14, FUNCT_1:82; then A17: B2 = ff .: fB2 by A16, XBOOLE_0:def_10; dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1; then A18: B1 c= ff .: fB1 by A15, FUNCT_1:76; ff .: fB1 c= B1 by A12, A15, FUNCT_1:82; then A19: B1 = ff .: fB1 by A18, XBOOLE_0:def_10; indx L1 = y by A3, A5, A7; hence x = x9 by A1, A5, A7, A8, A10, A11, A19, A17, Th24; ::_thesis: verum end; A20: for y being Element of I ex x being Element of I st S1[x,y] proof set p0 = the Point of (Segre_Product A); reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6; let x be Element of I; ::_thesis: ex x being Element of I st S1[x,x] reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11; dom A = I by PARTFUN1:def_2; then A . x in rng A by FUNCT_1:3; then not A . x is trivial by PENCIL_1:def_18; then reconsider C = [#] (A . x) as non trivial set ; reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7; dom p = I by PARTFUN1:def_2; then A21: b . x = C by FUNCT_7:31; then A22: indx b = x by PENCIL_1:def_21; product b c= the carrier of (Segre_Product A) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product b or a in the carrier of (Segre_Product A) ) assume a in product b ; ::_thesis: a in the carrier of (Segre_Product A) then consider f being Function such that A23: a = f and A24: dom f = dom b and A25: for x being set st x in dom b holds f . x in b . x by CARD_3:def_5; dom (Carrier A) = I by PARTFUN1:def_2; then A26: dom f = dom (Carrier A) by A24, PARTFUN1:def_2; A27: now__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_ f_._i_in_(Carrier_A)_._i let i be set ; ::_thesis: ( i in dom (Carrier A) implies f . b1 in (Carrier A) . b1 ) assume A28: i in dom (Carrier A) ; ::_thesis: f . b1 in (Carrier A) . b1 then reconsider i1 = i as Element of I ; A29: f . i in b . i by A24, A25, A26, A28; percases ( i1 = x or i1 <> x ) ; suppose i1 = x ; ::_thesis: f . b1 in (Carrier A) . b1 hence f . i in (Carrier A) . i by A21, A29, Th7; ::_thesis: verum end; suppose i1 <> x ; ::_thesis: f . b1 in (Carrier A) . b1 then f . i1 in p . i1 by A29, FUNCT_7:32; then f . i1 in {(p0 . i1)} by PZFMISC1:def_1; then f . i1 = p0 . i1 by TARSKI:def_1; then A30: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def_14; not [#] (A . i1) is empty ; then not (Carrier A) . i1 is empty by Th7; hence f . i in (Carrier A) . i by A30; ::_thesis: verum end; end; end; Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23; hence a in the carrier of (Segre_Product A) by A23, A26, A27, CARD_3:def_5; ::_thesis: verum end; then reconsider B = product b as Segre-Coset of A by A21, A22, PENCIL_2:def_2; reconsider fB = f " B as Segre-Coset of A by A1, PENCIL_2:25; consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A31: fB = product b0 and b0 . (indx b0) = [#] (A . (indx b0)) by PENCIL_2:def_2; take y = indx b0; ::_thesis: S1[y,x] let B1 be Segre-Coset of A; ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = y holds indx b2 = x let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y implies indx b2 = x ) f is bijective by PENCIL_2:def_4; then rng f = the carrier of (Segre_Product A) by FUNCT_2:def_3; then A32: f .: fB = product b by FUNCT_1:77; assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y ) ; ::_thesis: indx b2 = x hence indx b2 = x by A1, A22, A31, A32, Th24; ::_thesis: verum end; A33: for x being Element of I ex y being Element of I st S1[x,y] proof set p0 = the Point of (Segre_Product A); reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6; let x be Element of I; ::_thesis: ex y being Element of I st S1[x,y] reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11; dom A = I by PARTFUN1:def_2; then A . x in rng A by FUNCT_1:3; then not A . x is trivial by PENCIL_1:def_18; then reconsider C = [#] (A . x) as non trivial set ; reconsider b = p +* (x,C) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7; dom p = I by PARTFUN1:def_2; then A34: b . x = C by FUNCT_7:31; then A35: indx b = x by PENCIL_1:def_21; product b c= the carrier of (Segre_Product A) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product b or a in the carrier of (Segre_Product A) ) assume a in product b ; ::_thesis: a in the carrier of (Segre_Product A) then consider f being Function such that A36: a = f and A37: dom f = dom b and A38: for x being set st x in dom b holds f . x in b . x by CARD_3:def_5; dom (Carrier A) = I by PARTFUN1:def_2; then A39: dom f = dom (Carrier A) by A37, PARTFUN1:def_2; A40: now__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_A)_holds_ f_._i_in_(Carrier_A)_._i let i be set ; ::_thesis: ( i in dom (Carrier A) implies f . b1 in (Carrier A) . b1 ) assume A41: i in dom (Carrier A) ; ::_thesis: f . b1 in (Carrier A) . b1 then reconsider i1 = i as Element of I ; A42: f . i in b . i by A37, A38, A39, A41; percases ( i1 = x or i1 <> x ) ; suppose i1 = x ; ::_thesis: f . b1 in (Carrier A) . b1 hence f . i in (Carrier A) . i by A34, A42, Th7; ::_thesis: verum end; suppose i1 <> x ; ::_thesis: f . b1 in (Carrier A) . b1 then f . i1 in p . i1 by A42, FUNCT_7:32; then f . i1 in {(p0 . i1)} by PZFMISC1:def_1; then f . i1 = p0 . i1 by TARSKI:def_1; then A43: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def_14; not [#] (A . i1) is empty ; then not (Carrier A) . i1 is empty by Th7; hence f . i in (Carrier A) . i by A43; ::_thesis: verum end; end; end; Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23; hence a in the carrier of (Segre_Product A) by A36, A39, A40, CARD_3:def_5; ::_thesis: verum end; then reconsider B = product b as Segre-Coset of A by A34, A35, PENCIL_2:def_2; reconsider fB = f .: B as Segre-Coset of A by A1, PENCIL_2:24; consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A44: fB = product b0 and b0 . (indx b0) = [#] (A . (indx b0)) by PENCIL_2:def_2; take indx b0 ; ::_thesis: S1[x, indx b0] let B1 be Segre-Coset of A; ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds indx b2 = indx b0 let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x implies indx b2 = indx b0 ) assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x ) ; ::_thesis: indx b2 = indx b0 hence indx b2 = indx b0 by A1, A35, A44, Th24; ::_thesis: verum end; A45: for x, y, y9 being Element of I st S1[x,y] & S1[x,y9] holds y = y9 proof let x, y, y9 be Element of I; ::_thesis: ( S1[x,y] & S1[x,y9] implies y = y9 ) assume that A46: for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds indx b2 = y and A47: for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = x holds indx b2 = y9 ; ::_thesis: y = y9 consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A48: indx b1 = x and A49: product b1 is Segre-Coset of A by Th8; reconsider B1 = product b1 as Segre-Coset of A by A49; reconsider fB1 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24; consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A50: fB1 = product L1 and L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def_2; indx L1 = y by A46, A48, A50; hence y = y9 by A47, A48, A50; ::_thesis: verum end; thus ex f being Permutation of I st for x, y being Element of I holds ( f . x = y iff S1[x,y] ) from TRANSGEO:sch_1(A33, A20, A2, A45); ::_thesis: verum end; definition let I be non empty finite set ; let A be PLS-yielding ManySortedSet of I; assume B1: for i being Element of I holds A . i is strongly_connected ; let f be Collineation of (Segre_Product A); func permutation_of_indices f -> Permutation of I means :Def3: :: PENCIL_3:def 3 for i, j being Element of I holds ( it . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ); existence ex b1 being Permutation of I st for i, j being Element of I holds ( b1 . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) by B1, Th25; uniqueness for b1, b2 being Permutation of I st ( for i, j being Element of I holds ( b1 . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) ) & ( for i, j being Element of I holds ( b2 . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) ) holds b1 = b2 proof let s, t be Permutation of I; ::_thesis: ( ( for i, j being Element of I holds ( s . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) ) & ( for i, j being Element of I holds ( t . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) ) implies s = t ) assume that A1: for i, j being Element of I holds ( s . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) and A2: for i, j being Element of I holds ( t . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) ; ::_thesis: s = t A3: now__::_thesis:_for_a_being_set_st_a_in_I_holds_ s_._a_=_t_._a let a be set ; ::_thesis: ( a in I implies s . a = t . a ) assume a in I ; ::_thesis: s . a = t . a then reconsider i = a as Element of I ; reconsider j2 = t . i as Element of I ; reconsider j1 = s . i as Element of I ; consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A4: indx b1 = i and A5: product b1 is Segre-Coset of A by Th8; reconsider B1 = product b1 as Segre-Coset of A by A5; reconsider fB = f .: B1 as Segre-Coset of A by B1, PENCIL_2:24; consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A6: fB = product b2 and b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def_2; j1 = indx b2 by A1, A4, A6 .= j2 by A2, A4, A6 ; hence s . a = t . a ; ::_thesis: verum end; ( dom s = I & dom t = I ) by FUNCT_2:def_1; hence s = t by A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines permutation_of_indices PENCIL_3:def_3_:_ for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for b4 being Permutation of I holds ( b4 = permutation_of_indices f iff for i, j being Element of I holds ( b4 . i = j iff for B1 being Segre-Coset of A for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds indx b2 = j ) ); begin definition let I be non empty finite set ; let A be PLS-yielding ManySortedSet of I; assume B1: for i being Element of I holds A . i is strongly_connected ; let f be Collineation of (Segre_Product A); let b1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; assume B2: product b1 is Segre-Coset of A ; func canonical_embedding (f,b1) -> Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) means :Def4: :: PENCIL_3:def 4 ( it is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = it . (a . (indx b1)) ) ); existence ex b1 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st ( b1 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = b1 . (a . (indx b1)) ) ) proof reconsider B1 = product b1 as Segre-Coset of A by B2; set s = permutation_of_indices f; set i = indx b1; defpred S1[ set , set ] means for J being ManySortedSet of I st J in f .: (product (b1 +* ((indx b1),{$1}))) holds $2 = J . ((permutation_of_indices f) . (indx b1)); set B = the carrier of (A . (indx b1)); set t = permutation_of_indices f; reconsider B2 = f .: B1 as Segre-Coset of A by B1, PENCIL_2:24; consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A1: product b2 = B2 and A2: b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def_2; set j = indx b2; A3: f is bijective by PENCIL_2:def_4; then A4: f " B2 c= B1 by FUNCT_1:82; A5: Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def_23; A6: for x being set st x in the carrier of (A . (indx b1)) holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier of (A . (indx b1)) implies ex y being set st S1[x,y] ) consider bb being set such that A7: bb in B1 by XBOOLE_0:def_1; A8: ex bf being Function st ( bf = bb & dom bf = dom b1 & ( for o being set st o in dom b1 holds bf . o in b1 . o ) ) by A7, CARD_3:def_5; A9: dom b1 = I by PARTFUN1:def_2; then reconsider bb = bb as ManySortedSet of I by A8, PARTFUN1:def_2, RELAT_1:def_18; set bbx = bb +* ((indx b1),x); A10: {(bb +* ((indx b1),x))} = product (b1 +* ((indx b1),{x})) proof thus {(bb +* ((indx b1),x))} c= product (b1 +* ((indx b1),{x})) :: according to XBOOLE_0:def_10 ::_thesis: product (b1 +* ((indx b1),{x})) c= {(bb +* ((indx b1),x))} proof A11: now__::_thesis:_for_z_being_set_st_z_in_dom_(b1_+*_((indx_b1),{x}))_holds_ (bb_+*_((indx_b1),x))_._z_in_(b1_+*_((indx_b1),{x}))_._z let z be set ; ::_thesis: ( z in dom (b1 +* ((indx b1),{x})) implies (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 ) assume z in dom (b1 +* ((indx b1),{x})) ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 then A12: z in I ; then A13: z in dom bb by PARTFUN1:def_2; percases ( z = indx b1 or z <> indx b1 ) ; supposeA14: z = indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 then (bb +* ((indx b1),x)) . z = x by A13, FUNCT_7:31; then (bb +* ((indx b1),x)) . z in {x} by TARSKI:def_1; hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A9, A14, FUNCT_7:31; ::_thesis: verum end; supposeA15: z <> indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (b1 +* ((indx b1),{x})) . b1 then (bb +* ((indx b1),x)) . z = bb . z by FUNCT_7:32; then (bb +* ((indx b1),x)) . z in b1 . z by A7, A9, A12, CARD_3:9; hence (bb +* ((indx b1),x)) . z in (b1 +* ((indx b1),{x})) . z by A15, FUNCT_7:32; ::_thesis: verum end; end; end; let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in {(bb +* ((indx b1),x))} or o in product (b1 +* ((indx b1),{x})) ) assume o in {(bb +* ((indx b1),x))} ; ::_thesis: o in product (b1 +* ((indx b1),{x})) then A16: o = bb +* ((indx b1),x) by TARSKI:def_1; dom (bb +* ((indx b1),x)) = I by PARTFUN1:def_2 .= dom (b1 +* ((indx b1),{x})) by PARTFUN1:def_2 ; hence o in product (b1 +* ((indx b1),{x})) by A16, A11, CARD_3:9; ::_thesis: verum end; let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in product (b1 +* ((indx b1),{x})) or o in {(bb +* ((indx b1),x))} ) assume o in product (b1 +* ((indx b1),{x})) ; ::_thesis: o in {(bb +* ((indx b1),x))} then consider u being Function such that A17: u = o and A18: dom u = dom (b1 +* ((indx b1),{x})) and A19: for z being set st z in dom (b1 +* ((indx b1),{x})) holds u . z in (b1 +* ((indx b1),{x})) . z by CARD_3:def_5; A20: now__::_thesis:_for_z_being_set_st_z_in_dom_u_holds_ u_._z_=_(bb_+*_((indx_b1),x))_._z let z be set ; ::_thesis: ( z in dom u implies u . b1 = (bb +* ((indx b1),x)) . b1 ) assume A21: z in dom u ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1 then A22: z in I by A18; reconsider zz = z as Element of I by A18, A21; A23: u . z in (b1 +* ((indx b1),{x})) . z by A18, A19, A21; percases ( zz = indx b1 or zz <> indx b1 ) ; supposeA24: zz = indx b1 ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1 then u . z in {x} by A9, A23, FUNCT_7:31; then u . z = x by TARSKI:def_1; hence u . z = (bb +* ((indx b1),x)) . z by A8, A9, A24, FUNCT_7:31; ::_thesis: verum end; supposeA25: zz <> indx b1 ; ::_thesis: u . b1 = (bb +* ((indx b1),x)) . b1 then ( not b1 . zz is empty & b1 . zz is trivial ) by PENCIL_1:def_21; then b1 . zz is 1 -element ; then consider o being set such that A26: b1 . z = {o} by ZFMISC_1:131; u . z in b1 . z by A23, A25, FUNCT_7:32; then A27: u . z = o by A26, TARSKI:def_1; (bb +* ((indx b1),x)) . z = bb . z by A25, FUNCT_7:32; then (bb +* ((indx b1),x)) . z in {o} by A8, A9, A22, A26; hence u . z = (bb +* ((indx b1),x)) . z by A27, TARSKI:def_1; ::_thesis: verum end; end; end; dom u = I by A18, PARTFUN1:def_2 .= dom (bb +* ((indx b1),x)) by PARTFUN1:def_2 ; then u = bb +* ((indx b1),x) by A20, FUNCT_1:2; hence o in {(bb +* ((indx b1),x))} by A17, TARSKI:def_1; ::_thesis: verum end; assume A28: x in the carrier of (A . (indx b1)) ; ::_thesis: ex y being set st S1[x,y] A29: now__::_thesis:_for_o_being_set_st_o_in_dom_(Carrier_A)_holds_ (bb_+*_((indx_b1),x))_._o_in_(Carrier_A)_._o let o be set ; ::_thesis: ( o in dom (Carrier A) implies (bb +* ((indx b1),x)) . b1 in (Carrier A) . b1 ) assume A30: o in dom (Carrier A) ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (Carrier A) . b1 then reconsider u = o as Element of I ; percases ( u = indx b1 or u <> indx b1 ) ; supposeA31: u = indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (Carrier A) . b1 then (bb +* ((indx b1),x)) . u in [#] (A . (indx b1)) by A28, A8, A9, FUNCT_7:31; hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A31, Th7; ::_thesis: verum end; supposeA32: u <> indx b1 ; ::_thesis: (bb +* ((indx b1),x)) . b1 in (Carrier A) . b1 b1 c= Carrier A by PBOOLE:def_18; then A33: b1 . o c= (Carrier A) . o by A30, PBOOLE:def_2; (bb +* ((indx b1),x)) . u = bb . u by A32, FUNCT_7:32; then (bb +* ((indx b1),x)) . u in b1 . u by A7, A9, CARD_3:9; hence (bb +* ((indx b1),x)) . o in (Carrier A) . o by A33; ::_thesis: verum end; end; end; dom (bb +* ((indx b1),x)) = I by PARTFUN1:def_2 .= dom (Carrier A) by PARTFUN1:def_2 ; then reconsider bbx1 = bb +* ((indx b1),x) as Point of (Segre_Product A) by A5, A29, CARD_3:9; reconsider fbbx = f . bbx1 as ManySortedSet of I by PENCIL_1:14; take fbbx . ((permutation_of_indices f) . (indx b1)) ; ::_thesis: S1[x,fbbx . ((permutation_of_indices f) . (indx b1))] dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1; then bbx1 in dom f ; then A34: Im (f,(bb +* ((indx b1),x))) = {(f . (bb +* ((indx b1),x)))} by FUNCT_1:59; let J be ManySortedSet of I; ::_thesis: ( J in f .: (product (b1 +* ((indx b1),{x}))) implies fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1)) ) assume J in f .: (product (b1 +* ((indx b1),{x}))) ; ::_thesis: fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1)) hence fbbx . ((permutation_of_indices f) . (indx b1)) = J . ((permutation_of_indices f) . (indx b1)) by A10, A34, TARSKI:def_1; ::_thesis: verum end; consider M being Function such that A35: ( dom M = the carrier of (A . (indx b1)) & ( for x being set st x in the carrier of (A . (indx b1)) holds S1[x,M . x] ) ) from CLASSES1:sch_1(A6); A36: dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1; then B1 c= f " B2 by FUNCT_1:76; then A37: f " B2 = B1 by A4, XBOOLE_0:def_10; rng M c= the carrier of (A . ((permutation_of_indices f) . (indx b1))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng M or x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ) assume x in rng M ; ::_thesis: x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) then consider o being set such that A38: o in dom M and A39: x = M . o by FUNCT_1:def_3; reconsider o = o as Point of (A . (indx b1)) by A35, A38; consider p being ManySortedSet of I such that A40: p in product b1 and A41: {(p +* ((indx b1),o))} = product (b1 +* ((indx b1),{o})) by Th18; reconsider pio = p +* ((indx b1),o) as Point of (Segre_Product A) by B2, A40, PENCIL_1:25; reconsider J = f . pio as ManySortedSet of I by PENCIL_1:14; Im (f,(p +* ((indx b1),o))) = {(f . pio)} by A36, FUNCT_1:59; then A42: J in f .: (product (b1 +* ((indx b1),{o}))) by A41, TARSKI:def_1; (permutation_of_indices f) . (indx b1) in I ; then (permutation_of_indices f) . (indx b1) in dom (Carrier A) by PARTFUN1:def_2; then J . ((permutation_of_indices f) . (indx b1)) in (Carrier A) . ((permutation_of_indices f) . (indx b1)) by A5, CARD_3:9; then J . ((permutation_of_indices f) . (indx b1)) in [#] (A . ((permutation_of_indices f) . (indx b1))) by Th7; hence x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) by A35, A39, A42; ::_thesis: verum end; then reconsider M = M as Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) by A35, FUNCT_2:def_1, RELSET_1:4; set m = M; A43: indx b2 = (permutation_of_indices f) . (indx b1) by B1, A1, Def3; A44: M is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom M or not x2 in dom M or not M . x1 = M . x2 or x1 = x2 ) assume that A45: ( x1 in dom M & x2 in dom M ) and A46: M . x1 = M . x2 ; ::_thesis: x1 = x2 reconsider o1 = x1, o2 = x2 as Point of (A . (indx b1)) by A45; consider p1 being ManySortedSet of I such that A47: p1 in product b1 and A48: {(p1 +* ((indx b1),o1))} = product (b1 +* ((indx b1),{o1})) by Th18; reconsider p1io = p1 +* ((indx b1),o1) as Point of (Segre_Product A) by B2, A47, PENCIL_1:25; reconsider J1 = f . p1io as ManySortedSet of I by PENCIL_1:14; consider p2 being ManySortedSet of I such that A49: p2 in product b1 and A50: {(p2 +* ((indx b1),o2))} = product (b1 +* ((indx b1),{o2})) by Th18; A51: dom b1 = I by PARTFUN1:def_2; A52: dom p1 = I by PARTFUN1:def_2; A53: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ (p1_+*_((indx_b1),o1))_._o_in_b1_._o let o be set ; ::_thesis: ( o in I implies (p1 +* ((indx b1),o1)) . b1 in b1 . b1 ) assume A54: o in I ; ::_thesis: (p1 +* ((indx b1),o1)) . b1 in b1 . b1 percases ( o = indx b1 or o <> indx b1 ) ; supposeA55: o = indx b1 ; ::_thesis: (p1 +* ((indx b1),o1)) . b1 in b1 . b1 then (p1 +* ((indx b1),o1)) . o = o1 by A52, FUNCT_7:31; then (p1 +* ((indx b1),o1)) . o in [#] (A . (indx b1)) ; hence (p1 +* ((indx b1),o1)) . o in b1 . o by B2, A55, Th10; ::_thesis: verum end; suppose o <> indx b1 ; ::_thesis: (p1 +* ((indx b1),o1)) . b1 in b1 . b1 then (p1 +* ((indx b1),o1)) . o = p1 . o by FUNCT_7:32; hence (p1 +* ((indx b1),o1)) . o in b1 . o by A47, A51, A54, CARD_3:9; ::_thesis: verum end; end; end; dom (p1 +* ((indx b1),o1)) = I by PARTFUN1:def_2; then p1io in product b1 by A51, A53, CARD_3:9; then A56: J1 in B2 by A36, FUNCT_1:def_6; reconsider p2io = p2 +* ((indx b1),o2) as Point of (Segre_Product A) by B2, A49, PENCIL_1:25; reconsider J2 = f . p2io as ManySortedSet of I by PENCIL_1:14; Im (f,(p2 +* ((indx b1),o2))) = {(f . p2io)} by A36, FUNCT_1:59; then J2 in f .: (product (b1 +* ((indx b1),{o2}))) by A50, TARSKI:def_1; then A57: M . o2 = J2 . ((permutation_of_indices f) . (indx b1)) by A35; dom p1 = I by PARTFUN1:def_2; then A58: (p1 +* ((indx b1),o1)) . (indx b1) = o1 by FUNCT_7:31; A59: dom b1 = I by PARTFUN1:def_2; A60: dom p2 = I by PARTFUN1:def_2; A61: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ (p2_+*_((indx_b1),o2))_._o_in_b1_._o let o be set ; ::_thesis: ( o in I implies (p2 +* ((indx b1),o2)) . b1 in b1 . b1 ) assume A62: o in I ; ::_thesis: (p2 +* ((indx b1),o2)) . b1 in b1 . b1 percases ( o = indx b1 or o <> indx b1 ) ; supposeA63: o = indx b1 ; ::_thesis: (p2 +* ((indx b1),o2)) . b1 in b1 . b1 then (p2 +* ((indx b1),o2)) . o = o2 by A60, FUNCT_7:31; then (p2 +* ((indx b1),o2)) . o in [#] (A . (indx b1)) ; hence (p2 +* ((indx b1),o2)) . o in b1 . o by B2, A63, Th10; ::_thesis: verum end; suppose o <> indx b1 ; ::_thesis: (p2 +* ((indx b1),o2)) . b1 in b1 . b1 then (p2 +* ((indx b1),o2)) . o = p2 . o by FUNCT_7:32; hence (p2 +* ((indx b1),o2)) . o in b1 . o by A49, A59, A62, CARD_3:9; ::_thesis: verum end; end; end; dom (p2 +* ((indx b1),o2)) = I by PARTFUN1:def_2; then p2io in product b1 by A59, A61, CARD_3:9; then A64: J2 in B2 by A36, FUNCT_1:def_6; Im (f,(p1 +* ((indx b1),o1))) = {(f . p1io)} by A36, FUNCT_1:59; then A65: J1 in f .: (product (b1 +* ((indx b1),{o1}))) by A48, TARSKI:def_1; A66: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ J1_._o_=_J2_._o let o be set ; ::_thesis: ( o in I implies J1 . b1 = J2 . b1 ) assume o in I ; ::_thesis: J1 . b1 = J2 . b1 then reconsider l = o as Element of I ; percases ( l = indx b2 or l <> indx b2 ) ; suppose l = indx b2 ; ::_thesis: J1 . b1 = J2 . b1 hence J1 . o = J2 . o by A43, A35, A46, A65, A57; ::_thesis: verum end; suppose l <> indx b2 ; ::_thesis: J1 . b1 = J2 . b1 hence J1 . o = J2 . o by A1, A56, A64, PENCIL_1:23; ::_thesis: verum end; end; end; dom p2 = I by PARTFUN1:def_2; then A67: (p2 +* ((indx b1),o2)) . (indx b1) = o2 by FUNCT_7:31; ( dom J1 = I & dom J2 = I ) by PARTFUN1:def_2; then J1 = J2 by A66, FUNCT_1:2; hence x1 = x2 by A36, A3, A58, A67, FUNCT_1:def_4; ::_thesis: verum end; f is bijective by PENCIL_2:def_4; then A68: rng f = the carrier of (Segre_Product A) by FUNCT_2:def_3; A69: f " = f " by A3, TOPS_2:def_4; the carrier of (A . ((permutation_of_indices f) . (indx b1))) c= rng M proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) or x in rng M ) assume x in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ; ::_thesis: x in rng M then reconsider x1 = x as Point of (A . ((permutation_of_indices f) . (indx b1))) ; consider p0 being ManySortedSet of I such that A70: p0 in product b2 and {(p0 +* ((indx b2),x1))} = product (b2 +* ((indx b2),{x1})) by A43, Th18; reconsider p = p0 +* ((indx b2),x1) as Point of (Segre_Product A) by A1, A43, A70, PENCIL_1:25; reconsider p1 = p as ManySortedSet of I ; reconsider q = (f ") . p as ManySortedSet of I by PENCIL_1:14; A71: p = f . ((f ") . p) by A68, A3, A69, FUNCT_1:35; A72: dom b1 = I by PARTFUN1:def_2; A73: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ q_._o_in_(b1_+*_((indx_b1),{(q_._(indx_b1))}))_._o let o be set ; ::_thesis: ( o in I implies q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1 ) assume o in I ; ::_thesis: q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1 then reconsider l = o as Element of I ; percases ( l = indx b1 or l <> indx b1 ) ; suppose l = indx b1 ; ::_thesis: q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1 then (b1 +* ((indx b1),{(q . (indx b1))})) . l = {(q . o)} by A72, FUNCT_7:31; hence q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o by TARSKI:def_1; ::_thesis: verum end; suppose l <> indx b1 ; ::_thesis: q . b1 in (b1 +* ((indx b1),{(q . (indx b1))})) . b1 then A74: (b1 +* ((indx b1),{(q . (indx b1))})) . l = b1 . l by FUNCT_7:32; A75: dom b2 = I by PARTFUN1:def_2; A76: dom p0 = I by PARTFUN1:def_2; A77: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ p1_._o_in_b2_._o let o be set ; ::_thesis: ( o in I implies p1 . b1 in b2 . b1 ) assume A78: o in I ; ::_thesis: p1 . b1 in b2 . b1 percases ( o = indx b2 or o <> indx b2 ) ; supposeA79: o = indx b2 ; ::_thesis: p1 . b1 in b2 . b1 then p1 . o = x1 by A76, FUNCT_7:31; then p1 . o in the carrier of (A . ((permutation_of_indices f) . (indx b1))) ; hence p1 . o in b2 . o by B1, A1, A2, A79, Def3; ::_thesis: verum end; suppose o <> indx b2 ; ::_thesis: p1 . b1 in b2 . b1 then p1 . o = p0 . o by FUNCT_7:32; hence p1 . o in b2 . o by A70, A75, A78, CARD_3:9; ::_thesis: verum end; end; end; dom p1 = I by PARTFUN1:def_2; then p in product b2 by A75, A77, CARD_3:9; then consider q0 being set such that A80: q0 in dom f and A81: q0 in B1 and A82: p = f . q0 by A1, FUNCT_1:def_6; q = q0 by A36, A3, A71, A80, A82, FUNCT_1:def_4; hence q . o in (b1 +* ((indx b1),{(q . (indx b1))})) . o by A72, A74, A81, CARD_3:9; ::_thesis: verum end; end; end; I = dom (Carrier A) by PARTFUN1:def_2; then q . (indx b1) in (Carrier A) . (indx b1) by A5, CARD_3:9; then A83: q . (indx b1) in [#] (A . (indx b1)) by Th7; ( dom q = I & dom (b1 +* ((indx b1),{(q . (indx b1))})) = I ) by PARTFUN1:def_2; then q in product (b1 +* ((indx b1),{(q . (indx b1))})) by A73, CARD_3:9; then p0 +* ((indx b2),x1) in f .: (product (b1 +* ((indx b1),{(q . (indx b1))}))) by A36, A71, FUNCT_1:def_6; then ( dom p0 = I & M . (q . (indx b1)) = (p0 +* ((indx b2),x1)) . ((permutation_of_indices f) . (indx b1)) ) by A35, A83, PARTFUN1:def_2; then ( dom M = the carrier of (A . (indx b1)) & M . (q . (indx b1)) = x ) by A43, FUNCT_2:def_1, FUNCT_7:31; hence x in rng M by A83, FUNCT_1:3; ::_thesis: verum end; then A84: rng M = the carrier of (A . ((permutation_of_indices f) . (indx b1))) by XBOOLE_0:def_10; then M is onto by FUNCT_2:def_3; then A85: M " = M " by A44, TOPS_2:def_4; A86: M " is open proof let S0 be Subset of (A . ((permutation_of_indices f) . (indx b1))); :: according to T_0TOPSP:def_2 ::_thesis: ( not S0 is open or (M ") .: S0 is open ) assume S0 is open ; ::_thesis: (M ") .: S0 is open then reconsider S = S0 as Block of (A . ((permutation_of_indices f) . (indx b1))) by PRE_TOPC:def_2; reconsider L = product (b2 +* ((indx b2),S)) as Block of (Segre_Product A) by A43, Th12; reconsider K = f " L as Block of (Segre_Product A) ; consider k being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A87: K = product k and A88: k . (indx k) is Block of (A . (indx k)) by PENCIL_1:24; A89: dom b2 = I by PARTFUN1:def_2; A90: now__::_thesis:_for_x_being_set_st_x_in_I_holds_ (b2_+*_((indx_b2),S))_._x_c=_b2_._x let x be set ; ::_thesis: ( x in I implies (b2 +* ((indx b2),S)) . b1 c= b2 . b1 ) assume x in I ; ::_thesis: (b2 +* ((indx b2),S)) . b1 c= b2 . b1 percases ( x = indx b2 or x <> indx b2 ) ; supposeA91: x = indx b2 ; ::_thesis: (b2 +* ((indx b2),S)) . b1 c= b2 . b1 then (b2 +* ((indx b2),S)) . x = S by A89, FUNCT_7:31; then (b2 +* ((indx b2),S)) . x c= the carrier of (A . ((permutation_of_indices f) . (indx b1))) ; hence (b2 +* ((indx b2),S)) . x c= b2 . x by B1, A1, A2, A91, Def3; ::_thesis: verum end; suppose x <> indx b2 ; ::_thesis: (b2 +* ((indx b2),S)) . b1 c= b2 . b1 hence (b2 +* ((indx b2),S)) . x c= b2 . x by FUNCT_7:32; ::_thesis: verum end; end; end; dom (b2 +* ((indx b2),S)) = I by PARTFUN1:def_2; then L c= product b2 by A89, A90, CARD_3:27; then (product b1) /\ (product k) = K by A1, A37, A87, RELAT_1:143, XBOOLE_1:28; then A92: 2 c= card ((product b1) /\ (product k)) by PENCIL_1:def_6; then A93: indx k = indx b1 by PENCIL_1:26; M " S = k . (indx k) proof thus M " S c= k . (indx k) :: according to XBOOLE_0:def_10 ::_thesis: k . (indx k) c= M " S proof let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in M " S or o in k . (indx k) ) A94: dom b2 = I by PARTFUN1:def_2; assume A95: o in M " S ; ::_thesis: o in k . (indx k) then reconsider u = o as Point of (A . (indx b1)) ; consider p being ManySortedSet of I such that A96: p in product b1 and A97: {(p +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18; reconsider q = p +* ((indx b1),u) as Point of (Segre_Product A) by B2, A96, PENCIL_1:25; reconsider fq = f . q as ManySortedSet of I by PENCIL_1:14; Im (f,(p +* ((indx b1),u))) = {(f . q)} by A36, FUNCT_1:59; then A98: fq in f .: (product (b1 +* ((indx b1),{u}))) by A97, TARSKI:def_1; product (b1 +* ((indx b1),{u})) c= product b1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in product (b1 +* ((indx b1),{u})) or a in product b1 ) A99: dom b1 = I by PARTFUN1:def_2; assume a in product (b1 +* ((indx b1),{u})) ; ::_thesis: a in product b1 then consider g being Function such that A100: a = g and A101: dom g = dom (b1 +* ((indx b1),{u})) and A102: for o being set st o in dom (b1 +* ((indx b1),{u})) holds g . o in (b1 +* ((indx b1),{u})) . o by CARD_3:def_5; A103: dom g = I by A101, PARTFUN1:def_2; now__::_thesis:_for_o_being_set_st_o_in_I_holds_ g_._o_in_b1_._o let o be set ; ::_thesis: ( o in I implies g . b1 in b1 . b1 ) assume o in I ; ::_thesis: g . b1 in b1 . b1 then A104: g . o in (b1 +* ((indx b1),{u})) . o by A101, A102, A103; percases ( o = indx b1 or o <> indx b1 ) ; supposeA105: o = indx b1 ; ::_thesis: g . b1 in b1 . b1 then g . o in {u} by A99, A104, FUNCT_7:31; then g . o in [#] (A . (indx b1)) ; hence g . o in b1 . o by B2, A105, Th10; ::_thesis: verum end; suppose o <> indx b1 ; ::_thesis: g . b1 in b1 . b1 hence g . o in b1 . o by A104, FUNCT_7:32; ::_thesis: verum end; end; end; hence a in product b1 by A100, A103, A99, CARD_3:9; ::_thesis: verum end; then A106: f .: (product (b1 +* ((indx b1),{u}))) c= product b2 by A1, RELAT_1:123; M . o in S by A95, FUNCT_1:def_7; then A107: fq . ((permutation_of_indices f) . (indx b1)) in S by A35, A98; A108: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ fq_._o_in_(b2_+*_((indx_b2),S))_._o let o be set ; ::_thesis: ( o in I implies fq . b1 in (b2 +* ((indx b2),S)) . b1 ) assume A109: o in I ; ::_thesis: fq . b1 in (b2 +* ((indx b2),S)) . b1 percases ( o = indx b2 or o <> indx b2 ) ; suppose o = indx b2 ; ::_thesis: fq . b1 in (b2 +* ((indx b2),S)) . b1 hence fq . o in (b2 +* ((indx b2),S)) . o by A43, A107, A94, FUNCT_7:31; ::_thesis: verum end; suppose o <> indx b2 ; ::_thesis: fq . b1 in (b2 +* ((indx b2),S)) . b1 then (b2 +* ((indx b2),S)) . o = b2 . o by FUNCT_7:32; hence fq . o in (b2 +* ((indx b2),S)) . o by A98, A106, A94, A109, CARD_3:9; ::_thesis: verum end; end; end; ( dom fq = I & dom (b2 +* ((indx b2),S)) = I ) by PARTFUN1:def_2; then fq in L by A108, CARD_3:9; then ( dom k = I & q in K ) by A36, FUNCT_1:def_7, PARTFUN1:def_2; then ( dom p = I & (p +* ((indx b1),u)) . (indx b1) in k . (indx b1) ) by A87, CARD_3:9, PARTFUN1:def_2; hence o in k . (indx k) by A93, FUNCT_7:31; ::_thesis: verum end; let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in k . (indx k) or o in M " S ) assume A110: o in k . (indx k) ; ::_thesis: o in M " S k . (indx k) in the topology of (A . (indx b1)) by A88, A93; then reconsider u = o as Point of (A . (indx b1)) by A110; consider p0 being ManySortedSet of I such that A111: p0 in product b1 and A112: {(p0 +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18; reconsider p = p0 +* ((indx b1),u) as Point of (Segre_Product A) by B2, A111, PENCIL_1:25; reconsider fp = f . p as ManySortedSet of I by PENCIL_1:14; A113: dom b1 = I by PARTFUN1:def_2; A114: dom p0 = I by PARTFUN1:def_2; A115: now__::_thesis:_for_a_being_set_st_a_in_I_holds_ (p0_+*_((indx_b1),u))_._a_in_k_._a let a be set ; ::_thesis: ( a in I implies (p0 +* ((indx b1),u)) . b1 in k . b1 ) assume A116: a in I ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in k . b1 percases ( a = indx b1 or a <> indx b1 ) ; suppose a = indx b1 ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in k . b1 hence (p0 +* ((indx b1),u)) . a in k . a by A93, A110, A114, FUNCT_7:31; ::_thesis: verum end; supposeA117: a <> indx b1 ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in k . b1 then (p0 +* ((indx b1),u)) . a = p0 . a by FUNCT_7:32; then (p0 +* ((indx b1),u)) . a in b1 . a by A111, A113, A116, CARD_3:9; hence (p0 +* ((indx b1),u)) . a in k . a by A92, A117, PENCIL_1:26; ::_thesis: verum end; end; end; ( dom (p0 +* ((indx b1),u)) = I & dom k = I ) by PARTFUN1:def_2; then p in K by A87, A115, CARD_3:9; then ( dom (b2 +* ((indx b2),S)) = I & fp in L ) by FUNCT_1:def_7, PARTFUN1:def_2; then ( dom b2 = I & fp . (indx b2) in (b2 +* ((indx b2),S)) . (indx b2) ) by CARD_3:9, PARTFUN1:def_2; then A118: fp . ((permutation_of_indices f) . (indx b1)) in S by A43, FUNCT_7:31; Im (f,(p0 +* ((indx b1),u))) = {(f . p)} by A36, FUNCT_1:59; then fp in f .: (product (b1 +* ((indx b1),{u}))) by A112, TARSKI:def_1; then M . u = fp . ((permutation_of_indices f) . (indx b1)) by A35; hence o in M " S by A35, A118, FUNCT_1:def_7; ::_thesis: verum end; then (M ") .: S is Block of (A . (indx b1)) by A44, A85, A88, A93, FUNCT_1:85; hence (M ") .: S0 is open by PRE_TOPC:def_2; ::_thesis: verum end; A119: M is open proof let S0 be Subset of (A . (indx b1)); :: according to T_0TOPSP:def_2 ::_thesis: ( not S0 is open or M .: S0 is open ) assume S0 is open ; ::_thesis: M .: S0 is open then reconsider S = S0 as Block of (A . (indx b1)) by PRE_TOPC:def_2; reconsider L = product (b1 +* ((indx b1),S)) as Block of (Segre_Product A) by Th12; reconsider K = f .: L as Block of (Segre_Product A) ; consider k being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A120: K = product k and A121: k . (indx k) is Block of (A . (indx k)) by PENCIL_1:24; A122: dom b1 = I by PARTFUN1:def_2; A123: now__::_thesis:_for_x_being_set_st_x_in_I_holds_ (b1_+*_((indx_b1),S))_._x_c=_b1_._x let x be set ; ::_thesis: ( x in I implies (b1 +* ((indx b1),S)) . b1 c= b1 . b1 ) assume x in I ; ::_thesis: (b1 +* ((indx b1),S)) . b1 c= b1 . b1 percases ( x = indx b1 or x <> indx b1 ) ; supposeA124: x = indx b1 ; ::_thesis: (b1 +* ((indx b1),S)) . b1 c= b1 . b1 then (b1 +* ((indx b1),S)) . x = S by A122, FUNCT_7:31; then (b1 +* ((indx b1),S)) . x c= [#] (A . (indx b1)) ; hence (b1 +* ((indx b1),S)) . x c= b1 . x by B2, A124, Th10; ::_thesis: verum end; suppose x <> indx b1 ; ::_thesis: (b1 +* ((indx b1),S)) . b1 c= b1 . b1 hence (b1 +* ((indx b1),S)) . x c= b1 . x by FUNCT_7:32; ::_thesis: verum end; end; end; dom (b1 +* ((indx b1),S)) = I by PARTFUN1:def_2; then A125: L c= product b1 by A122, A123, CARD_3:27; then (product b2) /\ (product k) = K by A1, A120, RELAT_1:123, XBOOLE_1:28; then 2 c= card ((product b2) /\ (product k)) by PENCIL_1:def_6; then A126: indx k = (permutation_of_indices f) . (indx b1) by A43, PENCIL_1:26; A127: dom k = I by PARTFUN1:def_2; M .: S = k . (indx k) proof thus M .: S c= k . (indx k) :: according to XBOOLE_0:def_10 ::_thesis: k . (indx k) c= M .: S proof let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in M .: S or o in k . (indx k) ) A128: dom b1 = I by PARTFUN1:def_2; assume o in M .: S ; ::_thesis: o in k . (indx k) then consider u being set such that A129: u in dom M and A130: u in S and A131: o = M . u by FUNCT_1:def_6; reconsider u = u as Point of (A . (indx b1)) by A129; consider p0 being ManySortedSet of I such that A132: p0 in product b1 and A133: {(p0 +* ((indx b1),u))} = product (b1 +* ((indx b1),{u})) by Th18; reconsider p = p0 +* ((indx b1),u) as Point of (Segre_Product A) by B2, A132, PENCIL_1:25; reconsider q = f . p as ManySortedSet of I by PENCIL_1:14; Im (f,(p0 +* ((indx b1),u))) = {(f . p)} by A36, FUNCT_1:59; then q in f .: (product (b1 +* ((indx b1),{u}))) by A133, TARSKI:def_1; then A134: M . u = q . ((permutation_of_indices f) . (indx b1)) by A35; A135: dom p0 = I by PARTFUN1:def_2; A136: now__::_thesis:_for_a_being_set_st_a_in_I_holds_ (p0_+*_((indx_b1),u))_._a_in_(b1_+*_((indx_b1),S))_._a let a be set ; ::_thesis: ( a in I implies (p0 +* ((indx b1),u)) . b1 in (b1 +* ((indx b1),S)) . b1 ) assume A137: a in I ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in (b1 +* ((indx b1),S)) . b1 percases ( a = indx b1 or a <> indx b1 ) ; supposeA138: a = indx b1 ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in (b1 +* ((indx b1),S)) . b1 then (p0 +* ((indx b1),u)) . a = u by A135, FUNCT_7:31; hence (p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a by A130, A128, A138, FUNCT_7:31; ::_thesis: verum end; supposeA139: a <> indx b1 ; ::_thesis: (p0 +* ((indx b1),u)) . b1 in (b1 +* ((indx b1),S)) . b1 then (p0 +* ((indx b1),u)) . a = p0 . a by FUNCT_7:32; then (p0 +* ((indx b1),u)) . a in b1 . a by A132, A128, A137, CARD_3:9; hence (p0 +* ((indx b1),u)) . a in (b1 +* ((indx b1),S)) . a by A139, FUNCT_7:32; ::_thesis: verum end; end; end; ( dom (p0 +* ((indx b1),u)) = I & dom (b1 +* ((indx b1),S)) = I ) by PARTFUN1:def_2; then p in L by A136, CARD_3:9; then q in product k by A36, A120, FUNCT_1:def_6; hence o in k . (indx k) by A127, A126, A131, A134, CARD_3:9; ::_thesis: verum end; let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in k . (indx k) or o in M .: S ) assume A140: o in k . (indx k) ; ::_thesis: o in M .: S k . (indx k) in the topology of (A . ((permutation_of_indices f) . (indx b1))) by A121, A126; then reconsider u = o as Point of (A . ((permutation_of_indices f) . (indx b1))) by A140; consider p0 being ManySortedSet of I such that A141: p0 in product k and {(p0 +* (((permutation_of_indices f) . (indx b1)),u))} = product (k +* (((permutation_of_indices f) . (indx b1)),{u})) by A126, Th18; K in the topology of (Segre_Product A) ; then reconsider p = p0 +* (((permutation_of_indices f) . (indx b1)),u) as Point of (Segre_Product A) by A120, A141, PENCIL_1:25; reconsider q = (f ") . p as ManySortedSet of I by PENCIL_1:14; A142: dom k = I by PARTFUN1:def_2; A143: dom p0 = I by PARTFUN1:def_2; A144: now__::_thesis:_for_z_being_set_st_z_in_I_holds_ (p0_+*_(((permutation_of_indices_f)_._(indx_b1)),u))_._z_in_k_._z let z be set ; ::_thesis: ( z in I implies (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b1 in k . b1 ) assume A145: z in I ; ::_thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b1 in k . b1 percases ( z = (permutation_of_indices f) . (indx b1) or z <> (permutation_of_indices f) . (indx b1) ) ; suppose z = (permutation_of_indices f) . (indx b1) ; ::_thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b1 in k . b1 hence (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z by A126, A140, A143, FUNCT_7:31; ::_thesis: verum end; suppose z <> (permutation_of_indices f) . (indx b1) ; ::_thesis: (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . b1 in k . b1 then (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z = p0 . z by FUNCT_7:32; hence (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . z in k . z by A141, A142, A145, CARD_3:9; ::_thesis: verum end; end; end; A146: p = f . q by A68, A3, A69, FUNCT_1:35; dom (p0 +* (((permutation_of_indices f) . (indx b1)),u)) = I by PARTFUN1:def_2; then p in f .: L by A120, A142, A144, CARD_3:9; then ex qq being set st ( qq in dom f & qq in L & p = f . qq ) by FUNCT_1:def_6; then A147: q in L by A36, A3, A146, FUNCT_1:def_4; dom (b1 +* ((indx b1),S)) = I by PARTFUN1:def_2; then q . (indx b1) in (b1 +* ((indx b1),S)) . (indx b1) by A147, CARD_3:9; then A148: q . (indx b1) in S by A122, FUNCT_7:31; then reconsider qi = q . (indx b1) as Point of (A . (indx b1)) ; consider q0 being ManySortedSet of I such that A149: q0 in product b1 and A150: {(q0 +* ((indx b1),qi))} = product (b1 +* ((indx b1),{qi})) by Th18; A151: dom q0 = I by PARTFUN1:def_2; A152: now__::_thesis:_for_a_being_set_st_a_in_I_holds_ (q0_+*_((indx_b1),qi))_._a_=_q_._a let a be set ; ::_thesis: ( a in I implies (q0 +* ((indx b1),qi)) . b1 = q . b1 ) assume a in I ; ::_thesis: (q0 +* ((indx b1),qi)) . b1 = q . b1 percases ( a = indx b1 or a <> indx b1 ) ; suppose a = indx b1 ; ::_thesis: (q0 +* ((indx b1),qi)) . b1 = q . b1 hence (q0 +* ((indx b1),qi)) . a = q . a by A151, FUNCT_7:31; ::_thesis: verum end; supposeA153: a <> indx b1 ; ::_thesis: (q0 +* ((indx b1),qi)) . b1 = q . b1 then (q0 +* ((indx b1),qi)) . a = q0 . a by FUNCT_7:32; hence (q0 +* ((indx b1),qi)) . a = q . a by A125, A147, A149, A153, PENCIL_1:23; ::_thesis: verum end; end; end; ( dom q = I & dom (q0 +* ((indx b1),qi)) = I ) by PARTFUN1:def_2; then q0 +* ((indx b1),qi) = q by A152, FUNCT_1:2; then Im (f,(q0 +* ((indx b1),qi))) = {(f . q)} by A36, FUNCT_1:59; then p in f .: (product (b1 +* ((indx b1),{qi}))) by A146, A150, TARSKI:def_1; then M . (q . (indx b1)) = (p0 +* (((permutation_of_indices f) . (indx b1)),u)) . ((permutation_of_indices f) . (indx b1)) by A35; then M . (q . (indx b1)) = o by A143, FUNCT_7:31; hence o in M .: S by A35, A148, FUNCT_1:def_6; ::_thesis: verum end; hence M .: S0 is open by A121, A126, PRE_TOPC:def_2; ::_thesis: verum end; take M ; ::_thesis: ( M is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) ) ) A154: M is onto by A84, FUNCT_2:def_3; then M " is bijective by A44, PENCIL_2:12; hence M is isomorphic by A44, A154, A119, A86, PENCIL_2:def_4; ::_thesis: for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) let a be ManySortedSet of I; ::_thesis: ( a is Point of (Segre_Product A) & a in product b1 implies for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) ) assume that A155: a is Point of (Segre_Product A) and A156: a in product b1 ; ::_thesis: for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) dom (Carrier A) = I by PARTFUN1:def_2; then a . (indx b1) in (Carrier A) . (indx b1) by A5, A155, CARD_3:9; then a . (indx b1) in [#] (A . (indx b1)) by Th7; then reconsider ai = a . (indx b1) as Point of (A . (indx b1)) ; A157: dom b1 = I by PARTFUN1:def_2; A158: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ a_._o_in_(b1_+*_((indx_b1),{ai}))_._o let o be set ; ::_thesis: ( o in I implies a . b1 in (b1 +* ((indx b1),{ai})) . b1 ) assume A159: o in I ; ::_thesis: a . b1 in (b1 +* ((indx b1),{ai})) . b1 percases ( o = indx b1 or o <> indx b1 ) ; supposeA160: o = indx b1 ; ::_thesis: a . b1 in (b1 +* ((indx b1),{ai})) . b1 then (b1 +* ((indx b1),{ai})) . o = {ai} by A157, FUNCT_7:31; hence a . o in (b1 +* ((indx b1),{ai})) . o by A160, TARSKI:def_1; ::_thesis: verum end; suppose o <> indx b1 ; ::_thesis: a . b1 in (b1 +* ((indx b1),{ai})) . b1 then (b1 +* ((indx b1),{ai})) . o = b1 . o by FUNCT_7:32; hence a . o in (b1 +* ((indx b1),{ai})) . o by A156, A157, A159, CARD_3:9; ::_thesis: verum end; end; end; ( dom a = I & dom (b1 +* ((indx b1),{ai})) = I ) by PARTFUN1:def_2; then A161: a in product (b1 +* ((indx b1),{ai})) by A158, CARD_3:9; let b be ManySortedSet of I; ::_thesis: ( b = f . a implies b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) ) assume b = f . a ; ::_thesis: b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) then b in f .: (product (b1 +* ((indx b1),{ai}))) by A36, A155, A161, FUNCT_1:def_6; hence b . ((permutation_of_indices f) . (indx b1)) = M . (a . (indx b1)) by A35; ::_thesis: verum end; uniqueness for b1, b2 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) st b1 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = b1 . (a . (indx b1)) ) & b2 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = b2 . (a . (indx b1)) ) holds b1 = b2 proof set i = indx b1; set s = permutation_of_indices f; let f1, f2 be Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))); ::_thesis: ( f1 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = f1 . (a . (indx b1)) ) & f2 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = f2 . (a . (indx b1)) ) implies f1 = f2 ) assume that f1 is isomorphic and A162: for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = f1 . (a . (indx b1)) and f2 is isomorphic and A163: for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = f2 . (a . (indx b1)) ; ::_thesis: f1 = f2 A164: now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x ) consider p being set such that A165: p in product b1 by XBOOLE_0:def_1; assume x in dom f1 ; ::_thesis: f1 . x = f2 . x then reconsider x0 = x as Point of (A . (indx b1)) ; reconsider p = p as Point of (Segre_Product A) by B2, A165; reconsider P = p as ManySortedSet of I by PENCIL_1:14; set a = P +* ((indx b1),x0); reconsider a1 = P +* ((indx b1),x0) as Point of (Segre_Product A) by PENCIL_1:25; A166: dom b1 = I by PARTFUN1:def_2; A167: dom P = I by PARTFUN1:def_2; A168: now__::_thesis:_for_e_being_set_st_e_in_I_holds_ (P_+*_((indx_b1),x0))_._e_in_b1_._e let e be set ; ::_thesis: ( e in I implies (P +* ((indx b1),x0)) . b1 in b1 . b1 ) assume A169: e in I ; ::_thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1 percases ( e = indx b1 or e <> indx b1 ) ; supposeA170: e = indx b1 ; ::_thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1 then (P +* ((indx b1),x0)) . e = x0 by A167, FUNCT_7:31; then (P +* ((indx b1),x0)) . e in [#] (A . (indx b1)) ; hence (P +* ((indx b1),x0)) . e in b1 . e by B2, A170, Th10; ::_thesis: verum end; suppose e <> indx b1 ; ::_thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1 then (P +* ((indx b1),x0)) . e = P . e by FUNCT_7:32; hence (P +* ((indx b1),x0)) . e in b1 . e by A165, A166, A169, CARD_3:9; ::_thesis: verum end; end; end; reconsider b = f . a1 as ManySortedSet of I by PENCIL_1:14; dom P = I by PARTFUN1:def_2; then A171: (P +* ((indx b1),x0)) . (indx b1) = x by FUNCT_7:31; dom (P +* ((indx b1),x0)) = I by PARTFUN1:def_2; then A172: P +* ((indx b1),x0) in product b1 by A166, A168, CARD_3:9; then f2 . ((P +* ((indx b1),x0)) . (indx b1)) = b . ((permutation_of_indices f) . (indx b1)) by A163; hence f1 . x = f2 . x by A162, A172, A171; ::_thesis: verum end; dom f1 = the carrier of (A . (indx b1)) by FUNCT_2:def_1 .= dom f2 by FUNCT_2:def_1 ; hence f1 = f2 by A164, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines canonical_embedding PENCIL_3:def_4_:_ for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A holds for b5 being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) holds ( b5 = canonical_embedding (f,b1) iff ( b5 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds for b being ManySortedSet of I st b = f . a holds b . ((permutation_of_indices f) . (indx b1)) = b5 . (a . (indx b1)) ) ) ); theorem Th26: :: PENCIL_3:26 for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) proof let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A) for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) let f be Collineation of (Segre_Product A); ::_thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) let B1, B2 be Segre-Coset of A; ::_thesis: ( B1 misses B2 & B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) ) assume that A2: B1 misses B2 and A3: B1 '||' B2 ; ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b1 = B1 & product b2 = B2 implies canonical_embedding (f,b1) = canonical_embedding (f,b2) ) assume that A4: product b1 = B1 and A5: product b2 = B2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2) A6: indx b1 = indx b2 by A2, A3, A4, A5, Th21; reconsider B3 = f .: B1, B4 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24; A7: f is bijective by PENCIL_2:def_4; then A8: B3 misses B4 by A2, FUNCT_1:66; set i = indx b1; consider r being Element of I such that A9: r <> indx b1 and A10: for i being Element of I st i <> r holds b1 . i = b2 . i and A11: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds c1,c2 are_collinear by A2, A3, A4, A5, Th21; consider b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A12: product b4 = B4 and A13: b4 . (indx b4) = [#] (A . (indx b4)) by PENCIL_2:def_2; consider b3 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A14: product b3 = B3 and A15: b3 . (indx b3) = [#] (A . (indx b3)) by PENCIL_2:def_2; B3 '||' B4 by A3, Th20; then A16: indx b3 = indx b4 by A8, A14, A12, Th21; set j = indx b3; A17: dom f = the carrier of (Segre_Product A) by FUNCT_2:def_1; A18: dom b1 = I by PARTFUN1:def_2; A19: now__::_thesis:_for_o_being_set_st_o_in_the_carrier_of_(A_._(indx_b1))_holds_ (canonical_embedding_(f,b1))_._o_=_(canonical_embedding_(f,b2))_._o b2 . r is trivial by A6, A9, PENCIL_1:def_21; then consider c2 being set such that A20: b2 . r = {c2} by ZFMISC_1:131; b2 c= Carrier A by PBOOLE:def_18; then b2 . r c= (Carrier A) . r by PBOOLE:def_2; then A21: {c2} c= [#] (A . r) by A20, Th7; let o be set ; ::_thesis: ( o in the carrier of (A . (indx b1)) implies (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1 ) consider p0 being set such that A22: p0 in product b1 by XBOOLE_0:def_1; assume o in the carrier of (A . (indx b1)) ; ::_thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1 then reconsider u = o as Point of (A . (indx b1)) ; reconsider p1 = p0 as Point of (Segre_Product A) by A4, A22; reconsider p = p1 as ManySortedSet of I by PENCIL_1:14; set q = p +* ((indx b1),u); reconsider q1 = p +* ((indx b1),u) as Point of (Segre_Product A) by PENCIL_1:25; b1 . r is trivial by A9, PENCIL_1:def_21; then consider c1 being set such that A23: b1 . r = {c1} by ZFMISC_1:131; b1 c= Carrier A by PBOOLE:def_18; then b1 . r c= (Carrier A) . r by PBOOLE:def_2; then {c1} c= [#] (A . r) by A23, Th7; then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31; reconsider c2 = c2 as Point of (A . r) by A21, ZFMISC_1:31; set t = (p +* ((indx b1),u)) +* (r,c2); p +* ((indx b1),u) is Point of (Segre_Product A) by PENCIL_1:25; then reconsider t1 = (p +* ((indx b1),u)) +* (r,c2) as Point of (Segre_Product A) by PENCIL_1:25; percases ( c1 <> c2 or c1 = c2 ) ; supposeA24: c1 <> c2 ; ::_thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1 (p +* ((indx b1),u)) . r = p . r by A9, FUNCT_7:32; then (p +* ((indx b1),u)) . r in b1 . r by A18, A22, CARD_3:9; then A25: (p +* ((indx b1),u)) . r = c1 by A23, TARSKI:def_1; dom (p +* ((indx b1),u)) = I by PARTFUN1:def_2; then A26: ((p +* ((indx b1),u)) +* (r,c2)) . r = c2 by FUNCT_7:31; now__::_thesis:_for_q3,_t3_being_ManySortedSet_of_I_st_q3_=_q1_&_t3_=_t1_holds_ ex_r_being_Element_of_I_st_ (_(_for_a,_b_being_Point_of_(A_._r)_st_a_=_q3_._r_&_b_=_t3_._r_holds_ (_a_<>_b_&_a,b_are_collinear_)_)_&_(_for_j_being_Element_of_I_st_j_<>_r_holds_ q3_._j_=_t3_._j_)_) let q3, t3 be ManySortedSet of I; ::_thesis: ( q3 = q1 & t3 = t1 implies ex r being Element of I st ( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds q3 . j = t3 . j ) ) ) assume A27: ( q3 = q1 & t3 = t1 ) ; ::_thesis: ex r being Element of I st ( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds q3 . j = t3 . j ) ) take r = r; ::_thesis: ( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds ( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds q3 . j = t3 . j ) ) thus for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds ( a <> b & a,b are_collinear ) by A11, A23, A20, A24, A25, A26, A27; ::_thesis: for j being Element of I st j <> r holds q3 . j = t3 . j let j be Element of I; ::_thesis: ( j <> r implies q3 . j = t3 . j ) assume j <> r ; ::_thesis: q3 . j = t3 . j hence q3 . j = t3 . j by A27, FUNCT_7:32; ::_thesis: verum end; then q1,t1 are_collinear by A24, A25, A26, Th17; then A28: f . q1,f . t1 are_collinear by Th1; reconsider fq = f . q1, ft = f . t1 as ManySortedSet of I by PENCIL_1:14; A29: dom b1 = I by PARTFUN1:def_2; A30: dom p = I by PARTFUN1:def_2; A31: now__::_thesis:_for_a_being_set_st_a_in_I_holds_ (p_+*_((indx_b1),u))_._a_in_b1_._a let a be set ; ::_thesis: ( a in I implies (p +* ((indx b1),u)) . b1 in b1 . b1 ) assume A32: a in I ; ::_thesis: (p +* ((indx b1),u)) . b1 in b1 . b1 percases ( a = indx b1 or a <> indx b1 ) ; suppose a = indx b1 ; ::_thesis: (p +* ((indx b1),u)) . b1 in b1 . b1 then ( (p +* ((indx b1),u)) . a = u & b1 . a = [#] (A . (indx b1)) ) by A4, A30, Th10, FUNCT_7:31; hence (p +* ((indx b1),u)) . a in b1 . a ; ::_thesis: verum end; suppose a <> indx b1 ; ::_thesis: (p +* ((indx b1),u)) . b1 in b1 . b1 then (p +* ((indx b1),u)) . a = p . a by FUNCT_7:32; hence (p +* ((indx b1),u)) . a in b1 . a by A22, A29, A32, CARD_3:9; ::_thesis: verum end; end; end; A33: dom (p +* ((indx b1),u)) = I by PARTFUN1:def_2; then A34: p +* ((indx b1),u) in product b1 by A29, A31, CARD_3:9; A35: now__::_thesis:_for_a_being_set_st_a_in_I_holds_ ((p_+*_((indx_b1),u))_+*_(r,c2))_._a_in_b2_._a let a be set ; ::_thesis: ( a in I implies ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1 ) assume A36: a in I ; ::_thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1 percases ( a = r or a <> r ) ; supposeA37: a = r ; ::_thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1 then ((p +* ((indx b1),u)) +* (r,c2)) . a = c2 by A33, FUNCT_7:31; hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by A20, A37, TARSKI:def_1; ::_thesis: verum end; supposeA38: a <> r ; ::_thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b1 in b2 . b1 then ((p +* ((indx b1),u)) +* (r,c2)) . a = (p +* ((indx b1),u)) . a by FUNCT_7:32; then ((p +* ((indx b1),u)) +* (r,c2)) . a in b1 . a by A31, A36; hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by A10, A36, A38; ::_thesis: verum end; end; end; ( dom ((p +* ((indx b1),u)) +* (r,c2)) = I & dom b2 = I ) by PARTFUN1:def_2; then A39: (p +* ((indx b1),u)) +* (r,c2) in product b2 by A35, CARD_3:9; then A40: (canonical_embedding (f,b2)) . (((p +* ((indx b1),u)) +* (r,c2)) . (indx b1)) = ft . ((permutation_of_indices f) . (indx b1)) by A1, A5, A6, Def4; A41: f . q1 <> f . t1 by A17, A7, A24, A25, A26, FUNCT_1:def_4; A42: now__::_thesis:_not_fq_._(indx_b3)_<>_ft_._(indx_b3) consider l being Element of I such that for a, b being Point of (A . l) st a = fq . l & b = ft . l holds ( a <> b & a,b are_collinear ) and A43: for j being Element of I st j <> l holds fq . j = ft . j by A41, A28, Th17; assume fq . (indx b3) <> ft . (indx b3) ; ::_thesis: contradiction then A44: indx b3 = l by A43; A45: dom b4 = I by PARTFUN1:def_2; A46: fq in B3 by A17, A4, A34, FUNCT_1:def_6; A47: dom b3 = I by PARTFUN1:def_2; A48: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ fq_._o_in_b4_._o let o be set ; ::_thesis: ( o in I implies fq . b1 in b4 . b1 ) assume o in I ; ::_thesis: fq . b1 in b4 . b1 then reconsider o1 = o as Element of I ; percases ( o1 = indx b3 or o1 <> indx b3 ) ; suppose o1 = indx b3 ; ::_thesis: fq . b1 in b4 . b1 hence fq . o in b4 . o by A14, A15, A13, A16, A46, A47, CARD_3:9; ::_thesis: verum end; suppose o1 <> indx b3 ; ::_thesis: fq . b1 in b4 . b1 then A49: fq . o1 = ft . o1 by A43, A44; ft in product b4 by A17, A5, A12, A39, FUNCT_1:def_6; hence fq . o in b4 . o by A45, A49, CARD_3:9; ::_thesis: verum end; end; end; dom fq = I by PARTFUN1:def_2; then fq in product b4 by A45, A48, CARD_3:9; then fq in (product b3) /\ (product b4) by A14, A46, XBOOLE_0:def_4; hence contradiction by A8, A14, A12, XBOOLE_0:def_7; ::_thesis: verum end; A50: indx b3 = (permutation_of_indices f) . (indx b1) by A1, A4, A14, Def3; dom p = I by PARTFUN1:def_2; then A51: (p +* ((indx b1),u)) . (indx b1) = o by FUNCT_7:31; then ((p +* ((indx b1),u)) +* (r,c2)) . (indx b1) = o by A9, FUNCT_7:32; hence (canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o by A1, A4, A50, A34, A40, A42, A51, Def4; ::_thesis: verum end; supposeA52: c1 = c2 ; ::_thesis: (canonical_embedding (f,b1)) . b1 = (canonical_embedding (f,b2)) . b1 A53: now__::_thesis:_for_o_being_set_st_o_in_I_holds_ b1_._o_=_b2_._o let o be set ; ::_thesis: ( o in I implies b1 . b1 = b2 . b1 ) assume o in I ; ::_thesis: b1 . b1 = b2 . b1 then reconsider o1 = o as Element of I ; percases ( r = o1 or r <> o1 ) ; suppose r = o1 ; ::_thesis: b1 . b1 = b2 . b1 hence b1 . o = b2 . o by A23, A20, A52; ::_thesis: verum end; suppose r <> o1 ; ::_thesis: b1 . b1 = b2 . b1 hence b1 . o = b2 . o by A10; ::_thesis: verum end; end; end; ( dom b1 = I & dom b2 = I ) by PARTFUN1:def_2; hence (canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o by A53, FUNCT_1:2; ::_thesis: verum end; end; end; ( dom (canonical_embedding (f,b1)) = the carrier of (A . (indx b1)) & dom (canonical_embedding (f,b2)) = the carrier of (A . (indx b1)) ) by A6, FUNCT_2:def_1; hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A19, FUNCT_1:2; ::_thesis: verum end; theorem Th27: :: PENCIL_3:27 for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) proof let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A) for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) A2: now__::_thesis:_for_o_being_Element_of_I_holds_A_._o_is_connected let o be Element of I; ::_thesis: A . o is connected A . o is strongly_connected by A1; hence A . o is connected by Th4; ::_thesis: verum end; let f be Collineation of (Segre_Product A); ::_thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 holds canonical_embedding (f,b1) = canonical_embedding (f,b2) let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & indx b1 = indx b2 implies canonical_embedding (f,b1) = canonical_embedding (f,b2) ) assume that A3: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A ) and A4: indx b1 = indx b2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2) reconsider B1 = product b1, B2 = product b2 as Segre-Coset of A by A3; percases ( B1 misses B2 or B1 meets B2 ) ; suppose B1 misses B2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2) then consider D being FinSequence of bool the carrier of (Segre_Product A) such that A5: D . 1 = B1 and A6: D . (len D) = B2 and A7: for i being Nat st i in dom D holds D . i is Segre-Coset of A and A8: for i being Nat st 1 <= i & i < len D holds for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds ( Di misses Di1 & Di '||' Di1 ) by A2, A4, Th23; defpred S1[ Nat] means ( $1 in dom D implies for D1 being Segre-Coset of A st D1 = D . $1 holds for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D1 = product d1 holds canonical_embedding (f,b1) = canonical_embedding (f,d1) ); A9: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A10: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof assume k + 1 in dom D ; ::_thesis: for D1 being Segre-Coset of A st D1 = D . (k + 1) holds for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D1 = product d1 holds canonical_embedding (f,b1) = canonical_embedding (f,d1) then k + 1 <= len D by FINSEQ_3:25; then A11: k < len D by NAT_1:13; let D2 be Segre-Coset of A; ::_thesis: ( D2 = D . (k + 1) implies for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D2 = product d1 holds canonical_embedding (f,b1) = canonical_embedding (f,d1) ) assume A12: D2 = D . (k + 1) ; ::_thesis: for d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st D2 = product d1 holds canonical_embedding (f,b1) = canonical_embedding (f,d1) let d2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( D2 = product d2 implies canonical_embedding (f,b1) = canonical_embedding (f,d2) ) assume A13: D2 = product d2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,d2) percases ( k = 0 or 1 <= k ) by NAT_1:14; suppose k = 0 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,d2) hence canonical_embedding (f,b1) = canonical_embedding (f,d2) by A5, A12, A13, PUA2MSS1:2; ::_thesis: verum end; supposeA14: 1 <= k ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,d2) then k in dom D by A11, FINSEQ_3:25; then reconsider D1 = D . k as Segre-Coset of A by A7; consider d1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A15: product d1 = D1 and d1 . (indx d1) = [#] (A . (indx d1)) by PENCIL_2:def_2; ( D1 misses D2 & D1 '||' D2 ) by A8, A11, A12, A14; then canonical_embedding (f,d1) = canonical_embedding (f,d2) by A1, A13, A15, Th26; hence canonical_embedding (f,b1) = canonical_embedding (f,d2) by A10, A11, A14, A15, FINSEQ_3:25; ::_thesis: verum end; end; end; end; A16: S1[ 0 ] by FINSEQ_3:24; for n being Nat holds S1[n] from NAT_1:sch_2(A16, A9); then A17: S1[ len D] ; 1 in dom D by A5, FUNCT_1:def_2; then 1 <= len D by FINSEQ_3:25; hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A6, A17, FINSEQ_3:25; ::_thesis: verum end; suppose B1 meets B2 ; ::_thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2) hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A4, Th11; ::_thesis: verum end; end; end; definition let I be non empty finite set ; let A be PLS-yielding ManySortedSet of I; assume B1: for i being Element of I holds A . i is strongly_connected ; let f be Collineation of (Segre_Product A); let i be Element of I; func canonical_embedding (f,i) -> Function of (A . i),(A . ((permutation_of_indices f) . i)) means :Def5: :: PENCIL_3:def 5 for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds it = canonical_embedding (f,b); existence ex b1 being Function of (A . i),(A . ((permutation_of_indices f) . i)) st for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds b1 = canonical_embedding (f,b) proof consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A1: indx L = i and A2: product L is Segre-Coset of A by Th8; reconsider n = canonical_embedding (f,L) as Function of (A . i),(A . ((permutation_of_indices f) . i)) by A1; take n ; ::_thesis: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds n = canonical_embedding (f,b) let b be non trivial-yielding Segre-like ManySortedSubset of Carrier A; ::_thesis: ( product b is Segre-Coset of A & indx b = i implies n = canonical_embedding (f,b) ) assume ( product b is Segre-Coset of A & indx b = i ) ; ::_thesis: n = canonical_embedding (f,b) hence n = canonical_embedding (f,b) by B1, A1, A2, Th27; ::_thesis: verum end; uniqueness for b1, b2 being Function of (A . i),(A . ((permutation_of_indices f) . i)) st ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds b1 = canonical_embedding (f,b) ) & ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds b2 = canonical_embedding (f,b) ) holds b1 = b2 proof let n1, n2 be Function of (A . i),(A . ((permutation_of_indices f) . i)); ::_thesis: ( ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds n1 = canonical_embedding (f,b) ) & ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds n2 = canonical_embedding (f,b) ) implies n1 = n2 ) assume that A3: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds n1 = canonical_embedding (f,b) and A4: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds n2 = canonical_embedding (f,b) ; ::_thesis: n1 = n2 consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A5: ( indx L = i & product L is Segre-Coset of A ) by Th8; thus n1 = canonical_embedding (f,L) by A3, A5 .= n2 by A4, A5 ; ::_thesis: verum end; end; :: deftheorem Def5 defines canonical_embedding PENCIL_3:def_5_:_ for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) for i being Element of I for b5 being Function of (A . i),(A . ((permutation_of_indices f) . i)) holds ( b5 = canonical_embedding (f,i) iff for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds b5 = canonical_embedding (f,b) ); theorem :: PENCIL_3:28 for I being non empty finite set for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st for i being Element of I holds ( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds m is isomorphic ) & ( for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . (s . i)) st m = B . i holds b . (s . i) = m . (a . i) ) ) proof let I be non empty finite set ; ::_thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds for f being Collineation of (Segre_Product A) ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st for i being Element of I holds ( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds m is isomorphic ) & ( for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . (s . i)) st m = B . i holds b . (s . i) = m . (a . i) ) ) let A be PLS-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st for i being Element of I holds ( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds m is isomorphic ) & ( for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . (s . i)) st m = B . i holds b . (s . i) = m . (a . i) ) ) ) assume A1: for i being Element of I holds A . i is strongly_connected ; ::_thesis: for f being Collineation of (Segre_Product A) ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st for i being Element of I holds ( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds m is isomorphic ) & ( for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . (s . i)) st m = B . i holds b . (s . i) = m . (a . i) ) ) let f be Collineation of (Segre_Product A); ::_thesis: ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st for i being Element of I holds ( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds m is isomorphic ) & ( for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . (s . i)) st m = B . i holds b . (s . i) = m . (a . i) ) ) set s = permutation_of_indices f; take permutation_of_indices f ; ::_thesis: ex B being Function-yielding ManySortedSet of I st for i being Element of I holds ( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds m is isomorphic ) & ( for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) ) ) defpred S1[ set , set ] means for i being Element of I st i = $1 holds $2 = canonical_embedding (f,i); A2: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume i in I ; ::_thesis: ex j being set st S1[i,j] then reconsider i1 = i as Element of I ; S1[i1, canonical_embedding (f,i1)] ; hence ex j being set st S1[i,j] ; ::_thesis: verum end; consider B being ManySortedSet of I such that A3: for i being set st i in I holds S1[i,B . i] from PBOOLE:sch_3(A2); now__::_thesis:_for_x_being_set_st_x_in_dom_B_holds_ B_._x_is_Function let x be set ; ::_thesis: ( x in dom B implies B . x is Function ) assume x in dom B ; ::_thesis: B . x is Function then reconsider y = x as Element of I ; B . y = canonical_embedding (f,y) by A3; hence B . x is Function ; ::_thesis: verum end; then reconsider B = B as Function-yielding ManySortedSet of I by FUNCOP_1:def_6; take B ; ::_thesis: for i being Element of I holds ( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds m is isomorphic ) & ( for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) ) ) let i be Element of I; ::_thesis: ( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds m is isomorphic ) & ( for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) ) ) A4: B . i = canonical_embedding (f,i) by A3; thus ( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds m is isomorphic ) ) ::_thesis: for p being Point of (Segre_Product A) for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) proof thus B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) by A4; ::_thesis: for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds m is isomorphic let m be Function of (A . i),(A . ((permutation_of_indices f) . i)); ::_thesis: ( m = B . i implies m is isomorphic ) assume A5: m = B . i ; ::_thesis: m is isomorphic consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A6: ( indx L = i & product L is Segre-Coset of A ) by Th8; B . i = canonical_embedding (f,L) by A1, A4, A6, Def5; hence m is isomorphic by A1, A5, A6, Def4; ::_thesis: verum end; let p be Point of (Segre_Product A); ::_thesis: for a being ManySortedSet of I st a = p holds for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) let a be ManySortedSet of I; ::_thesis: ( a = p implies for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) ) assume A7: a = p ; ::_thesis: for b being ManySortedSet of I st b = f . p holds for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that A8: ( indx b1 = i & product b1 is Segre-Coset of A ) and A9: a in product b1 by A7, Th9; let b be ManySortedSet of I; ::_thesis: ( b = f . p implies for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) ) assume A10: b = f . p ; ::_thesis: for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds b . ((permutation_of_indices f) . i) = m . (a . i) let m be Function of (A . i),(A . ((permutation_of_indices f) . i)); ::_thesis: ( m = B . i implies b . ((permutation_of_indices f) . i) = m . (a . i) ) assume m = B . i ; ::_thesis: b . ((permutation_of_indices f) . i) = m . (a . i) then m = canonical_embedding (f,b1) by A1, A4, A8, Def5; hence b . ((permutation_of_indices f) . i) = m . (a . i) by A1, A7, A10, A8, A9, Def4; ::_thesis: verum end;