:: 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, WAYBEL18, PENCIL_1, FUNCT_7,
      PENCIL_2, TOPS_2, FINSEQ_6, GRAPH_2;
 constructors PZFMISC1, TOPS_2, REALSET2, T_0TOPSP, GRAPH_2, PENCIL_2,
      RELSET_1, PBOOLE, FUNCT_7, PRE_POLY, FINSEQ_6;
 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,
      WAYBEL18;
 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, FINSEQ_6;
 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 & i<len
D 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 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 connected;
  let i be Element of I;
  let p be Point of A.i;
  let b1,b2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A
  such that
A2: product b2 is Segre-Coset of A and
A3: b1=b2+*(i,{p}) and
A4: not p in b2.i;
  defpred P[set,set] means for a,b being Point of A.i st $1=a & $2=b holds a,b
  are_collinear;
A5: now
    assume i=indx(b2);
    then b2.i = [#](A.i) by A2,Th10;
    hence contradiction by A4;
  end;
  then b2.i is 1-element by PENCIL_1:12;
  then consider q being object 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;
  then {q} c= [#](A.i) by A6,Th7;
  then reconsider 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 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, x,y being set st 1 <= j & j < len f & x=f.j
  & y=f.(j+1) holds P[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 P[F.j,F.(j+1)] from PENCIL_2:sch 1(A7,A9);
A11: now
    assume F={};
    then dom F = {};
    then F.1 = {} & F.(len F) = {} by FUNCT_1:def 2;
    hence contradiction by A4,A6,A10,TARSKI:def 1;
  end;
  deffunc H(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=H(j) from
  FINSEQ_1:sch 2;
  rng G c= bool the carrier of Segre_Product A
  proof
    let a be object;
    assume a in rng G;
    then consider o being object such that
A13: o in dom G and
A14: G.o=a by FUNCT_1:def 3;
    reconsider 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 thesis by A14,A15;
  end;
  then reconsider
  D=G as FinSequence of bool the carrier of Segre_Product A by FINSEQ_1:def 4;
  take D;
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;
  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;
  thus for j being Nat st j in dom D holds D.j is Segre-Coset of A
  proof
    let j be Nat;
    assume
A17: j in dom D;
    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 Segre-like non trivial-yielding
    ManySortedSubset of Carrier A by A5,Th13;
    BB.indx(b2) = b2.indx(b2) by A5,FUNCT_7:32;
    then BB.indx(b2) is non 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 thesis by A20,A19,PENCIL_2:def 2;
  end;
A21: dom b2=I by PARTFUN1:def 2;
  thus for i being Nat st 1<=i & i<len D 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;
    assume
A22: 1<=j & j<len D;
    let Di,Di1 be Segre-Coset of A such that
A23: Di=D.j and
A24: Di1=D.(j+1);
    reconsider 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 Segre-like non trivial-yielding
    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 Segre-like non trivial-yielding
    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
    proof
A32:  j<>j+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 & i<len D 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 finite non empty set;
  let A be PLS-yielding ManySortedSet of I;
  assume
A1: for i being Element of I holds A.i is connected;
  let B1,B2 be Segre-Coset of A such that
A2: B1 misses B2;
  let b1,b2 be Segre-like non trivial-yielding ManySortedSubset of Carrier A
  such that
A3: B1 = product b1 and
A4: B2 = product b2;
  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 for Di,Di1 being
  Segre-Coset of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1
  proof
    defpred P[Nat] means for c1,c2 being Segre-like non trivial-yielding
    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 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 for Di,Di1
being Segre-Coset of A st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||'
    Di1;
A5: now
      let k be Nat;
      assume
A6:   P[k];
      thus P[k+1]
      proof
        let c1,c2 being Segre-like non trivial-yielding ManySortedSubset of
        Carrier A such 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;
        {i where i is Element of I: c1.i<>c2.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<len E 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 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
            dom c2 = I by PARTFUN1:def 2;
            then
A30:        c3.j = {p} by FUNCT_7:31;
            assume len F=1;
            hence contradiction by A12,A15,A25,A26,A30,PUA2MSS1:2;
          end;
          reconsider D = E ^' F as FinSequence of bool the carrier of
          Segre_Product A;
          take D;
          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,FINSEQ_6:140;
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,FINSEQ_6:142;
          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 FINSEQ_6:143;
            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 D 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;
            assume that
A39:        1<=i and
A40:        i<len D;
            let Di,Di1 be Segre-Coset of A such that
A41:        Di=D.i and
A42:        Di1=D.(i+1);
            reconsider i as Element of NAT by ORDINAL1:def 12;
            per cases;
            suppose
A43:          i<len E;
              then i+1 <= len E by NAT_1:13;
              then
A44:          Di1=E.(i+1) by A42,FINSEQ_6:140,NAT_1:11;
              Di=E.i by A39,A41,A43,FINSEQ_6:140;
              hence thesis by A24,A39,A43,A44;
            end;
            suppose
              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,FINSEQ_6:139;
                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,FINSEQ_6:141,NAT_1:11;
                0+1<=k by A47,NAT_1:13;
                then
A52:            Di=F.(k+1) by A41,A45,A50,FINSEQ_6:141;
                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,
FINSEQ_6:140,141;
                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 & i<len D 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;
    thus D.1=B1 & D.(len D)=B2 by A3,A4,A59;
    thus thesis by A60;
  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 for Di,Di1 being Segre-Coset of A
  st Di=D.i & Di1=D.(i+1) holds Di misses Di1 & Di '||' Di1;
  defpred P[Nat] means for bb being Segre-like non trivial-yielding
  ManySortedSubset of Carrier A st product bb = D.$1 holds indx(b1) = indx(bb);
A65: now
    let k be Nat;
    assume
A66: P[k];
    thus P[k+1]
    proof
      let bb be Segre-like non trivial-yielding ManySortedSubset of Carrier A
      such that
A67:  product bb = D.(k+1);
A68:  k+1 in dom D by A67,FUNCT_1:def 2;
      then
A69:  k+1 <= len D by FINSEQ_3:25;
      per cases;
      suppose
        k=0;
        hence thesis by A3,A61,A67,PUA2MSS1:2;
      end;
      suppose
        0<k;
        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 Segre-like non trivial-yielding 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 thesis by A67,A71,A72,Th21;
      end;
    end;
  end;
A73: P[ 0 ]
  proof
A74: not 0 in dom D by FINSEQ_3:24;
    let bb be Segre-like non trivial-yielding ManySortedSubset of Carrier A;
    assume product bb = D.0;
    hence thesis by A74,FUNCT_1:def 2;
  end;
  for n being Nat holds P[n] from NAT_1:sch 2(A73,A65);
  hence thesis by A4,A62;
end;

theorem Th24:
  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
  for b1,b2,b3,b4 being Segre-like non trivial-yielding ManySortedSubset of
  Carrier A st B1 = product b1 & B2 = product b2 & f.:B1 = product b3 & f.:B2 =
  product b4 holds indx(b1)=indx(b2) implies indx(b3)=indx(b4)
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 i be Element of I;
    A.i is strongly_connected by A1;
    hence A.i is connected by Th4;
  end;
  let f be Collineation of Segre_Product A;
  let B1,B2 be Segre-Coset of A;
  let b1,b2,b3,b4 be Segre-like non trivial-yielding ManySortedSubset of
  Carrier A such that
A3: B1 = product b1 and
A4: B2 = product b2 and
A5: f.:B1 = product b3 & f.:B2 = product b4;
  assume
A6: indx(b1)=indx(b2);
  per cases;
  suppose
A7: B1 misses B2;
    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 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 F(Nat)=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 = F(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 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;
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;
      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;
      assume that
A18:  Ei=E.i and
A19:  Ei1=E.(i+1);
      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;
      Di '||' Di1 by A12,A13,A17;
      hence thesis by A20,A21,Th20;
    end;
A22: for i being Nat st i in dom E holds E.i is Segre-Coset of A
    proof
      let i be Nat;
      assume
A23:  i in dom E;
      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 thesis by A1,PENCIL_2:24;
    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 thesis by A2,A5,A24,A22,A15,A8,Th23;
  end;
  suppose
    B1 meets B2;
    then B1=B2 by A3,A4,A6,Th11;
    hence thesis by A5,PUA2MSS1:2;
  end;
end;

theorem Th25:
  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 st 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
proof
  let I be finite non empty set;
  let A be PLS-yielding ManySortedSet of I;
  assume
A1: for i be Element of I holds A.i is strongly_connected;
  let f be Collineation of Segre_Product A;
  defpred P[set,set] means 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)=$1 implies indx(b2)=$2;
A2: for x,y,x9 being Element of I st P[x,y] & P[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;
    assume that
A3: 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
A4: 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)=x9 implies indx(b2)=y;
    consider b1 being Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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 Segre-like non trivial-yielding 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 qua Function)" 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;
    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;
    indx(L1)=y by A3,A5,A7;
    hence thesis by A1,A5,A7,A8,A10,A11,A19,A17,Th24;
  end;
A20: for y being Element of I ex x 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
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 object;
      assume a in product b;
      then consider f being Function such that
A23:  a=f and
A24:  dom f=dom b and
A25:  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
A26:  dom f = dom Carrier A by A24,PARTFUN1:def 2;
A27:  now
        let i be object;
        assume
A28:    i in dom Carrier A;
        then reconsider i1=i as Element of I;
A29:    f.i in b.i by A24,A25,A26,A28;
        per cases;
        suppose
          i1=x;
          hence f.i in (Carrier A).i by A21,A29,Th7;
        end;
        suppose
          i1<>x;
          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<len D 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 P[Nat] means $1 in dom D implies for D1 being Segre-Coset of A st
    D1=D.$1 for d1 being Segre-like non trivial-yielding ManySortedSubset of
Carrier A st D1=product d1 holds canonical_embedding(f,b1)=canonical_embedding(
    f,d1);
A9: now
      let k be Nat;
      assume
A10:  P[k];
      thus P[k+1]
      proof
        assume k+1 in dom D;
        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 such that
A12:    D2=D.(k+1);
        let d2 be Segre-like non trivial-yielding ManySortedSubset of Carrier
        A such that
A13:    D2=product d2;
        per cases by NAT_1:14;
        suppose
          k=0;
          hence thesis by A5,A12,A13,PUA2MSS1:2;
        end;
        suppose
A14:      1<=k;
          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 Segre-like non trivial-yielding 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 thesis by A10,A11,A14,A15,FINSEQ_3:25;
        end;
      end;
    end;
A16: P[ 0 ] by FINSEQ_3:24;
    for n being Nat holds P[n] from NAT_1:sch 2(A16,A9);
    then
A17: P[len D];
    1 in dom D by A5,FUNCT_1:def 2;
    then 1 <= len D by FINSEQ_3:25;
    hence thesis by A6,A17,FINSEQ_3:25;
  end;
  suppose
    B1 meets B2;
    hence thesis by A4,Th11;
  end;
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;
  let i be Element of I;
  func canonical_embedding(f,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;