pencil_3.miz



    begin

    theorem :: PENCIL_3:1

    

     Th1: for S be non empty non void TopStruct holds for f be Collineation of S holds for p,q be 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 be 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 :: PENCIL_3:2

    

     Th2: for I be non empty set holds for i be Element of I holds for A be 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 :: PENCIL_3:3

    

     Th3: for S be 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 be 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 be Point of S;

        X1 is closed_under_lines strong by PENCIL_1: 20, PENCIL_1: 21;

        then

        consider f be FinSequence of ( bool the carrier of S) such that

         A3: X = (f . 1) and

         A4: x in (f . ( len f)) and

         A5: for W be Subset of S st W in ( rng f) holds W is closed_under_lines strong and

         A6: for i be 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 be 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 be 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 be 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 be Block of S st x in l;

        end;

      end;

      hence thesis by PENCIL_1:def 9;

    end;

    theorem :: PENCIL_3:4

    

     Th4: for S be non empty non void identifying_close_blocks TopStruct holds S is strongly_connected implies S is connected

    proof

      let S be 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 :: PENCIL_3:5

    for S be non void non degenerated TopStruct holds for L be Block of S holds ex x be 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 be 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 :: PENCIL_3:6

    

     Th6: for I be non empty set holds for A be non-Empty TopStruct-yielding ManySortedSet of I holds for p be 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 be Function such that

       A1: f = p and

       A2: ( dom f) = ( dom ( Carrier A)) and

       A3: for x be 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 be 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 :: PENCIL_3:7

    

     Th7: for I be non empty set holds for A be 1-sorted-yielding ManySortedSet of I holds for x be 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 be 1-sorted st R = (A . x) & (( Carrier A) . x) = the carrier of R by PRALG_1:def 15;

      hence thesis;

    end;

    theorem :: PENCIL_3:8

    

     Th8: for I be non empty set holds for i be Element of I holds for A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I holds ex L be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st ( indx L) = i & ( product L) is Segre-Coset of A

    proof

      let I be non empty set;

      let x be 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, PENCIL_1: 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 be Function such that

         A3: a = f and

         A4: ( dom f) = ( dom b) and

         A5: for x be 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 :: PENCIL_3:9

    

     Th9: for I be non empty set holds for i be Element of I holds for A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I holds for p be Point of ( Segre_Product A) holds ex L be 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 be non empty set;

      let x be 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, PENCIL_1: 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 be Function such that

         A3: a = f and

         A4: ( dom f) = ( dom b) and

         A5: for x be 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 :: PENCIL_3:10

    

     Th10: for I be non empty set holds for A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I holds for b be 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 be 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 :: PENCIL_3:11

    

     Th11: for I be non empty set holds for A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I holds for L1,L2 be 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 be 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 be 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 be 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 be 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 be 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 be 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 :: PENCIL_3:12

    

     Th12: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for L be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) holds for B be Block of (A . ( indx L)) holds ( product (L +* (( indx L),B))) is Block of ( Segre_Product A)

    proof

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let L be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A);

      let B be 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, PENCIL_1: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 :: PENCIL_3:13

    

     Th13: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for i be Element of I holds for p be Point of (A . i) holds for L be 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, PENCIL_1:def 20;

    end;

    theorem :: PENCIL_3:14

    

     Th14: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for i be Element of I holds for S be Subset of (A . i) holds for L be 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 :: PENCIL_3:15

    

     Th15: for I be non empty set holds for P be ManySortedSet of I holds for i be Element of I holds ( {P} . i) is 1 -element

    proof

      let I be 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 :: PENCIL_3:16

    

     Th16: for I be non empty set holds for i be Element of I holds for A be PLS-yielding ManySortedSet of I holds for B be Block of (A . i) holds for P be Element of ( Carrier A) holds ( product ( {P} +* (i,B))) is Block of ( Segre_Product A)

    proof

      let I be non empty set;

      let i be Element of I;

      let A be PLS-yielding ManySortedSet of I;

      let B be Block of (A . i);

      let P be 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, PENCIL_1: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 :: PENCIL_3:17

    

     Th17: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for p,q be Point of ( Segre_Product A) st p <> q holds (p,q) are_collinear iff for p1,q1 be ManySortedSet of I st p1 = p & q1 = q holds ex i be Element of I st (for a,b be Point of (A . i) st a = (p1 . i) & b = (q1 . i) holds a <> b & (a,b) are_collinear ) & for j be Element of I st j <> i holds (p1 . j) = (q1 . j)

    proof

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let p,q be Point of ( Segre_Product A);

      assume

       A1: p <> q;

      thus (p,q) are_collinear implies for p1,q1 be ManySortedSet of I st p1 = p & q1 = q holds ex i be Element of I st (for a,b be Point of (A . i) st a = (p1 . i) & b = (q1 . i) holds a <> b & (a,b) are_collinear ) & for j be Element of I st j <> i holds (p1 . j) = (q1 . j)

      proof

        assume (p,q) are_collinear ;

        then

        consider l be 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 be 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 be 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 be Point of (A . i);

          

           A9: ex p0 be Function st p0 = p1 & ( dom p0) = ( dom L) & for o be object st o in ( dom L) holds (p0 . o) in (L . o) by A6, A8, CARD_3:def 5;

          

           A10: ex q0 be Function st q0 = q1 & ( dom q0) = ( dom L) & for o be 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 be 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 be 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 be ManySortedSet of I st p1 = p & q1 = q holds ex i be Element of I st (for a,b be Point of (A . i) st a = (p1 . i) & b = (q1 . i) holds a <> b & (a,b) are_collinear ) & for j be Element of I st j <> i holds (p1 . j) = (q1 . j);

      then

      consider i be Element of I such that

       A19: for a,b be Point of (A . i) st a = (p1 . i) & b = (q1 . i) holds a <> b & (a,b) are_collinear and

       A20: for j be 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 be Block of (A . i) st {a, b} c= l;

        then

        consider l be 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 be 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 be 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 :: PENCIL_3:18

    

     Th18: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for b be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) holds for x be Point of (A . ( indx b)) holds ex p be 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 be object such that

       A1: bb in ( product b1) by XBOOLE_0:def 1;

      

       A2: ex bf be Function st bf = bb & ( dom bf) = ( dom b1) & for o be 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 be Function such that

         A10: u = o and

         A11: ( dom u) = ( dom (b1 +* (i, {x}))) and

         A12: for z be 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 be 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;

      :: PENCIL_3:def1

      func diff (b1,b2) -> Nat equals ( card { i where i be Element of I : (b1 . i) <> (b2 . i) });

      correctness

      proof

        { i where i be Element of I : (b1 . i) <> (b2 . i) } c= I

        proof

          let a be object;

          assume a in { i where i be Element of I : (b1 . i) <> (b2 . i) };

          then ex i be Element of I st a = i & (b1 . i) <> (b2 . i);

          hence thesis;

        end;

        then

        reconsider F = { i where i be Element of I : (b1 . i) <> (b2 . i) } as finite set by FINSET_1: 1;

        ( card F) = ( card F);

        hence thesis;

      end;

    end

    theorem :: PENCIL_3:19

    

     Th19: for I be finite non empty set holds for b1,b2 be ManySortedSet of I holds for i be 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 be Element of I : (b1 . i) <> (b2 . i) } c= I

      proof

        let a be object;

        assume a in { i where i be Element of I : (b1 . i) <> (b2 . i) };

        then ex i be Element of I st a = i & (b1 . i) <> (b2 . i);

        hence thesis;

      end;

      then

      reconsider F = { i where i be Element of I : (b1 . i) <> (b2 . i) } as finite set by FINSET_1: 1;

      { i where i be Element of I : (b1 . i) <> (b3 . i) } c= I

      proof

        let a be object;

        assume a in { i where i be Element of I : (b1 . i) <> (b3 . i) };

        then ex i be Element of I st a = i & (b1 . i) <> (b3 . i);

        hence thesis;

      end;

      then

      reconsider G = { i where i be 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 be 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 be 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 be 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

    definition

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let B1,B2 be Segre-Coset of A;

      :: PENCIL_3:def2

      pred B1 '||' B2 means for x be Point of ( Segre_Product A) st x in B1 holds ex y be Point of ( Segre_Product A) st y in B2 & (x,y) are_collinear ;

    end

    theorem :: PENCIL_3:20

    

     Th20: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for B1,B2 be Segre-Coset of A st B1 '||' B2 holds for f be Collineation of ( Segre_Product A) holds for C1,C2 be 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 be 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 be 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 be 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 :: PENCIL_3:21

    

     Th21: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for B1,B2 be Segre-Coset of A st B1 misses B2 holds B1 '||' B2 iff for b1,b2 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st B1 = ( product b1) & B2 = ( product b2) holds ( indx b1) = ( indx b2) & ex r be Element of I st r <> ( indx b1) & (for i be Element of I st i <> r holds (b1 . i) = (b2 . i)) & for c1,c2 be Point of (A . r) st (b1 . r) = {c1} & (b2 . r) = {c2} holds (c1,c2) are_collinear

    proof

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let B1,B2 be Segre-Coset of A;

      consider L1 be 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 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st B1 = ( product b1) & B2 = ( product b2) holds ( indx b1) = ( indx b2) & ex r be Element of I st r <> ( indx b1) & (for i be Element of I st i <> r holds (b1 . i) = (b2 . i)) & for c1,c2 be Point of (A . r) st (b1 . r) = {c1} & (b2 . r) = {c2} holds (c1,c2) are_collinear

      proof

        assume

         A3: B1 '||' B2;

        consider L2 be 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 be 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 be 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 be object such that

           A12: (b2 . ( indx b1)) = {c2} by ZFMISC_1: 131;

          set bl = the Block of (A . ( indx b1));

          consider p0 be 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 be 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 be Function st f = p & ( dom f) = ( dom b1) & for a be 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 be 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 be Element of I such that for a,b be Point of (A . i0) st a = (x1 . i0) & b = (y1 . i0) holds a <> b & (a,b) are_collinear and

             A24: for j be 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 be Function st g = y1 & ( dom g) = ( dom b2) & for a be 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 be Function st f = p & ( dom f) = ( dom b1) & for a be 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 be Element of I st r <> ( indx b1) & (for i be Element of I st i <> r holds (b1 . i) = (b2 . i)) & for c1,c2 be Point of (A . r) st (b1 . r) = {c1} & (b2 . r) = {c2} holds (c1,c2) are_collinear

        proof

          consider x be 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 be 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 be Element of I such that

           A36: for a,b be Point of (A . r) st a = (x1 . r) & b = (y1 . r) holds a <> b & (a,b) are_collinear and

           A37: for j be 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 be 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 be 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 be 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 be 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 be 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 be 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 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st B1 = ( product b1) & B2 = ( product b2) holds ( indx b1) = ( indx b2) & ex r be Element of I st r <> ( indx b1) & (for i be Element of I st i <> r holds (b1 . i) = (b2 . i)) & for c1,c2 be Point of (A . r) st (b1 . r) = {c1} & (b2 . r) = {c2} holds (c1,c2) are_collinear ;

      then

      consider r be Element of I such that

       A54: r <> ( indx L1) and

       A55: for i be Element of I st i <> r holds (L1 . i) = (L2 . i) and

       A56: for c1,c2 be 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 be 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 be 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 be Block of (A . r) such that

       A62: {c1, c2} c= bb by A59, PENCIL_1:def 1;

      let x be Point of ( Segre_Product A);

      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 be Function st x2 = x & ( dom x2) = ( dom L1) & for o be 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 :: PENCIL_3:22

    

     Th22: for I be finite non empty set holds for A be PLS-yielding ManySortedSet of I st for i be Element of I holds (A . i) is connected holds for i be Element of I holds for p be Point of (A . i) holds for b1,b2 be 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) holds ex D be FinSequence of ( bool the carrier of ( Segre_Product A)) st (D . 1) = ( product b1) & (D . ( len D)) = ( product b2) & (for i be Nat st i in ( dom D) holds (D . i) is Segre-Coset of A) & for i be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be 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 be 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 be 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 be FinSequence of the carrier of (A . i) such that

       A7: p = (f . 1) & q = (f . ( len f)) and

       A8: for j be Nat st 1 <= j & j < ( len f) holds for a,b be 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 be Element of NAT , x,y be set st 1 <= j & j < ( len f) & x = (f . j) & y = (f . (j + 1)) holds P[x, y] by A8;

      consider F be 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 be 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 be FinSequence such that

       A12: ( len G) = ( len F) & for j be 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 be 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 be 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 be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be 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 be Function such that

           A34: x2 = x and ( dom x2) = ( dom (b2 +* (i, {(F . (j + 1))}))) and

           A35: for o be 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 be Function such that

           A37: x1 = x and ( dom x1) = ( dom (b2 +* (i, {(F . j)}))) and

           A38: for o be 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 be 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 be 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 :: PENCIL_3:23

    

     Th23: for I be finite non empty set holds for A be PLS-yielding ManySortedSet of I st for i be Element of I holds (A . i) is connected holds for B1,B2 be Segre-Coset of A st B1 misses B2 holds for b1,b2 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st B1 = ( product b1) & B2 = ( product b2) holds ( indx b1) = ( indx b2) iff ex D be FinSequence of ( bool the carrier of ( Segre_Product A)) st (D . 1) = B1 & (D . ( len D)) = B2 & (for i be Nat st i in ( dom D) holds (D . i) is Segre-Coset of A) & for i be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be 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 be FinSequence of ( bool the carrier of ( Segre_Product A)) st (D . 1) = B1 & (D . ( len D)) = B2 & (for i be Nat st i in ( dom D) holds (D . i) is Segre-Coset of A) & for i be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be 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 holds ex D be FinSequence of ( bool the carrier of ( Segre_Product A)) st (D . 1) = ( product c1) & (D . ( len D)) = ( product c2) & (for i be Nat st i in ( dom D) holds (D . i) is Segre-Coset of A) & for i be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be 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 be Element of I : (c1 . i) <> (c2 . i) } <> {} by A10;

            then

            consider j0 be object such that

             A11: j0 in { i where i be Element of I : (c1 . i) <> (c2 . i) } by XBOOLE_0:def 1;

            consider j be 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 be 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 be 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 be 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 be Nat st i in ( dom E) holds (E . i) is Segre-Coset of A and

               A24: for i be Nat st 1 <= i & i < ( len E) holds for Ei,Ei1 be 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 be 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 be Nat st i in ( dom F) holds (F . i) is Segre-Coset of A and

               A28: for i be Nat st 1 <= i & i < ( len F) holds for Di,Di1 be 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 be 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 be 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 be 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 be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be 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, FINSEQ_6: 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 be 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 be 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 be 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 be Nat st i in ( dom D) holds (D . i) is Segre-Coset of A) & for i be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be 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 be Nat st i in ( dom D) holds (D . i) is Segre-Coset of A and

       A64: for i be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be Segre-Coset of A st Di = (D . i) & Di1 = (D . (i + 1)) holds Di misses Di1 & Di '||' Di1;

      defpred P[ Nat] means for bb be 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 be 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 be Nat holds P[n] from NAT_1:sch 2( A73, A65);

      hence thesis by A4, A62;

    end;

    theorem :: PENCIL_3:24

    

     Th24: for I be finite non empty set holds for A be PLS-yielding ManySortedSet of I st for i be Element of I holds (A . i) is strongly_connected holds for f be Collineation of ( Segre_Product A) holds for B1,B2 be Segre-Coset of A holds for b1,b2,b3,b4 be 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 be 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 be 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 be Nat st i in ( dom D) holds (D . i) is Segre-Coset of A and

         A12: for i be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be FinSequence of ( bool the carrier of ( Segre_Product A)) such that

         A13: ( len E) = ( len D) & for j be 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 be Nat st 1 <= i & i < ( len E) holds for Ei,Ei1 be 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 be 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 :: PENCIL_3:25

    

     Th25: for I be finite non empty set holds for A be PLS-yielding ManySortedSet of I st for i be Element of I holds (A . i) is strongly_connected holds for f be Collineation of ( Segre_Product A) holds ex s be Permutation of I st for i,j be Element of I holds (s . i) = j iff for B1 be Segre-Coset of A holds for b1,b2 be 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 be Segre-Coset of A holds for b1,b2 be 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 be 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 be Segre-Coset of A holds for b1,b2 be 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 be Segre-Coset of A holds for b1,b2 be 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 be 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 be 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 be 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 be 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 be Element of I holds ex x be 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, PENCIL_1: 10, PENCIL_2: 7;

        ( dom p) = I by PARTFUN1:def 2;

        then

         A21: (b . x) = C by FUNCT_7: 31;

        then

         A22: ( indx b) = x by PENCIL_1:def 21;

        ( product b) c= the carrier of ( Segre_Product A)

        proof

          let a be object;

          assume a in ( product b);

          then

          consider f be Function such that

           A23: a = f and

           A24: ( dom f) = ( dom b) and

           A25: for x be 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 be 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 be Segre-Coset of A;

        let b1,b2 be 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 be Element of I holds ex y be 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, PENCIL_1: 10, PENCIL_2: 7;

        ( dom p) = I by PARTFUN1:def 2;

        then

         A34: (b . x) = C by FUNCT_7: 31;

        then

         A35: ( indx b) = x by PENCIL_1:def 21;

        ( product b) c= the carrier of ( Segre_Product A)

        proof

          let a be object;

          assume a in ( product b);

          then

          consider f be Function such that

           A36: a = f and

           A37: ( dom f) = ( dom b) and

           A38: for x be 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 be 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 be Segre-Coset of A;

        let b1,b2 be 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 be 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 be Segre-Coset of A holds for b1,b2 be 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 be Segre-Coset of A holds for b1,b2 be 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 be 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 be 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 be Permutation of I st for x,y be 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;

      let f be Collineation of ( Segre_Product A);

      :: PENCIL_3:def3

      func permutation_of_indices (f) -> Permutation of I means

      : Def3: for i,j be Element of I holds (it . i) = j iff for B1 be Segre-Coset of A holds for b1,b2 be 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 be Element of I holds (s . i) = j iff for B1 be Segre-Coset of A holds for b1,b2 be 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 be Element of I holds (t . i) = j iff for B1 be Segre-Coset of A holds for b1,b2 be 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 be 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 be 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

    definition

      let I be finite non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let f be Collineation of ( Segre_Product A);

      let b1 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A);

      :: PENCIL_3:def4

      func canonical_embedding (f,b1) -> Function of (A . ( indx b1)), (A . (( permutation_of_indices f) . ( indx b1))) means

      : Def4: it is isomorphic & for a be ManySortedSet of I st a is Point of ( Segre_Product A) & a in ( product b1) holds for b be 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 be 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 be 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 be object st x in B holds ex y be object st P[x, y]

        proof

          let x be object;

          consider bb be object such that

           A9: bb in B1 by XBOOLE_0:def 1;

          

           A10: ex bf be Function st bf = bb & ( dom bf) = ( dom b1) & for o be 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 be Function such that

             A19: u = o and

             A20: ( dom u) = ( dom (b1 +* (i, {x}))) and

             A21: for z be 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 be 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 be Function such that

         A37: ( dom M) = B & for x be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be Function such that

                 A102: a = g and

                 A103: ( dom g) = ( dom (b1 +* (i, {u}))) and

                 A104: for o be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be ManySortedSet of I st a is Point of ( Segre_Product A) & a in ( product b1) holds for b be ManySortedSet of I st b = (f . a) holds (b . (s . i)) = (f1 . (a . i)) and f2 is isomorphic and

         A165: for a be ManySortedSet of I st a is Point of ( Segre_Product A) & a in ( product b1) holds for b be ManySortedSet of I st b = (f . a) holds (b . (s . i)) = (f2 . (a . i));

         A166:

        now

          let x be object;

          consider p be 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 :: PENCIL_3:26

    

     Th26: for I be finite non empty set holds for A be PLS-yielding ManySortedSet of I st for i be Element of I holds (A . i) is strongly_connected holds for f be Collineation of ( Segre_Product A) holds for B1,B2 be Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds for b1,b2 be 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 be 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 be Element of I such that

       A9: r <> ( indx b1) and

       A10: for i be Element of I st i <> r holds (b1 . i) = (b2 . i) and

       A11: for c1,c2 be Point of (A . r) st (b1 . r) = {c1} & (b2 . r) = {c2} holds (c1,c2) are_collinear by A2, A3, A4, A5, Th21;

      consider b4 be 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 be 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 be 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 be 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 be 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 be 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 be Element of I such that for a,b be Point of (A . l) st a = (fq . l) & b = (ft . l) holds a <> b & (a,b) are_collinear and

             A43: for j be 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 :: PENCIL_3:27

    

     Th27: for I be finite non empty set holds for A be PLS-yielding ManySortedSet of I st for i be Element of I holds (A . i) is strongly_connected holds for f be Collineation of ( Segre_Product A) holds for b1,b2 be 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 be 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 be 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 be Nat st i in ( dom D) holds (D . i) is Segre-Coset of A and

         A8: for i be Nat st 1 <= i & i < ( len D) holds for Di,Di1 be 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 be Segre-Coset of A st D1 = (D . $1) holds for d1 be 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 be 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 be 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;

      let f be Collineation of ( Segre_Product A);

      let i be Element of I;

      :: PENCIL_3:def5

      func canonical_embedding (f,i) -> Function of (A . i), (A . (( permutation_of_indices f) . i)) means

      : Def5: for b be 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 be 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 be 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 be 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 be 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 :: PENCIL_3:28

    for I be finite non empty set holds for A be PLS-yielding ManySortedSet of I st for i be Element of I holds (A . i) is strongly_connected holds for f be Collineation of ( Segre_Product A) holds ex s be Permutation of I, B be Function-yielding ManySortedSet of I st for i be Element of I holds ((B . i) is Function of (A . i), (A . (s . i)) & for m be Function of (A . i), (A . (s . i)) st m = (B . i) holds m is isomorphic) & for p be Point of ( Segre_Product A) holds for a be ManySortedSet of I st a = p holds for b be ManySortedSet of I st b = (f . p) holds for m be 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 be 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 be Element of I st i = $1 holds $2 = ( canonical_embedding (f,i));

      

       A2: for i be object st i in I holds ex j be 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 be ManySortedSet of I such that

       A3: for i be 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 be 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 be 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 be 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;