:: On the Characterization of Collineations of the Segre Product of Strongly :: Connected Partial Linear Spaces :: by Adam Naumowicz :: :: Received October 18, 2004 :: Copyright (c) 2004-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, STRUCT_0, PRE_TOPC, PENCIL_2, PENCIL_1, FUNCT_1, RELAT_1, TARSKI, SUBSET_1, PRALG_1, PBOOLE, ZFMISC_1, RELAT_2, FINSEQ_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, WAYBEL_3, RLVECT_2, CARD_3, INTEGRA1, FUNCT_4, FINSET_1, FDIFF_1, PARSP_1, GRAPH_2, FUNCT_2, CAT_1, RCOMP_1, FUNCOP_1, PENCIL_3, WAYBEL18; notations TARSKI, XBOOLE_0, ZFMISC_1, XCMPLX_0, XXREAL_0, ORDINAL1, NUMBERS, NAT_1, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, RELSET_1, CARD_1, FINSET_1, FINSEQ_1, CARD_3, DOMAIN_1, STRUCT_0, PRE_TOPC, PBOOLE, PZFMISC1, T_0TOPSP, PRALG_1, WAYBEL_3, PENCIL_1, FUNCT_7, PENCIL_2, TOPS_2, GRAPH_2; constructors PZFMISC1, TOPS_2, REALSET2, T_0TOPSP, GRAPH_2, PENCIL_2, RELSET_1, PBOOLE, FUNCT_7, PRE_POLY; registrations SUBSET_1, RELSET_1, FUNCT_2, XREAL_0, NAT_1, CARD_1, PBOOLE, STRUCT_0, PENCIL_1, ORDINAL1, FUNCT_1, RELAT_1, FINSEQ_1, PRE_POLY; requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM; definitions TARSKI, XBOOLE_0, PBOOLE, FUNCT_1, T_0TOPSP; equalities XBOOLE_0, STRUCT_0, RELAT_1; expansions TARSKI, XBOOLE_0, PBOOLE, FUNCT_1; theorems XBOOLE_0, ZFMISC_1, FUNCT_1, FINSEQ_1, FINSEQ_3, NAT_1, CARD_3, PBOOLE, PRE_TOPC, FUNCT_7, PRALG_1, PZFMISC1, TARSKI, FUNCT_2, TOPS_2, PENCIL_1, PENCIL_2, CARD_1, XBOOLE_1, PUA2MSS1, FINSET_1, CARD_2, GRAPH_2, FUNCOP_1, RELAT_1, RELSET_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1; schemes TRANSGEO, NAT_1, FINSEQ_2, PENCIL_2, FINSEQ_1, PBOOLE, CLASSES1; begin :: Preliminaries theorem Th1: 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; let f be Collineation of S; A1: dom f = the carrier of S by FUNCT_2:def 1; let p,q be Point of S; assume A2: p,q are_collinear; per cases; suppose p=q; hence thesis by PENCIL_1:def 1; end; suppose p<>q; 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 thesis by PENCIL_1:def 1; end; end; theorem Th2: for I being non empty set for i be Element of I for A being non-Trivial-yielding 1-sorted-yielding ManySortedSet of I holds A.i is non trivial proof let I be non empty set; let i be Element of I; let A be non-Trivial-yielding 1-sorted-yielding ManySortedSet of I; dom A = I by PARTFUN1:def 2; then A.i in rng A by FUNCT_1:3; hence thesis by PENCIL_1:def 17; end; theorem Th3: 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; assume A1: S is strongly_connected; now consider X being object such that A2: X in the topology of S by XBOOLE_0:def 1; reconsider X as Block of S by A2; reconsider X1=X as Subset of S by A2; let x being Point of S; X1 is closed_under_lines strong by PENCIL_1:20,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 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 strong by A5,A8; per cases; suppose x in X; hence ex l being Block of S st x in l; end; suppose A10: not x in X; 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 object 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 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; end; end; hence thesis by PENCIL_1:def 9; end; theorem Th4: for S being non empty non void identifying_close_blocks TopStruct holds S is strongly_connected implies S is connected proof let S being non empty non void identifying_close_blocks TopStruct; assume A1: S is strongly_connected; then S is without_isolated_points by Th3; hence thesis by A1,PENCIL_1:28; end; theorem for S being non void non degenerated TopStruct for L being Block of S ex x being Point of S st not x in L proof let S be non void non degenerated TopStruct; let L be Block of S; A1: L in the topology of S; now assume [#]S c= L; then [#]S=L by A1; hence contradiction by PENCIL_1:def 5; end; then consider x being object such that A2: x in [#]S and A3: not x in L; reconsider x as Point of S by A2; take x; thus thesis by A3; end; theorem Th6: 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; let A be non-Empty TopStruct-yielding ManySortedSet of I; let p be Point of Segre_Product 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 object 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 as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18; for i being object st i in I holds f.i is Element of (Carrier A).i by A2,A3,A4; hence thesis by A1,PBOOLE:def 14; end; theorem Th7: for I being non empty set for A be 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; let A be 1-sorted-yielding ManySortedSet of I; let x be Element of I; ex R being 1-sorted st R=A.x & (Carrier A).x = the carrier of R by PRALG_1:def 13; hence thesis; end; theorem Th8: for I being non empty set for i being Element of I for A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I ex L being Segre-like non trivial-yielding ManySortedSubset of Carrier A st indx(L)=i & product L is Segre-Coset of A proof let I being non empty set; let x being Element of I; let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I; 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 A.x is non trivial by PENCIL_1:def 18; then reconsider C=[#](A.x) as non trivial set; reconsider p0 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 Segre-like non trivial-yielding ManySortedSubset of Carrier A by PENCIL_1:9,10,PENCIL_2:7; take 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; product b c= the carrier of Segre_Product A proof let a be object; assume a in product b; then consider f being Function such that A3: a=f and A4: dom f=dom b and A5: for x being object st x in dom b holds f.x in b.x by CARD_3:def 5; dom Carrier A = I by PARTFUN1:def 2; then A6: dom f = dom Carrier A by A4,PARTFUN1:def 2; A7: now let i be object; assume A8: i in dom Carrier A; then reconsider i1=i as Element of I; A9: f.i in b.i by A4,A5,A6,A8; per cases; suppose i1=x; hence f.i in (Carrier A).i by A1,A9,Th7; end; suppose A10: i1<>x; I = dom A by PARTFUN1:def 2; then A.i1 in rng A by FUNCT_1:3; then A.i1 is non 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; AA is non empty; then [#](A.i1) is non empty; then (Carrier A).i1 is non empty by Th7; hence f.i in (Carrier A).i by A11; end; end; Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by PENCIL_1:def 23; hence thesis by A3,A6,A7,CARD_3:def 5; end; hence thesis by A1,A2,PENCIL_2:def 2; end; theorem Th9: for I being non empty set for i being Element of I for A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I for p being Point of Segre_Product A ex L being Segre-like non trivial-yielding ManySortedSubset of Carrier A st indx(L)=i & product L is Segre-Coset of A & p in product L proof let I being non empty set; let x being Element of I; let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I; let p0 be Point of Segre_Product A; dom A = I by PARTFUN1:def 2; then A.x in rng A by FUNCT_1:3; then A.x is non 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 Segre-like non trivial-yielding ManySortedSubset of Carrier A by PENCIL_1:9,10,PENCIL_2:7; take 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; product b c= the carrier of Segre_Product A proof let a be object; assume a in product b; then consider f being Function such that A3: a=f and A4: dom f=dom b and A5: for x being object st x in dom b holds f.x in b.x by CARD_3:def 5; dom Carrier A = I by PARTFUN1:def 2; then A6: dom f = dom Carrier A by A4,PARTFUN1:def 2; A7: now let i be object; assume A8: i in dom Carrier A; then reconsider i1=i as Element of I; A9: f.i in b.i by A4,A5,A6,A8; per cases; suppose i1=x; hence f.i in (Carrier A).i by A1,A9,Th7; end; suppose A10: i1<>x; I = dom A by PARTFUN1:def 2; then A.i1 in rng A by FUNCT_1:3; then A.i1 is non 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; AA is non empty; then [#](A.i1) is non empty; then (Carrier A).i1 is non empty by Th7; hence f.i in (Carrier A).i by A11; end; end; Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by PENCIL_1:def 23; hence thesis by A3,A6,A7,CARD_3:def 5; end; hence product b is Segre-Coset of A by A1,A2,PENCIL_2:def 2; A12: dom p = I by PARTFUN1:def 2; A13: now let z be object; assume A14: z in I; 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: tc is non empty; per cases; suppose A16: z=x; 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; end; suppose z<>x; 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; end; end; dom p09 = I & dom (p+*(x,C)) = I by PARTFUN1:def 2; hence thesis by A13,CARD_3:9; end; theorem Th10: for I being non empty set for A being non-Trivial-yielding TopStruct-yielding ManySortedSet of I for b being Segre-like non trivial-yielding 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; let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I; let b be Segre-like non trivial-yielding ManySortedSubset of Carrier A; assume product b is Segre-Coset of A; then consider L being Segre-like non trivial-yielding 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 thesis by A2; end; theorem Th11: for I being non empty set for A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I for L1,L2 being Segre-like non trivial-yielding 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; let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I; let L1,L2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A; 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; reconsider B1=product L1, B2=product L2 as Segre-Coset of A by A1; B1 /\ B2 <> {} by A3; then consider x being object 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 as Element of Carrier A by A4,Th6; consider b1 being Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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 let a be object; assume A14: a in dom L1; then reconsider i=a as Element of I; per cases; suppose i=indx(L1); hence L1.a = L2.a by A2,A8,A10,A13,A11; end; suppose A15: i<>indx(L1); then L1.i is non empty trivial by PENCIL_1:def 21; then L1.i is 1-element; then consider o1 being object such that A16: L1.i = {o1} by ZFMISC_1:131; L2.i is non empty trivial by A2,A15,PENCIL_1:def 21; then L2.i is 1-element; then consider o2 being object 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; end; end; hence thesis by A12; end; theorem Th12: for I being non empty set for A be PLS-yielding ManySortedSet of I for L being Segre-like non trivial-yielding 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 being non empty set; let A be PLS-yielding ManySortedSet of I; let L being Segre-like non trivial-yielding ManySortedSubset of Carrier A; let B being Block of A.indx(L); B in the topology of A.indx(L); then reconsider B1=B as Subset of A.indx(L); A1: now let i be Element of I; assume A2: i <> indx(L); 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; end; 2 c= card B by PENCIL_1:def 6; then B1 is non trivial by PENCIL_1:4; then reconsider S=L+*(indx(L),B1) as Segre-like non trivial-yielding ManySortedSubset of Carrier A by A1,PENCIL_1:9,def 20,PENCIL_2:7; A3: now assume indx(S)<>indx(L); then S.indx(S) is 1-element by A1; hence contradiction by PENCIL_1:def 21; end; dom L = I by PARTFUN1:def 2; then S.indx(S) = B1 by A3,FUNCT_7:31; hence thesis by A3,PENCIL_1:24; end; theorem Th13: for I being non empty set for A be PLS-yielding ManySortedSet of I for i being Element of I for p being Point of A.i for L being Segre-like non trivial-yielding ManySortedSubset of Carrier A st i<>indx(L) holds L+*(i,{p}) is Segre-like non trivial-yielding ManySortedSubset of Carrier A proof let I be non empty set; let A be PLS-yielding ManySortedSet of I; let i be Element of I; let p be Point of A.i; let L be Segre-like non trivial-yielding ManySortedSubset of Carrier A; A1: now let j be Element of I; A2: dom L=I by PARTFUN1:def 2; assume A3: j<>indx(L); per cases; suppose j=i; hence L+*(i,{p}).j is 1-element by A2,FUNCT_7:31; end; suppose j<>i; then L+*(i,{p}).j = L.j by FUNCT_7:32; hence L+*(i,{p}).j is 1-element by A3,PENCIL_1:12; end; end; A4: L+*(i,{p}) c= Carrier A proof let a be object; assume A5: a in I; then reconsider a1=a as Element of I; A6: a1 in dom L by A5,PARTFUN1:def 2; per cases; suppose A7: a=i; then L+*(i,{p}).a1 = {p} by A6,FUNCT_7:31; then L+*(i,{p}).a1 c= [#](A.a1) by A7; hence thesis by Th7; end; suppose A8: a<>i; A9: L c= Carrier A by PBOOLE:def 18; L+*(i,{p}).a1 = L.a1 by A8,FUNCT_7:32; hence thesis by A9; end; end; assume i<>indx(L); then L+*(i,{p}).indx(L) = L.indx(L) by FUNCT_7:32; then A10: L+*(i,{p}).indx(L) is non 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 thesis by A4,A1,A10,PBOOLE:def 18,PENCIL_1:def 16,def 20; end; theorem Th14: 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 Segre-like non trivial-yielding ManySortedSubset of Carrier A holds product (L+*(i,S)) is Subset of Segre_Product A proof let I be non empty set; let A be PLS-yielding ManySortedSet of I; let i be Element of I; let S be Subset of A.i; let L be Segre-like non trivial-yielding ManySortedSubset of Carrier A; A1: dom (L+*(i,S)) = I by PARTFUN1:def 2 .= dom Carrier A by PARTFUN1:def 2; A2: now let a be object; assume a in dom (L+*(i,S)); then A3: a in I; then A4: a in dom L by PARTFUN1:def 2; per cases; suppose A5: a=i; 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; end; suppose A6: a<>i; 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; end; end; Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by PENCIL_1:def 23; hence thesis by A1,A2,CARD_3:27; end; theorem Th15: 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 being non empty set; let P be ManySortedSet of I; let i be Element of I; {P}.i = {P.i} by PZFMISC1:def 1; hence thesis; end; theorem Th16: for I being non empty set for i being Element of I for A be 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 being non empty set; let i be Element of I; let A be PLS-yielding ManySortedSet of I; let B being Block of A.i; let P being Element of Carrier 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 let j be Element of I; assume j <> i; then {P}+*(i,B1).j = {P}.j by FUNCT_7:32; hence {P}+*(i,B1).j is 1-element by Th15; end; 2 c= card B by PENCIL_1:def 6; then B1 is non trivial by PENCIL_1:4; then reconsider S=PP+*(i,B1) as Segre-like non trivial-yielding ManySortedSubset of Carrier A by A1,PENCIL_1:9,def 20,PENCIL_2:7; A2: now assume indx(S)<>i; then S.indx(S) is 1-element by A1; hence contradiction by PENCIL_1:def 21; end; dom {P} = I by PARTFUN1:def 2; then S.indx(S) = B1 by A2,FUNCT_7:31; hence thesis by A2,PENCIL_1:24; end; theorem Th17: 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 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 being non empty set; let A being PLS-yielding ManySortedSet of I; let p,q being Point of Segre_Product A; assume A1: p<>q; thus p,q are_collinear implies for p1,q1 being ManySortedSet of I st p1=p & q1=q 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 assume p,q are_collinear; 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; assume that A3: p1=p and A4: q1=q; A5: q1 in l by A2,A4,ZFMISC_1:32; consider L being Segre-like non trivial-yielding 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); 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 proof reconsider LI=L.indx(L) as Block of A.indx(L) by A7; let a,b being Point of A.i; A9: ex p0 being Function st p0=p1 & dom p0=dom L & for o being object 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 object 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; now assume A12: a=b; A13: now let o be object; assume A14: o in dom p1; then reconsider o1=o as Element of I; per cases; suppose o1=i; hence p1.o = q1.o by A11,A12; end; suppose o1<>i; then L.o1 is 1-element by PENCIL_1:12; then consider s being object 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; 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; end; hence a<>b; 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 thesis by PENCIL_1:def 1; end; let j being Element of I; assume j<>i; hence thesis by A6,A8,A5,PENCIL_1:23; 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 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 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; per cases by A21,PENCIL_1:def 1; suppose a=b; hence thesis by A19; end; suppose ex l being Block of A.i st {a,b} c= l; 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 object st o in dom ({p1}+*(i,l)) holds q1.o in ({p1}+*(i,l)) .o proof let o be object; assume A26: o in dom ({p1}+*(i,l)); then reconsider o1=o as Element of I; per cases; suppose A27: o1 = i; then ({p1}+*(i,l)).o = l by A24,A26,FUNCT_7:31; hence thesis by A22,A27,ZFMISC_1:32; end; suppose A28: o1 <> i; 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 thesis by TARSKI:def 1; end; end; A29: for o being object st o in dom ({p1}+*(i,l)) holds p1.o in ({p1}+*(i,l)) .o proof let o be object; assume A30: o in dom ({p1}+*(i,l)); per cases; suppose A31: o = i; then ({p1}+*(i,l)).o = l by A24,A30,FUNCT_7:31; hence thesis by A22,A31,ZFMISC_1:32; end; suppose o <> i; then ({p1}+*(i,l)).o = {p1}.o by FUNCT_7:32; then ({p1}+*(i,l)).o = {p1.o} by A30,PZFMISC1:def 1; hence thesis by TARSKI:def 1; 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 thesis by PENCIL_1:def 1; end; end; theorem Th18: for I being non empty set for A being PLS-yielding ManySortedSet of I for b being Segre-like non trivial-yielding 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) qua set} = product(b+*(indx(b),{x})) proof let I be non empty set; let A be PLS-yielding ManySortedSet of I; let b1 be Segre-like non trivial-yielding ManySortedSubset of Carrier A; set i=indx(b1); let x be Point of A.i; consider bb being object 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 object 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 as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18; take p=bb; thus p in product b1 by A1; set bbx=bb+*(i,x); thus {p+*(i,x) qua set}=product(b1+*(i,{x})) proof thus {p+*(i,x) qua set} c= product(b1+*(i,{x})) proof A4: now let z be object; assume z in dom (b1+*(i,{x})); then A5: z in I; then A6: z in dom bb by PARTFUN1:def 2; per cases; suppose A7: z=i; then bbx.z = x by A6,FUNCT_7:31; then bbx.z in {x} by TARSKI:def 1; hence bbx.z in (b1+*(i,{x})).z by A3,A7,FUNCT_7:31; end; suppose A8: z<>i; then bbx.z = bb.z by FUNCT_7:32; then bbx.z in b1.z by A1,A3,A5,CARD_3:9; hence bbx.z in (b1+*(i,{x})).z by A8,FUNCT_7:32; end; end; let o be object; assume o in {p+*(i,x) qua set}; then A9: o = bbx by TARSKI:def 1; dom bbx = I by PARTFUN1:def 2 .= dom (b1+*(i,{x})) by PARTFUN1:def 2; hence thesis by A9,A4,CARD_3:9; end; let o be object; assume o in product(b1+*(i,{x})); then consider u being Function such that A10: u=o and A11: dom u=dom (b1+*(i,{x})) and A12: for z being object st z in dom (b1+*(i,{x})) holds u.z in (b1+*(i,{x }) ).z by CARD_3:def 5; A13: now let z be object; assume A14: z in dom u; then A15: z in I by A11; reconsider zz=z as Element of I by A11,A14; A16: u.z in (b1+*(i,{x})).z by A11,A12,A14; per cases; suppose A17: zz=i; then u.z in {x} by A3,A16,FUNCT_7:31; then u.z = x by TARSKI:def 1; hence u.z = bbx.z by A2,A3,A17,FUNCT_7:31; end; suppose A18: zz<>i; then b1.zz is non empty trivial by PENCIL_1:def 21; then b1.zz is 1-element; then consider o being object 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; bbx.z = bb.z by A18,FUNCT_7:32; then bbx.z in {o} by A2,A3,A15,A19; hence u.z = bbx.z by A20,TARSKI:def 1; end; end; dom u = I by A11,PARTFUN1:def 2 .= dom bbx by PARTFUN1:def 2; then u=bbx by A13; hence thesis by A10,TARSKI:def 1; end; end; definition let I be finite non empty set; let b1,b2 be ManySortedSet of I; func diff(b1,b2) -> Nat equals card {i where i is Element of I: b1.i <> b2.i}; correctness proof {i where i is Element of I: b1.i <> b2.i} c= I proof let a be object; assume a in {i where i is Element of I: b1.i <> b2.i}; then ex i being Element of I st a=i & b1.i<>b2.i; hence thesis; 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 thesis; end; end; theorem Th19: for I being finite non empty 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 finite non empty set; let b1,b2 be ManySortedSet of I; let j be Element of I; set b3=b2+*(j,b1.j); {i where i is Element of I: b1.i <> b2.i} c= I proof let a be object; assume a in {i where i is Element of I: b1.i <> b2.i}; then ex i being Element of I st a=i & b1.i<>b2.i; hence thesis; 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 <> b3.i} c= I proof let a be object; assume a in {i where i is Element of I: b1.i <> b3.i}; then ex i being Element of I st a=i & b1.i<>b3.i; hence thesis; end; then reconsider G={i where i is Element of I: b1.i <> b3.i} as finite set by FINSET_1:1; assume A1: b1.j<>b2.j; A2: F = G \/ {j} proof thus F c= G \/ {j} proof let o be object; assume o in F; then consider i being Element of I such that A3: o=i and A4: b1.i <> b2.i; per cases; suppose i=j; then o in {j} by A3,TARSKI:def 1; hence thesis by XBOOLE_0:def 3; end; suppose i<>j; then b3.i=b2.i by FUNCT_7:32; then i in G by A4; hence thesis by A3,XBOOLE_0:def 3; end; end; let o be object; assume A5: o in G \/ {j}; per cases by A5,XBOOLE_0:def 3; suppose o in G; then consider i being Element of I such that A6: o=i and A7: b1.i <> b3.i; now assume A8: b1.i = b2.i; then i=j by A7,FUNCT_7:32; hence contradiction by A1,A8; end; hence thesis by A6; end; suppose o in {j}; then o=j by TARSKI:def 1; hence thesis by A1; end; end; now assume j in G; then A9: ex jj being Element of I st jj=j & b1.jj <> b3.jj; dom b2=I by PARTFUN1:def 2; hence contradiction by A9,FUNCT_7:31; end; hence thesis by A2,CARD_2:41; end; begin :: The adherence of Segre cosets definition let I be non empty set; let A be PLS-yielding ManySortedSet of I; let B1,B2 be Segre-Coset of A; pred B1 '||' B2 means for x being Point of Segre_Product A st x in B1 ex y being Point of Segre_Product A st y in B2 & x,y are_collinear; end; theorem Th20: 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 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; let A be PLS-yielding ManySortedSet of I; let B1,B2 be Segre-Coset of A such that A1: B1 '||' B2; let f be Collineation of Segre_Product A; let C1,C2 be Segre-Coset of A such that A2: C1=f.:B1 and A3: C2=f.:B2; let x be Point of Segre_Product A; assume x in C1; then consider a being object 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 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; take y=f.b; 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; per cases; suppose a=b; hence thesis by A6,PENCIL_1:def 1; end; suppose a<>b; 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 thesis by PENCIL_1:def 1; end; end; theorem Th21: 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 Segre-like non trivial-yielding 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 being non empty set; let A being PLS-yielding ManySortedSet of I; let B1,B2 being Segre-Coset of A; consider L1 being Segre-like non trivial-yielding 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; thus B1 '||' B2 implies for b1,b2 being Segre-like non trivial-yielding 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 assume A3: B1 '||' B2; consider L2 being Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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 being Segre-like non trivial-yielding ManySortedSubset of Carrier A; assume that A8: B1 = product b1 and A9: B2 = product b2; A10: b1 = L1 by A8,A6,PUA2MSS1:2; thus A11: indx(b1)=indx(b2) proof assume indx(b1)<>indx(b2); then b2.indx(b1) is 1-element by PENCIL_1:12; then consider c2 being object such that A12: b2.indx(b1)={c2} by ZFMISC_1:131; set bl = the Block of A.indx(b1); consider p0 being object such that A13: p0 in B1 by A8,XBOOLE_0:def 1; reconsider p0 as Point of Segre_Product A by A13; reconsider p=p0 as Element of Carrier A by Th6; bl in the topology of A.indx(b1); then 2 c= card bl & card bl c= card (the carrier of (A.indx(b1))) by CARD_1:11,PENCIL_1:def 6; then consider a being object such that A14: a in the carrier of (A.indx(b1)) and A15: a <> c2 by PENCIL_1:3,XBOOLE_1:1; reconsider 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 let i be object; assume A17: i in dom x1; then i in I; then A18: i in dom p by PARTFUN1:def 2; per cases; suppose A19: i=indx(b1); then x1.i = a by A18,FUNCT_7:31; hence x1.i in b1.i by A7,A10,A19; end; suppose i<>indx(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 object 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; 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; reconsider y1=y as Element of Carrier A by Th6; per cases; suppose y=x; then y in B1 /\ B2 by A21,A22,XBOOLE_0:def 4; hence contradiction by A2; end; suppose y<>x; 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 let i be object; assume A26: i in dom y1; then reconsider i5=i as Element of I; per cases; suppose A27: i=indx(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; end; suppose A28: i<>indx(b1); (ex g being Function st g=y1 & dom g = dom b2 & for a being object 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 object 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; 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; 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 proof consider x being object such that A33: x in B1 by A8,XBOOLE_0:def 1; reconsider 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; reconsider y1=y as Element of Carrier A by Th6; reconsider x1=x as Element of Carrier A by Th6; x <> y by A2,A33,A34,XBOOLE_0:def 4; 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; now assume A38: r=indx(b1); A39: now let o be object; assume A40: o in dom b1; then reconsider o1=o as Element of I; per cases; suppose A41: o1=r; 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; end; suppose A42: o1<>r; then b1.o1 is 1-element by A38,PENCIL_1:12; then consider c being object 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; 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; end; hence r<>indx(b1); thus for i being Element of I st i<>r holds b1.i=b2.i proof let i be Element of I; assume A44: i<>r; per cases; suppose i=indx(b1); hence thesis by A7,A5,A10,A32,A11; end; suppose A45: i<>indx(b1); then b2.i is 1-element by A11,PENCIL_1:12; then A46: ex d being object 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 object 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 thesis by A48,A46,A47,TARSKI:def 1; end; end; let c1,c2 being Point of A.r; assume that A49: b1.r={c1} and A50: b2.r={c2}; 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 thesis by A36,A51; end; end; consider L2 being Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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; 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 object 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; then {c2} c= [#](A.r) by A57,Th7; then reconsider c2 as Point of A.r by ZFMISC_1:31; L1.r is 1-element by A54,PENCIL_1:12; then consider c1 being object 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; then {c1} c= [#](A.r) by A58,Th7; then reconsider c1 as Point of A.r by ZFMISC_1:31; A59: now assume A60: c1=c2; A61: now let s be object; assume s in dom L1; then reconsider s1=s as Element of I; per cases; suppose s1=r; hence L1.s=L2.s by A58,A57,A60; end; suppose s1<>r; hence L1.s=L2.s by A55; end; end; dom L1 = I by PARTFUN1:def 2 .= dom L2 by PARTFUN1:def 2; then L1=L2 by A61; then B1 /\ B1 = {} by A2,A1,A52; hence contradiction by A1; 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 being Point of Segre_Product A; 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; then A63: ex x2 being Function st x2=x & dom x2=dom L1 & for o being object st o in dom L1 holds x2.o in L1.o by A1,CARD_3:def 5; A64: now let a be object; assume a in dom L2; then reconsider a1=a as Element of I; per cases; suppose A65: a1=r; 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; end; suppose A66: a1<>r; 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; end; end; take y; dom y1 = I by PARTFUN1:def 2 .= dom L2 by PARTFUN1:def 2; hence y in B2 by A52,A64,CARD_3:def 5; reconsider B=product({x1}+*(r,bb)) as Block of Segre_Product A by Th16; A67: now let s be object; assume s in dom y1; then A68: s in I; then A69: s in dom {x1} & s in dom x1 by PARTFUN1:def 2; per cases; suppose s=r; 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; end; suppose A70: s<>r; 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; 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 let s be object; assume A74: s in dom x1; then A75: s in I; then A76: s in dom {x1} by PARTFUN1:def 2; per cases; suppose A77: s=r; 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; end; suppose s<>r; 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; 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 thesis by PENCIL_1:def 1; end; theorem Th22: for I being finite non empty set for A being PLS-yielding ManySortedSet of I st for i being Element of I holds A.i is connected for i being Element of I for p being Point of A.i for b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1=b2+*(i,{p}) & not p in b2.i 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 & ij+1; assume Di /\ Di1 <> {}; then consider x being object 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 object 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 object 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; end; now let c1,c2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A40: Di = product c1 and A41: Di1 = product c2; 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: c2.indx(b2) is non 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: c1.indx(b2) is non 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; take r=i; thus r<>indx(c1) by A5,A45,PENCIL_1:def 21; thus for j being Element of I st j<>r holds c1.j=c2.j proof let j be Element of I; assume A46: j<>r; hence c1.j = b2.j by A44,FUNCT_7:32 .= c2.j by A42,A46,FUNCT_7:32; end; thus for p1,p2 being Point of A.r st c1.r={p1} & c2.r={p2} holds p1,p2 are_collinear proof let p1,p2 be Point of A.r such that A47: c1.r={p1} and A48: c2.r={p2}; 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 thesis by A10,A12,A22,A49; end; end; hence thesis by A31,Th21; end; end; theorem Th23: for I being finite non empty set for A being PLS-yielding ManySortedSet of I st for i being Element of I holds A.i is connected for B1,B2 being Segre-Coset of A st B1 misses B2 for b1,b2 being Segre-like non trivial-yielding 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 & ic2.i} <> {} by A10; then consider j0 being object 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 object 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; then p in (Carrier A).j by ZFMISC_1:31; then p in [#](A.j) by Th7; then reconsider p as Point of A.j; reconsider c3=c2+*(j,{p}) as Segre-like non trivial-yielding 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 object st c2.j={r} by ZFMISC_1:131; A.indx(c1) is non 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; per cases; suppose A20: product c1 misses product c3; 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 1 by A29,XXREAL_0:1; hence D.(len D)=product c2 by A26,GRAPH_2:16; thus for i being Nat st i in dom D holds D.i is Segre-Coset of A proof let i be Nat; A33: rng D c= rng E \/ rng F by GRAPH_2:17; assume i in dom D; then A34: D.i in rng D by FUNCT_1:3; per cases by A34,A33,XBOOLE_0:def 3; suppose D.i in rng E; then consider i0 being object such that A35: i0 in dom E and A36: D.i = E.i0 by FUNCT_1:def 3; thus thesis by A23,A35,A36; end; suppose D.i in rng F; then consider i0 being object such that A37: i0 in dom F and A38: D.i = F.i0 by FUNCT_1:def 3; thus thesis by A27,A37,A38; end; end; thus for i being Nat st 1<=i & i=len E; then consider k being Nat such that A45: i=len E+k by NAT_1:10; A46: F <> {} by A31; reconsider k as Element of NAT by ORDINAL1:def 12; per cases; suppose A47: k>0; 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 thesis by A28,A52,A51; end; suppose k=0; then Di = F.1 & Di1 = F.(1+1) by A22,A25,A32,A39,A41,A42,A45, GRAPH_2:14,15; hence thesis by A28,A32; end; end; end; end; suppose A53: product c1 meets product c3; not p in c2.j by A12,A15,A17,TARSKI:def 1; hence thesis by A1,A8,A9,A18,A19,A53,Th11,Th22; end; end; end; A54: P[ 0 ] proof let c1,c2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A; 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; A57: now let a be object; assume a in dom c1; then reconsider j=a as Element of I; assume c1.a<>c2.a; then j in {i where i is Element of I: c1.i <> c2.i}; hence contradiction by A56; end; dom c1 = I by PARTFUN1:def 2 .= dom c2 by PARTFUN1:def 2; hence thesis by A55,A57,FUNCT_1:2; end; for n being Nat holds P[n] from NAT_1:sch 2(A54,A5); then A58: P[diff(b1,b2)]; assume indx(b1)=indx(b2); 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 & ix; 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; [#](A.i1) is non empty; then (Carrier A).i1 is non empty by Th7; hence f.i in (Carrier A).i by A30; end; end; Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by PENCIL_1:def 23; hence thesis by A23,A26,A27,CARD_3:def 5; 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 Segre-like non trivial-yielding 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); let B1 being Segre-Coset of A; let b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A; 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; hence thesis by A1,A22,A31,A32,Th24; end; A33: for x being Element of I ex y being Element of I st P[x,y] proof set p0 = the Point of Segre_Product A; reconsider p0 as Element of Carrier A by Th6; let x be Element of I; 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 A.x is non trivial by PENCIL_1:def 18; then reconsider C=[#](A.x) as non trivial set; reconsider b=p+*(x,C) as Segre-like non trivial-yielding ManySortedSubset of Carrier A by PENCIL_1:9,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 object; assume a in product b; then consider f being Function such that A36: a=f and A37: dom f=dom b and A38: for x being object st x in dom b holds f.x in b.x by CARD_3:def 5; dom Carrier A = I by PARTFUN1:def 2; then A39: dom f = dom Carrier A by A37,PARTFUN1:def 2; A40: now let i be object; assume A41: i in dom Carrier A; then reconsider i1=i as Element of I; A42: f.i in b.i by A37,A38,A39,A41; per cases; suppose i1=x; hence f.i in (Carrier A).i by A34,A42,Th7; end; suppose i1<>x; 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; [#](A.i1) is non empty; then (Carrier A).i1 is non empty by Th7; hence f.i in (Carrier A).i by A43; end; end; Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by PENCIL_1:def 23; hence thesis by A36,A39,A40,CARD_3:def 5; 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 Segre-like non trivial-yielding 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); let B1 being Segre-Coset of A; let b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A; assume B1 = product b1 & f.:B1 = product b2 & indx(b1)=x; hence thesis by A1,A35,A44,Th24; end; A45: for x,y,y9 being Element of I st P[x,y] & P[x,y9] holds y=y9 proof let x,y,y9 be Element of I; assume that A46: for B1 being Segre-Coset of A for b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 = product b2 holds indx(b1)=x implies indx(b2)=y and A47: for B1 being Segre-Coset of A for b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 = product b2 holds indx(b1)=x implies indx(b2)=y9; consider b1 being Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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 thesis by A47,A48,A50; end; thus ex f being Permutation of I st for x,y being Element of I holds f.x=y iff P[x,y] from TRANSGEO:sch 1(A33,A20,A2,A45); end; definition let I be finite non empty set; let A be PLS-yielding ManySortedSet of I such that A1: 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: for i,j being Element of I holds it.i=j iff for B1 being Segre-Coset of A for b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 = product b2 holds indx(b1)=i implies indx(b2)=j; existence by A1,Th25; uniqueness proof let s,t be Permutation of I such that A2: for i,j being Element of I holds s.i=j iff for B1 being Segre-Coset of A for b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 = product b2 holds indx(b1)=i implies indx(b2)=j and A3: for i,j being Element of I holds t.i=j iff for B1 being Segre-Coset of A for b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st B1 = product b1 & f.:B1 = product b2 holds indx(b1)=i implies indx(b2)=j; A4: now let a be object; assume a in I; 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 Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A5: indx(b1)=i and A6: product b1 is Segre-Coset of A by Th8; reconsider B1=product b1 as Segre-Coset of A by A6; reconsider fB=f.:B1 as Segre-Coset of A by A1,PENCIL_2:24; consider b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A7: fB = product b2 and b2.indx(b2) = [#](A.indx(b2)) by PENCIL_2:def 2; j1 = indx(b2) by A2,A5,A7 .= j2 by A3,A5,A7; hence s.a=t.a; end; thus s=t by A4; end; end; begin :: Canonical embeddings and automorphisms of Segre product definition let I be finite non empty set; let A be PLS-yielding ManySortedSet of I such that A1: for i being Element of I holds A.i is strongly_connected; let f be Collineation of Segre_Product A; let b1 be Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A2: 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: it is isomorphic & for a being ManySortedSet of I st a is Point of Segre_Product A & a in product b1 for b being ManySortedSet of I st b=f.a holds b.(permutation_of_indices(f).indx(b1))= it.(a.indx(b1)); existence proof reconsider B1=product b1 as Segre-Coset of A by A2; set s=permutation_of_indices(f); set i=indx(b1); defpred P[object,object] means for J being ManySortedSet of I st J in f.:( product(b1+*(i,{$1}))) holds $2 = J.(s.i); set B = the carrier of A.i; set t=s; reconsider B2=f.:B1 as Segre-Coset of A by A1,PENCIL_2:24; consider b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A3: product b2=B2 and A4: b2.indx(b2) = [#](A.indx(b2)) by PENCIL_2:def 2; set j=indx(b2); A5: f is bijective by PENCIL_2:def 4; then A6: f"B2 c= B1 by FUNCT_1:82; A7: Segre_Product A = TopStruct(#product Carrier A, Segre_Blocks A#) by PENCIL_1:def 23; A8: for x being object st x in B ex y being object st P[x,y] proof let x be object; consider bb being object such that A9: bb in B1 by XBOOLE_0:def 1; A10: ex bf being Function st bf=bb & dom bf=dom b1 & for o being object st o in dom b1 holds bf.o in b1.o by A9,CARD_3:def 5; A11: dom b1=I by PARTFUN1:def 2; then reconsider bb as ManySortedSet of I by A10,PARTFUN1:def 2 ,RELAT_1:def 18; set bbx=bb+*(i,x); A12: {bbx qua set} = product(b1+*(i,{x})) proof thus {bbx qua set} c= product(b1+*(i,{x})) proof A13: now let z be object; assume z in dom (b1+*(i,{x})); then A14: z in I; then A15: z in dom bb by PARTFUN1:def 2; per cases; suppose A16: z=i; then bbx.z = x by A15,FUNCT_7:31; then bbx.z in {x} by TARSKI:def 1; hence bbx.z in (b1+*(i,{x})).z by A11,A16,FUNCT_7:31; end; suppose A17: z<>i; then bbx.z = bb.z by FUNCT_7:32; then bbx.z in b1.z by A9,A11,A14,CARD_3:9; hence bbx.z in (b1+*(i,{x})).z by A17,FUNCT_7:32; end; end; let o be object; assume o in {bbx qua set}; then A18: o = bbx by TARSKI:def 1; dom bbx = I by PARTFUN1:def 2 .= dom (b1+*(i,{x})) by PARTFUN1:def 2; hence thesis by A18,A13,CARD_3:9; end; let o be object; assume o in product(b1+*(i,{x})); then consider u being Function such that A19: u=o and A20: dom u=dom (b1+*(i,{x})) and A21: for z being object st z in dom (b1+*(i,{x})) holds u.z in (b1+*( i,{x}) ).z by CARD_3:def 5; A22: now let z be object; assume A23: z in dom u; then A24: z in I by A20; reconsider zz=z as Element of I by A20,A23; A25: u.z in (b1+*(i,{x})).z by A20,A21,A23; per cases; suppose A26: zz=i; then u.z in {x} by A11,A25,FUNCT_7:31; then u.z = x by TARSKI:def 1; hence u.z = bbx.z by A10,A11,A26,FUNCT_7:31; end; suppose A27: zz<>i; then b1.zz is non empty trivial by PENCIL_1:def 21; then b1.zz is 1-element; then consider o being object such that A28: b1.z = {o} by ZFMISC_1:131; u.z in b1.z by A25,A27,FUNCT_7:32; then A29: u.z = o by A28,TARSKI:def 1; bbx.z = bb.z by A27,FUNCT_7:32; then bbx.z in {o} by A10,A11,A24,A28; hence u.z = bbx.z by A29,TARSKI:def 1; end; end; dom u = I by A20,PARTFUN1:def 2 .= dom bbx by PARTFUN1:def 2; then u=bbx by A22; hence thesis by A19,TARSKI:def 1; end; assume A30: x in B; A31: now let o be object; assume A32: o in dom Carrier A; then reconsider u=o as Element of I; per cases; suppose A33: u=i; then bbx.u in [#](A.i) by A30,A10,A11,FUNCT_7:31; hence bbx.o in (Carrier A).o by A33,Th7; end; suppose A34: u<>i; b1 c= Carrier A by PBOOLE:def 18; then A35: b1.o c= (Carrier A).o by A32; bbx.u = bb.u by A34,FUNCT_7:32; then bbx.u in b1.u by A9,A11,CARD_3:9; hence bbx.o in (Carrier A).o by A35; end; end; dom bbx= I by PARTFUN1:def 2 .= dom Carrier A by PARTFUN1:def 2; then reconsider bbx1=bbx as Point of Segre_Product A by A7,A31,CARD_3:9; reconsider fbbx=f.bbx1 as ManySortedSet of I by PENCIL_1:14; take fbbx.(s.i); dom f = the carrier of Segre_Product A by FUNCT_2:def 1; then bbx1 in dom f; then A36: Im(f,bbx) = {f.bbx} by FUNCT_1:59; let J be ManySortedSet of I; assume J in f.:product(b1+*(i,{x})); hence thesis by A12,A36,TARSKI:def 1; end; consider M being Function such that A37: dom M = B & for x being object st x in B holds P[x,M.x] from CLASSES1:sch 1(A8); A38: dom f = the carrier of Segre_Product A by FUNCT_2:def 1; then B1 c= f"B2 by FUNCT_1:76; then A39: f"B2 = B1 by A6; rng M c= the carrier of A.(t.i) proof let x be object; assume x in rng M; then consider o being object such that A40: o in dom M and A41: x=M.o by FUNCT_1:def 3; reconsider o as Point of A.i by A37,A40; consider p being ManySortedSet of I such that A42: p in product b1 and A43: {p+*(i,o) qua set} = product(b1+*(i,{o})) by Th18; reconsider pio=p+*(i,o) as Point of Segre_Product A by A2,A42,PENCIL_1:25 ; reconsider J=f.pio as ManySortedSet of I by PENCIL_1:14; Im(f,p+*(i,o)) = {f.pio} by A38,FUNCT_1:59; then A44: J in f.:(product(b1+*(i,{o}))) by A43,TARSKI:def 1; s.i in I; then s.i in dom Carrier A by PARTFUN1:def 2; then J.(s.i) in (Carrier A).(s.i) by A7,CARD_3:9; then J.(s.i) in [#](A.(s.i)) by Th7; hence thesis by A37,A41,A44; end; then reconsider M as Function of A.i,A.(t.i) by A37,FUNCT_2:def 1 ,RELSET_1:4; set m=M; A45: indx(b2)=s.i by A1,A3,Def3; A46: m is one-to-one proof let x1,x2 be object; assume that A47: x1 in dom m & x2 in dom m and A48: m.x1 = m.x2; reconsider o1=x1,o2=x2 as Point of A.i by A47; consider p1 being ManySortedSet of I such that A49: p1 in product b1 and A50: {p1+*(i,o1) qua set} = product(b1+*(i,{o1})) by Th18; reconsider p1io=p1+*(i,o1) as Point of Segre_Product A by A2,A49, PENCIL_1:25; reconsider J1=f.p1io as ManySortedSet of I by PENCIL_1:14; consider p2 being ManySortedSet of I such that A51: p2 in product b1 and A52: {p2+*(i,o2) qua set} = product(b1+*(i,{o2})) by Th18; A53: dom b1=I by PARTFUN1:def 2; A54: dom p1=I by PARTFUN1:def 2; A55: now let o be object; assume A56: o in I; per cases; suppose A57: o=indx(b1); then p1+*(i,o1).o = o1 by A54,FUNCT_7:31; then p1+*(i,o1).o in [#](A.i); hence p1+*(i,o1).o in b1.o by A2,A57,Th10; end; suppose o<>indx(b1); then p1+*(i,o1).o = p1.o by FUNCT_7:32; hence p1+*(i,o1).o in b1.o by A49,A53,A56,CARD_3:9; end; end; dom (p1+*(i,o1))=I by PARTFUN1:def 2; then p1io in product b1 by A53,A55,CARD_3:9; then A58: J1 in B2 by A38,FUNCT_1:def 6; reconsider p2io=p2+*(i,o2) as Point of Segre_Product A by A2,A51, PENCIL_1:25; reconsider J2=f.p2io as ManySortedSet of I by PENCIL_1:14; Im(f,p2+*(i,o2)) = {f.p2io} by A38,FUNCT_1:59; then J2 in f.:(product(b1+*(i,{o2}))) by A52,TARSKI:def 1; then A59: M.o2 = J2.(s.i) by A37; dom p1 = I by PARTFUN1:def 2; then A60: p1+*(i,o1).i = o1 by FUNCT_7:31; A61: dom b1=I by PARTFUN1:def 2; A62: dom p2=I by PARTFUN1:def 2; A63: now let o be object; assume A64: o in I; per cases; suppose A65: o=indx(b1); then p2+*(i,o2).o = o2 by A62,FUNCT_7:31; then p2+*(i,o2).o in [#](A.i); hence p2+*(i,o2).o in b1.o by A2,A65,Th10; end; suppose o<>indx(b1); then p2+*(i,o2).o = p2.o by FUNCT_7:32; hence p2+*(i,o2).o in b1.o by A51,A61,A64,CARD_3:9; end; end; dom (p2+*(i,o2))=I by PARTFUN1:def 2; then p2io in product b1 by A61,A63,CARD_3:9; then A66: J2 in B2 by A38,FUNCT_1:def 6; Im(f,p1+*(i,o1)) = {f.p1io} by A38,FUNCT_1:59; then A67: J1 in f.:(product(b1+*(i,{o1}))) by A50,TARSKI:def 1; A68: now let o be object; assume o in I; then reconsider l=o as Element of I; per cases; suppose l=indx(b2); hence J1.o=J2.o by A45,A37,A48,A67,A59; end; suppose l<>indx(b2); hence J1.o=J2.o by A3,A58,A66,PENCIL_1:23; end; end; dom p2 = I by PARTFUN1:def 2; then A69: p2+*(i,o2).i = o2 by FUNCT_7:31; J1=J2 by A68; hence thesis by A38,A5,A60,A69,FUNCT_1:def 4; end; f is bijective by PENCIL_2:def 4; then A70: rng f = the carrier of Segre_Product A by FUNCT_2:def 3; A71: f" = (f qua Function)" by A5,TOPS_2:def 4; the carrier of A.(t.i) c= rng m proof let x be object; assume x in the carrier of A.(t.i); then reconsider x1=x as Point of A.(t.i); consider p0 being ManySortedSet of I such that A72: p0 in product b2 and {p0+*(indx(b2),x1) qua set} = product(b2+*(indx(b2),{x1})) by A45,Th18; reconsider p=p0+*(indx(b2),x1) as Point of Segre_Product A by A3,A45,A72, PENCIL_1:25; reconsider p1=p as ManySortedSet of I; reconsider q=f".p as ManySortedSet of I by PENCIL_1:14; A73: p=f.(f".p) by A70,A5,A71,FUNCT_1:35; A74: dom b1=I by PARTFUN1:def 2; A75: now let o be object; assume o in I; then reconsider l=o as Element of I; per cases; suppose l=i; then b1+*(i,{q.i}).l = {q.o} by A74,FUNCT_7:31; hence q.o in b1+*(i,{q.i}).o by TARSKI:def 1; end; suppose l<>i; then A76: b1+*(i,{q.i}).l = b1.l by FUNCT_7:32; A77: dom b2 = I by PARTFUN1:def 2; A78: dom p0 = I by PARTFUN1:def 2; A79: now let o be object; assume A80: o in I; per cases; suppose A81: o=indx(b2); then p1.o = x1 by A78,FUNCT_7:31; then p1.o in the carrier of A.(t.i); hence p1.o in b2.o by A1,A3,A4,A81,Def3; end; suppose o<>indx(b2); then p1.o = p0.o by FUNCT_7:32; hence p1.o in b2.o by A72,A77,A80,CARD_3:9; end; end; dom p1 = I by PARTFUN1:def 2; then p in product b2 by A77,A79,CARD_3:9; then consider q0 being object such that A82: q0 in dom f and A83: q0 in B1 and A84: p=f.q0 by A3,FUNCT_1:def 6; q=q0 by A38,A5,A73,A82,A84,FUNCT_1:def 4; hence q.o in b1+*(i,{q.i}).o by A74,A76,A83,CARD_3:9; end; end; I = dom Carrier A by PARTFUN1:def 2; then q.i in (Carrier A).i by A7,CARD_3:9; then A85: q.i in [#](A.i) by Th7; dom q = I & dom (b1+*(i,{q.i})) = I by PARTFUN1:def 2; then q in product(b1+*(i,{q.i})) by A75,CARD_3:9; then p0+*(indx(b2),x1) in f.:(product(b1+*(i,{q.i}))) by A38,A73, FUNCT_1:def 6; then dom p0 = I & m.(q.i) = p0+*(indx(b2),x1).(s.i) by A37,A85, PARTFUN1:def 2; then dom m = the carrier of A.i & m.(q.i)=x by A45,FUNCT_2:def 1 ,FUNCT_7:31; hence thesis by A85,FUNCT_1:3; end; then A86: rng m = the carrier of A.(t.i); then m is onto by FUNCT_2:def 3; then A87: m" = (m qua Function)" by A46,TOPS_2:def 4; A88: m" is open proof let S0 be Subset of A.(t.i); assume S0 is open; then reconsider S=S0 as Block of A.(t.i) by PRE_TOPC:def 2; reconsider L=product(b2+*(j,S)) as Block of Segre_Product A by A45,Th12; reconsider K=f"L as Block of Segre_Product A; consider k being Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A89: K = product k and A90: k.indx(k) is Block of A.indx(k) by PENCIL_1:24; A91: dom b2 = I by PARTFUN1:def 2; A92: now let x be object; assume x in I; per cases; suppose A93: x=j; then b2+*(j,S).x = S by A91,FUNCT_7:31; then b2+*(j,S).x c= the carrier of A.(t.i); hence b2+*(j,S).x c= b2.x by A1,A3,A4,A93,Def3; end; suppose x<>j; hence b2+*(j,S).x c= b2.x by FUNCT_7:32; end; end; dom (b2+*(j,S)) = I by PARTFUN1:def 2; then L c= product b2 by A91,A92,CARD_3:27; then product b1 /\ product k = K by A3,A39,A89,RELAT_1:143,XBOOLE_1:28; then A94: 2 c= card(product b1 /\ product k) by PENCIL_1:def 6; then A95: indx(k)=i by PENCIL_1:26; m"S=k.indx(k) proof thus m"S c= k.indx(k) proof let o be object; A96: dom b2 = I by PARTFUN1:def 2; assume A97: o in m"S; then reconsider u=o as Point of A.i; consider p being ManySortedSet of I such that A98: p in product b1 and A99: {p+*(i,u) qua set} = product(b1+*(i,{u})) by Th18; reconsider q=p+*(i,u) as Point of Segre_Product A by A2,A98, PENCIL_1:25; reconsider fq=f.q as ManySortedSet of I by PENCIL_1:14; Im(f,p+*(i,u)) = {f.q} by A38,FUNCT_1:59; then A100: fq in f.:product(b1+*(i,{u})) by A99,TARSKI:def 1; product(b1+*(i,{u})) c= product b1 proof let a be object; A101: dom b1 = I by PARTFUN1:def 2; assume a in product(b1+*(i,{u})); then consider g being Function such that A102: a=g and A103: dom g=dom (b1+*(i,{u})) and A104: for o being object st o in dom (b1+*(i,{u})) holds g.o in b1+*(i,{u}) .o by CARD_3:def 5; A105: dom g = I by A103,PARTFUN1:def 2; now let o be object; assume o in I; then A106: g.o in b1+*(i,{u}).o by A103,A104,A105; per cases; suppose A107: o=i; then g.o in {u} by A101,A106,FUNCT_7:31; then g.o in [#](A.i); hence g.o in b1.o by A2,A107,Th10; end; suppose o<>i; hence g.o in b1.o by A106,FUNCT_7:32; end; end; hence thesis by A102,A105,A101,CARD_3:9; end; then A108: f.:product(b1+*(i,{u})) c= product b2 by A3,RELAT_1:123; m.o in S by A97,FUNCT_1:def 7; then A109: fq.(s.i) in S by A37,A100; A110: now let o be object; assume A111: o in I; per cases; suppose o=j; hence fq.o in b2+*(j,S).o by A45,A109,A96,FUNCT_7:31; end; suppose o<>j; then b2+*(j,S).o = b2.o by FUNCT_7:32; hence fq.o in b2+*(j,S).o by A100,A108,A96,A111,CARD_3:9; end; end; dom fq = I & dom (b2+*(j,S)) = I by PARTFUN1:def 2; then fq in L by A110,CARD_3:9; then dom k = I & q in K by A38,FUNCT_1:def 7,PARTFUN1:def 2; then dom p = I & p+*(i,u).i in k.i by A89,CARD_3:9,PARTFUN1:def 2; hence thesis by A95,FUNCT_7:31; end; let o be object; assume A112: o in k.indx(k); k.indx(k) in the topology of A.i by A90,A95; then reconsider u=o as Point of A.i by A112; consider p0 being ManySortedSet of I such that A113: p0 in product b1 and A114: {p0+*(i,u) qua set} = product(b1+*(i,{u})) by Th18; reconsider p=p0+*(i,u) as Point of Segre_Product A by A2,A113, PENCIL_1:25; reconsider fp=f.p as ManySortedSet of I by PENCIL_1:14; A115: dom b1 = I by PARTFUN1:def 2; A116: dom p0 = I by PARTFUN1:def 2; A117: now let a be object; assume A118: a in I; per cases; suppose a=i; hence p0+*(i,u).a in k.a by A95,A112,A116,FUNCT_7:31; end; suppose A119: a<>i; then p0+*(i,u).a = p0.a by FUNCT_7:32; then p0+*(i,u).a in b1.a by A113,A115,A118,CARD_3:9; hence p0+*(i,u).a in k.a by A94,A119,PENCIL_1:26; end; end; dom (p0+*(i,u)) = I & dom k = I by PARTFUN1:def 2; then p in K by A89,A117,CARD_3:9; then dom (b2+*(j,S)) = I & fp in L by FUNCT_1:def 7,PARTFUN1:def 2; then dom b2 = I & fp.j in b2+*(j,S).j by CARD_3:9,PARTFUN1:def 2; then A120: fp.(s.i) in S by A45,FUNCT_7:31; Im(f,p0+*(i,u)) = {f.p} by A38,FUNCT_1:59; then fp in f.:product(b1+*(i,{u})) by A114,TARSKI:def 1; then m.u = fp.(s.i) by A37; hence thesis by A37,A120,FUNCT_1:def 7; end; then m".:S is Block of A.i by A46,A87,A90,A95,FUNCT_1:85; hence thesis by PRE_TOPC:def 2; end; A121: m is open proof let S0 be Subset of A.i; assume S0 is open; then reconsider S=S0 as Block of A.i by PRE_TOPC:def 2; reconsider L=product(b1+*(i,S)) as Block of Segre_Product A by Th12; reconsider K=f.:L as Block of Segre_Product A; consider k being Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A122: K = product k and A123: k.indx(k) is Block of A.indx(k) by PENCIL_1:24; A124: dom b1 = I by PARTFUN1:def 2; A125: now let x be object; assume x in I; per cases; suppose A126: x=i; then b1+*(i,S).x = S by A124,FUNCT_7:31; then b1+*(i,S).x c= [#](A.i); hence b1+*(i,S).x c= b1.x by A2,A126,Th10; end; suppose x<>i; hence b1+*(i,S).x c= b1.x by FUNCT_7:32; end; end; dom (b1+*(i,S)) = I by PARTFUN1:def 2; then A127: L c= product b1 by A124,A125,CARD_3:27; then product b2 /\ product k = K by A3,A122,RELAT_1:123,XBOOLE_1:28; then 2 c= card(product b2 /\ product k) by PENCIL_1:def 6; then A128: indx(k)=t.i by A45,PENCIL_1:26; A129: dom k = I by PARTFUN1:def 2; m.:S=k.indx(k) proof thus m.:S c= k.indx(k) proof let o be object; A130: dom b1 = I by PARTFUN1:def 2; assume o in m.:S; then consider u being object such that A131: u in dom m and A132: u in S and A133: o=m.u by FUNCT_1:def 6; reconsider u as Point of A.i by A131; consider p0 being ManySortedSet of I such that A134: p0 in product b1 and A135: {p0+*(indx(b1),u) qua set} = product(b1+*(indx(b1),{u})) by Th18; reconsider p=p0+*(indx(b1),u) as Point of Segre_Product A by A2,A134, PENCIL_1:25; reconsider q=f.p as ManySortedSet of I by PENCIL_1:14; Im(f,p0+*(indx(b1),u)) = {f.p} by A38,FUNCT_1:59; then q in f.:product(b1+*(indx(b1),{u})) by A135,TARSKI:def 1; then A136: m.u = q.(s.i) by A37; A137: dom p0 = I by PARTFUN1:def 2; A138: now let a be object; assume A139: a in I; per cases; suppose A140: a=i; then p0+*(i,u).a = u by A137,FUNCT_7:31; hence p0+*(i,u).a in b1+*(i,S).a by A132,A130,A140,FUNCT_7:31; end; suppose A141: a<>i; then p0+*(i,u).a = p0.a by FUNCT_7:32; then p0+*(i,u).a in b1.a by A134,A130,A139,CARD_3:9; hence p0+*(i,u).a in b1+*(i,S).a by A141,FUNCT_7:32; end; end; dom (p0+*(i,u)) = I & dom (b1+*(i,S)) = I by PARTFUN1:def 2; then p in L by A138,CARD_3:9; then q in product k by A38,A122,FUNCT_1:def 6; hence thesis by A129,A128,A133,A136,CARD_3:9; end; let o be object; assume A142: o in k.indx(k); k.indx(k) in the topology of A.(s.i) by A123,A128; then reconsider u=o as Point of A.(s.i) by A142; consider p0 being ManySortedSet of I such that A143: p0 in product k and {p0+*(s.i,u) qua set} = product(k+*(s.i,{u})) by A128,Th18; K in the topology of Segre_Product A; then reconsider p=p0+*(s.i,u) as Point of Segre_Product A by A122,A143,PENCIL_1:25; reconsider q=f".p as ManySortedSet of I by PENCIL_1:14; A144: dom k = I by PARTFUN1:def 2; A145: dom p0 = I by PARTFUN1:def 2; A146: now let z be object; assume A147: z in I; per cases; suppose z=s.i; hence p0+*(s.i,u).z in k.z by A128,A142,A145,FUNCT_7:31; end; suppose z<>s.i; then p0+*(s.i,u).z = p0.z by FUNCT_7:32; hence p0+*(s.i,u).z in k.z by A143,A144,A147,CARD_3:9; end; end; A148: p=f.q by A70,A5,A71,FUNCT_1:35; dom (p0+*(s.i,u)) = I by PARTFUN1:def 2; then p in f.:L by A122,A144,A146,CARD_3:9; then ex qq being object st qq in dom f & qq in L & p=f.qq by FUNCT_1:def 6; then A149: q in L by A38,A5,A148,FUNCT_1:def 4; dom(b1+*(i,S)) = I by PARTFUN1:def 2; then q.i in b1+*(i,S).i by A149,CARD_3:9; then A150: q.i in S by A124,FUNCT_7:31; then reconsider qi=q.i as Point of A.i; consider q0 being ManySortedSet of I such that A151: q0 in product b1 and A152: {q0+*(i,qi) qua set} = product(b1+*(i,{qi})) by Th18; A153: dom q0 = I by PARTFUN1:def 2; A154: now let a be object; assume a in I; per cases; suppose a=i; hence q0+*(i,qi).a = q.a by A153,FUNCT_7:31; end; suppose A155: a<>i; then q0+*(i,qi).a = q0.a by FUNCT_7:32; hence q0+*(i,qi).a = q.a by A127,A149,A151,A155,PENCIL_1:23; end; end; q0+*(i,qi) = q by A154; then Im(f,q0+*(i,qi))={f.q} by A38,FUNCT_1:59; then p in f.:product(b1+*(i,{qi})) by A148,A152,TARSKI:def 1; then m.(q.i) = p0+*(s.i,u).(s.i) by A37; then m.(q.i) = o by A145,FUNCT_7:31; hence thesis by A37,A150,FUNCT_1:def 6; end; hence thesis by A123,A128,PRE_TOPC:def 2; end; take M; A156: m is onto by A86,FUNCT_2:def 3; then m" is bijective by A46,PENCIL_2:12; hence m is isomorphic by A46,A156,A121,A88,PENCIL_2:def 4; let a be ManySortedSet of I such that A157: a is Point of Segre_Product A and A158: a in product b1; dom Carrier A = I by PARTFUN1:def 2; then a.i in (Carrier A).i by A7,A157,CARD_3:9; then a.i in [#](A.i) by Th7; then reconsider ai=a.i as Point of A.i; A159: dom b1 = I by PARTFUN1:def 2; A160: now let o be object; assume A161: o in I; per cases; suppose A162: o=i; then b1+*(i,{ai}).o = {ai} by A159,FUNCT_7:31; hence a.o in b1+*(i,{ai}).o by A162,TARSKI:def 1; end; suppose o<>i; then b1+*(i,{ai}).o = b1.o by FUNCT_7:32; hence a.o in b1+*(i,{ai}).o by A158,A159,A161,CARD_3:9; end; end; dom a = I & dom (b1+*(i,{ai})) = I by PARTFUN1:def 2; then A163: a in product(b1+*(i,{ai})) by A160,CARD_3:9; let b be ManySortedSet of I; assume b=f.a; then b in f.:product(b1+*(i,{ai})) by A38,A157,A163,FUNCT_1:def 6; hence thesis by A37; end; uniqueness proof set i=indx(b1); set s=permutation_of_indices(f); let f1,f2 be Function of A.i,A.(permutation_of_indices(f).i) such that f1 is isomorphic and A164: for a being ManySortedSet of I st a is Point of Segre_Product A & a in product b1 for b being ManySortedSet of I st b=f.a holds b.(s.i)=f1.(a.i ) and f2 is isomorphic and A165: for a being ManySortedSet of I st a is Point of Segre_Product A & a in product b1 for b being ManySortedSet of I st b=f.a holds b.(s.i)=f2.(a.i ); A166: now let x be object; consider p being object such that A167: p in product b1 by XBOOLE_0:def 1; assume x in dom f1; then reconsider x0=x as Point of A.i; reconsider p as Point of Segre_Product A by A2,A167; reconsider P=p as ManySortedSet of I by PENCIL_1:14; set a=P+*(i,x0); reconsider a1=a as Point of Segre_Product A by PENCIL_1:25; A168: dom b1 = I by PARTFUN1:def 2; A169: dom P = I by PARTFUN1:def 2; A170: now let e be object; assume A171: e in I; per cases; suppose A172: e=i; then a.e = x0 by A169,FUNCT_7:31; then a.e in [#](A.i); hence a.e in b1.e by A2,A172,Th10; end; suppose e<>i; then a.e = P.e by FUNCT_7:32; hence a.e in b1.e by A167,A168,A171,CARD_3:9; end; end; reconsider b=f.a1 as ManySortedSet of I by PENCIL_1:14; dom P = I by PARTFUN1:def 2; then A173: a.i=x by FUNCT_7:31; dom a = I by PARTFUN1:def 2; then A174: a in product b1 by A168,A170,CARD_3:9; then f2.(a.i)=b.(s.i) by A165; hence f1.x = f2.x by A164,A174,A173; end; dom f1 = the carrier of A.i by FUNCT_2:def 1 .= dom f2 by FUNCT_2:def 1; hence f1=f2 by A166; end; end; theorem Th26: for I being finite non empty set for A being PLS-yielding ManySortedSet of I st for i being Element of I holds A.i is strongly_connected for f being Collineation of Segre_Product A for B1,B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 for b1,b2 being Segre-like non trivial-yielding ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds canonical_embedding(f,b1) = canonical_embedding(f,b2) proof let I be finite non empty set; let A be PLS-yielding ManySortedSet of I such that A1: for i being Element of I holds A.i is strongly_connected; let f be Collineation of Segre_Product A; let B1,B2 be Segre-Coset of A such that A2: B1 misses B2 and A3: B1 '||' B2; let b1,b2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A4: product b1 = B1 and A5: product b2 = 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 Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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 b2.r is trivial by A6,A9,PENCIL_1:def 21; then consider c2 being object 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; then A21: {c2} c= [#](A.r) by A20,Th7; let o be object; consider p0 being object such that A22: p0 in product b1 by XBOOLE_0:def 1; assume o in the carrier of A.i; then reconsider u=o as Point of A.i; 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+*(i,u); reconsider q1=q as Point of Segre_Product A by PENCIL_1:25; b1.r is trivial by A9,PENCIL_1:def 21; then consider c1 being object 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; then {c1} c= [#](A.r) by A23,Th7; then reconsider c1 as Point of A.r by ZFMISC_1:31; reconsider c2 as Point of A.r by A21,ZFMISC_1:31; set t=q+*(r,c2); q is Point of Segre_Product A by PENCIL_1:25; then reconsider t1=t as Point of Segre_Product A by PENCIL_1:25; per cases; suppose A24: c1<>c2; q.r = p.r by A9,FUNCT_7:32; then q.r in b1.r by A18,A22,CARD_3:9; then A25: q.r = c1 by A23,TARSKI:def 1; dom q = I by PARTFUN1:def 2; then A26: t.r=c2 by FUNCT_7:31; now let q3,t3 be ManySortedSet of I such that A27: q3=q1 & t3=t1; take r; 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; let j be Element of I; assume j<>r; hence q3.j = t3.j by A27,FUNCT_7:32; 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 let a be object; assume A32: a in I; per cases; suppose a=i; then q.a = u & b1.a = [#](A.i) by A4,A30,Th10,FUNCT_7:31; hence q.a in b1.a; end; suppose a<>i; then q.a = p.a by FUNCT_7:32; hence q.a in b1.a by A22,A29,A32,CARD_3:9; end; end; A33: dom q = I by PARTFUN1:def 2; then A34: q in product b1 by A29,A31,CARD_3:9; A35: now let a be object; assume A36: a in I; per cases; suppose A37: a=r; then t.a = c2 by A33,FUNCT_7:31; hence t.a in b2.a by A20,A37,TARSKI:def 1; end; suppose A38: a<>r; then t.a = q.a by FUNCT_7:32; then t.a in b1.a by A31,A36; hence t.a in b2.a by A10,A36,A38; end; end; dom t = I & dom b2 = I by PARTFUN1:def 2; then A39: t in product b2 by A35,CARD_3:9; then A40: canonical_embedding(f,b2).(t.i)=ft.(permutation_of_indices(f) .i) by A1,A5,A6,Def4; A41: f.q1 <> f.t1 by A17,A7,A24,A25,A26,FUNCT_1:def 4; A42: now 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.j<>ft.j; then A44: j=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 let o be object; assume o in I; then reconsider o1=o as Element of I; per cases; suppose o1=j; hence fq.o in b4.o by A14,A15,A13,A16,A46,A47,CARD_3:9; end; suppose o1<>j; 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; 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; end; A50: j=permutation_of_indices(f).i by A1,A4,A14,Def3; dom p = I by PARTFUN1:def 2; then A51: q.i=o by FUNCT_7:31; then t.i=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; end; suppose A52: c1=c2; A53: now let o be object; assume o in I; then reconsider o1=o as Element of I; per cases; suppose r=o1; hence b1.o=b2.o by A23,A20,A52; end; suppose r<>o1; hence b1.o=b2.o by A10; 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; end; end; dom canonical_embedding(f,b1) = the carrier of A.i & dom canonical_embedding (f,b2) = the carrier of A.i by A6,FUNCT_2:def 1; hence thesis by A19; end; theorem Th27: for I being finite non empty set for A being PLS-yielding ManySortedSet of I st for i being Element of I holds A.i is strongly_connected for f being Collineation of Segre_Product A for b1,b2 being Segre-like non trivial-yielding 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 finite non empty set; let A be PLS-yielding ManySortedSet of I such that A1: for i being Element of I holds A.i is strongly_connected; A2: now let o be Element of I; A.o is strongly_connected by A1; hence A.o is connected by Th4; end; let f be Collineation of Segre_Product A; let b1,b2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A3: product b1 is Segre-Coset of A & product b2 is Segre-Coset of A and A4: indx(b1)=indx(b2); reconsider B1=product b1, B2=product b2 as Segre-Coset of A by A3; per cases; suppose B1 misses 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 Function of A.i,A.(permutation_of_indices(f ).i) means :Def5: for b being Segre-like non trivial-yielding ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx(b)=i holds it= canonical_embedding(f,b); existence proof consider L being Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A2: indx(L)=i and A3: 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 A2; take n; let b be Segre-like non trivial-yielding ManySortedSubset of Carrier A; assume product b is Segre-Coset of A & indx(b)=i; hence thesis by A1,A2,A3,Th27; end; uniqueness proof let n1,n2 be Function of A.i,A.(permutation_of_indices(f).i) such that A4: for b being Segre-like non trivial-yielding ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx(b)=i holds n1= canonical_embedding(f,b) and A5: for b being Segre-like non trivial-yielding ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx(b)=i holds n2= canonical_embedding(f,b); consider L being Segre-like non trivial-yielding ManySortedSubset of Carrier A such that A6: indx(L)=i & product L is Segre-Coset of A by Th8; thus n1=canonical_embedding(f,L) by A4,A6 .= n2 by A5,A6; end; end; theorem for I being finite non empty set for A being PLS-yielding ManySortedSet of I st for i being Element of I holds A.i is strongly_connected for f being Collineation of Segre_Product A ex s being Permutation of I, 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 for b being ManySortedSet of I st b=f.p 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 finite non empty set; let A be PLS-yielding ManySortedSet of I such that A1: for i being Element of I holds A.i is strongly_connected; let f be Collineation of Segre_Product A; set s=permutation_of_indices(f); take s; defpred P[object,object] means for i being Element of I st i=$1 holds $2= canonical_embedding(f,i); A2: for i being object st i in I ex j being object st P[i,j] proof let i be object; assume i in I; then reconsider i1=i as Element of I; P[i1,canonical_embedding(f,i1)]; hence thesis; end; consider B being ManySortedSet of I such that A3: for i being object st i in I holds P[i,B.i] from PBOOLE:sch 3(A2); now let x be object; assume x in dom B; then reconsider y=x as Element of I; B.y = canonical_embedding(f,y) by A3; hence B.x is Function; end; then reconsider B as Function-yielding ManySortedSet of I by FUNCOP_1:def 6; take B; let i be Element of I; A4: B.i = canonical_embedding(f,i) by A3; thus 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 proof thus B.i is Function of A.i,A.(s.i) by A4; let m be Function of A.i,A.(s.i); assume A5: m=B.i; consider L being Segre-like non trivial-yielding 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 thesis by A1,A5,A6,Def4; end; let p be Point of Segre_Product A; let a be ManySortedSet of I such that A7: a=p; consider b1 being Segre-like non trivial-yielding 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 such that A10: b=f.p; let m be Function of A.i,A.(s.i); assume m=B.i; then m=canonical_embedding(f,b1) by A1,A4,A8,Def5; hence thesis by A1,A7,A10,A8,A9,Def4; end;