pencil_2.miz



    begin

    definition

      let D be set;

      let p be FinSequence of D;

      let i,j be Nat;

      :: PENCIL_2:def1

      func Del (p,i,j) -> FinSequence of D equals ((p | (i -' 1)) ^ (p /^ j));

      coherence ;

    end

    theorem :: PENCIL_2:1

    

     Th1: for D be set, p be FinSequence of D, i,j be Element of NAT holds ( rng ( Del (p,i,j))) c= ( rng p)

    proof

      let D be set, p be FinSequence of D, i,j be Element of NAT ;

      

       A1: ( rng (p /^ j)) c= ( rng p)

      proof

        per cases ;

          suppose

           A2: D is empty;

          then

           A3: j > ( len p) implies thesis;

          j <= ( len p) implies thesis by A2;

          hence thesis by A3;

        end;

          suppose D is non empty;

          then

          reconsider E = D as non empty set;

          reconsider r = p as FinSequence of E;

          ( rng (r /^ j)) c= ( rng r) by FINSEQ_5: 33;

          hence thesis;

        end;

      end;

      ( rng (p | (i -' 1))) = ( rng (p | ( Seg (i -' 1)))) by FINSEQ_1:def 15;

      then

       A4: ( rng (p | (i -' 1))) c= ( rng p) by RELAT_1: 70;

      ( rng ((p | (i -' 1)) ^ (p /^ j))) = (( rng (p | (i -' 1))) \/ ( rng (p /^ j))) by FINSEQ_1: 31;

      hence thesis by A4, A1, XBOOLE_1: 8;

    end;

    theorem :: PENCIL_2:2

    

     Th2: for D be set, p be FinSequence of D, i,j be Element of NAT st i in ( dom p) & j in ( dom p) holds ( len ( Del (p,i,j))) = (((( len p) - j) + i) - 1)

    proof

      let D be set;

      let p be FinSequence of D;

      let i,j be Element of NAT ;

      assume that

       A1: i in ( dom p) and

       A2: j in ( dom p);

      

       A3: i <= ( len p) by A1, FINSEQ_3: 25;

      1 <= i by A1, FINSEQ_3: 25;

      then

       A4: (i - 1) >= (1 - 1) by XREAL_1: 9;

      

       A5: (i -' 1) <= i by NAT_D: 35;

      

       A6: j <= ( len p) by A2, FINSEQ_3: 25;

      

      thus ( len ( Del (p,i,j))) = (( len (p | (i -' 1))) + ( len (p /^ j))) by FINSEQ_1: 22

      .= ((i -' 1) + ( len (p /^ j))) by A3, A5, FINSEQ_1: 59, XXREAL_0: 2

      .= ((i -' 1) + (( len p) - j)) by A6, RFINSEQ:def 1

      .= ((i - 1) + (( len p) - j)) by A4, XREAL_0:def 2

      .= (((( len p) - j) + i) - 1);

    end;

    theorem :: PENCIL_2:3

    

     Th3: for D be set, p be FinSequence of D, i,j be Element of NAT st i in ( dom p) & j in ( dom p) holds ( len ( Del (p,i,j))) = 0 implies i = 1 & j = ( len p)

    proof

      let D be set;

      let p be FinSequence of D;

      let i,j be Element of NAT ;

      assume that

       A1: i in ( dom p) and

       A2: j in ( dom p) and

       A3: ( len ( Del (p,i,j))) = 0 ;

      

       A4: 1 <= i by A1, FINSEQ_3: 25;

      j <= ( len p) by A2, FINSEQ_3: 25;

      then

       A5: (( len p) - j) >= 0 by XREAL_1: 48;

      

       A6: (((( len p) - j) + i) - 1) = 0 by A1, A2, A3, Th2;

      then (( len p) - j) = (1 - i);

      then 1 >= i by A5, XREAL_1: 49;

      hence i = 1 by A4, XXREAL_0: 1;

      hence thesis by A6;

    end;

    theorem :: PENCIL_2:4

    

     Th4: for D be set, p be FinSequence of D, i,j,k be Element of NAT st i in ( dom p) & 1 <= k & k <= (i - 1) holds (( Del (p,i,j)) . k) = (p . k)

    proof

      let D be set;

      let p be FinSequence of D;

      let i,j,k be Element of NAT ;

      assume that

       A1: i in ( dom p) and

       A2: 1 <= k and

       A3: k <= (i - 1);

      

       A4: i <= ( len p) by A1, FINSEQ_3: 25;

      

       A5: k <= (i -' 1) by A3, XREAL_0:def 2;

      

       A6: (i -' 1) <= i by NAT_D: 35;

      then ( len (p | (i -' 1))) = (i -' 1) by A4, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A7: k in ( dom (p | (i -' 1))) by A2, A5, FINSEQ_3: 25;

      (i -' 1) <= ( len p) by A4, A6, XXREAL_0: 2;

      then k <= ( len p) by A5, XXREAL_0: 2;

      then

       A8: k in ( dom p) by A2, FINSEQ_3: 25;

      

      thus (( Del (p,i,j)) . k) = ((p | (i -' 1)) . k) by A7, FINSEQ_1:def 7

      .= ((p | (i -' 1)) /. k) by A7, PARTFUN1:def 6

      .= (p /. k) by A7, FINSEQ_4: 70

      .= (p . k) by A8, PARTFUN1:def 6;

    end;

    theorem :: PENCIL_2:5

    

     Th5: for p,q be FinSequence, k be Element of NAT holds (( len p) + 1) <= k implies ((p ^ q) . k) = (q . (k - ( len p)))

    proof

      let p,q be FinSequence;

      let k be Element of NAT ;

      assume

       A1: (( len p) + 1) <= k;

      per cases ;

        suppose k <= (( len p) + ( len q));

        hence thesis by A1, FINSEQ_1: 23;

      end;

        suppose

         A2: not k <= (( len p) + ( len q));

        then (k - ( len p)) > ( len q) by XREAL_1: 20;

        then

         A3: not (k - ( len p)) in ( dom q) by FINSEQ_3: 25;

         not k <= ( len (p ^ q)) by A2, FINSEQ_1: 22;

        then not k in ( dom (p ^ q)) by FINSEQ_3: 25;

        

        hence ((p ^ q) . k) = {} by FUNCT_1:def 2

        .= (q . (k - ( len p))) by A3, FUNCT_1:def 2;

      end;

    end;

    theorem :: PENCIL_2:6

    

     Th6: for D be set, p be FinSequence of D, i,j,k be Element of NAT st i in ( dom p) & j in ( dom p) & i <= j & i <= k & k <= (((( len p) - j) + i) - 1) holds (( Del (p,i,j)) . k) = (p . (((j -' i) + k) + 1))

    proof

      let D be set;

      let p be FinSequence of D;

      let i,j,k be Element of NAT ;

      assume that

       A1: i in ( dom p) and

       A2: j in ( dom p) and

       A3: i <= j and

       A4: i <= k and

       A5: k <= (((( len p) - j) + i) - 1);

      

       A6: (i -' 1) <= i by NAT_D: 35;

      (i -' 1) <= i by NAT_D: 35;

      then k >= (i -' 1) by A4, XXREAL_0: 2;

      then (k - (i -' 1)) >= ((i -' 1) - (i -' 1)) by XREAL_1: 9;

      then

       A7: (k - (i -' 1)) = (k -' (i -' 1)) by XREAL_0:def 2;

      

       A8: 1 <= i by A1, FINSEQ_3: 25;

      then

       A9: ((i -' 1) + 1) <= k by A4, XREAL_1: 235;

      (i - 1) >= (1 - 1) by A8, XREAL_1: 9;

      then

       A10: (i -' 1) = (i - 1) by XREAL_0:def 2;

      (j - i) >= (i - i) by A3, XREAL_1: 9;

      then

       A11: (j -' i) = (j - i) by XREAL_0:def 2;

      

       A12: j <= ( len p) by A2, FINSEQ_3: 25;

      then

       A13: ( len (p /^ j)) = (( len p) - j) by RFINSEQ:def 1;

      k <= ((( len p) - j) + (i - 1)) by A5;

      then

       A14: (k - (i -' 1)) <= (( len p) - j) by A10, XREAL_1: 20;

      1 <= (k - (i -' 1)) by A9, XREAL_1: 19;

      then

       A15: (k - (i -' 1)) in ( dom (p /^ j)) by A7, A13, A14, FINSEQ_3: 25;

      i <= ( len p) by A1, FINSEQ_3: 25;

      then ( len (p | (i -' 1))) = (i -' 1) by A6, FINSEQ_1: 59, XXREAL_0: 2;

      

      hence (( Del (p,i,j)) . k) = ((p /^ j) . (k - (i -' 1))) by A9, Th5

      .= (p . (j + (k + (1 - i)))) by A12, A10, A15, RFINSEQ:def 1

      .= (p . (((j -' i) + k) + 1)) by A11;

    end;

    scheme :: PENCIL_2:sch1

    FinSeqOneToOne { X,Y,D() -> set , f() -> FinSequence of D() , P[ set, set] } :

ex g be one-to-one FinSequence of D() st X() = (g . 1) & Y() = (g . ( len g)) & ( rng g) c= ( rng f()) & for j be Element of NAT st 1 <= j & j < ( len g) holds P[(g . j), (g . (j + 1))]

      provided

       A1: X() = (f() . 1) & Y() = (f() . ( len f()))

       and

       A2: for i be Element of NAT , d1,d2 be set st 1 <= i & i < ( len f()) & d1 = (f() . i) & d2 = (f() . (i + 1)) holds P[d1, d2];

      defpred Q[ Nat] means ex f be FinSequence of D() st ( len f) = $1 & X() = (f . 1) & Y() = (f . ( len f)) & ( rng f) c= ( rng f()) & for i be Element of NAT st 1 <= i & i < ( len f) holds P[(f . i), (f . (i + 1))];

      for i be Element of NAT st 1 <= i & i < ( len f()) holds P[(f() . i), (f() . (i + 1))] by A2;

      then

       A3: ex k be Nat st Q[k] by A1;

      consider k be Nat such that

       A4: Q[k] & for n be Nat st Q[n] holds k <= n from NAT_1:sch 5( A3);

      consider g be FinSequence of D() such that

       A5: ( len g) = k and

       A6: X() = (g . 1) and

       A7: Y() = (g . ( len g)) and

       A8: ( rng g) c= ( rng f()) and

       A9: for i be Element of NAT st 1 <= i & i < ( len g) holds P[(g . i), (g . (i + 1))] by A4;

      now

        assume not g is one-to-one;

        then

        consider x,y be object such that

         A10: x in ( dom g) and

         A11: y in ( dom g) and

         A12: (g . x) = (g . y) and

         A13: x <> y by FUNCT_1:def 4;

        reconsider x, y as Element of NAT by A10, A11;

        per cases by A13, XXREAL_0: 1;

          suppose

           A14: x < y;

          set d = ( Del (g,(x + 1),y));

          

           A15: 1 <= y by A11, FINSEQ_3: 25;

          

           A16: (x + 1) >= 1 by NAT_1: 11;

          

           A17: y <= ( len g) by A11, FINSEQ_3: 25;

          then

           A18: x < ( len g) by A14, XXREAL_0: 2;

          then (x + 1) <= ( len g) by NAT_1: 13;

          then

           A19: (x + 1) in ( dom g) by A16, FINSEQ_3: 25;

          

           A20: (x + 1) <= y by A14, NAT_1: 13;

          then

           A21: (y - (x + 1)) >= 0 by XREAL_1: 48;

          

           A22: ( rng d) c= ( rng f()) & for i be Element of NAT st 1 <= i & i < ( len d) holds P[(d . i), (d . (i + 1))]

          proof

            ( rng d) c= ( rng g) by Th1;

            hence ( rng d) c= ( rng f()) by A8;

            let i be Element of NAT ;

            assume that

             A23: 1 <= i and

             A24: i < ( len d);

            per cases by XXREAL_0: 1;

              suppose

               A25: i < x;

              then (i + 1) <= ((x + 1) - 1) by NAT_1: 13;

              then

               A26: (d . (i + 1)) = (g . (i + 1)) by A19, Th4, NAT_1: 11;

              i <= ((x + 1) - 1) by A25;

              then

               A27: (d . i) = (g . i) by A19, A23, Th4;

              i < ( len g) by A18, A25, XXREAL_0: 2;

              hence thesis by A9, A23, A27, A26;

            end;

              suppose

               A28: i = x;

              now

                assume y = ( len g);

                then x < (((( len g) - ( len g)) + (x + 1)) - 1) by A11, A19, A24, A28, Th2;

                hence contradiction;

              end;

              then

               A29: y < ( len g) by A17, XXREAL_0: 1;

              then

               A30: 0 < (( len g) - y) by XREAL_1: 50;

              then 0 < (( len g) -' y) by XREAL_0:def 2;

              then ( 0 + 1) <= (( len g) -' y) by NAT_1: 13;

              then (1 - 1) <= ((( len g) -' y) - 1) by XREAL_1: 9;

              then 0 <= ((( len g) - y) - 1) by A30, XREAL_0:def 2;

              then ((i + 1) + 0 ) <= ((i + 1) + ((( len g) - y) - 1)) by XREAL_1: 7;

              then ((i + 1) + 0 ) <= (((i + 1) + (( len g) - y)) - 1);

              

              then

               A31: (d . (i + 1)) = (g . (((y -' (x + 1)) + (i + 1)) + 1)) by A11, A20, A19, A28, Th6

              .= (g . (y + 1)) by A20, A28, XREAL_1: 235;

              i <= ((x + 1) - 1) by A28;

              then (d . i) = (g . y) by A12, A19, A23, A28, Th4;

              hence thesis by A9, A15, A29, A31;

            end;

              suppose i > x;

              then

               A32: (x + 1) <= i by NAT_1: 13;

              

               A33: (( len g) - y) >= 0 by A17, XREAL_1: 48;

              i < (((( len g) - y) + (x + 1)) - 1) by A11, A19, A24, Th2;

              then

               A34: i < (((( len g) -' y) + (x + 1)) - 1) by A33, XREAL_0:def 2;

              then (i + 1) <= ((( len g) -' y) + x) by NAT_1: 13;

              then (i + 1) <= ((((( len g) - y) + x) + 1) - 1) by A33, XREAL_0:def 2;

              then

               A35: (i + 1) <= (((( len g) - y) + (x + 1)) - 1);

              i < ((((( len g) -' y) + x) + 1) - 1) by A34;

              then i < ((( len g) - y) + x) by A33, XREAL_0:def 2;

              then (i - x) < (((( len g) - y) + x) - x) by XREAL_1: 9;

              then ((i - x) + y) < ((( len g) - y) + y) by XREAL_1: 8;

              then ((((y - x) - 1) + i) + 1) < ( len g);

              then

               A36: (((y -' (x + 1)) + i) + 1) < ( len g) by A21, XREAL_0:def 2;

              i <= (i + 1) by NAT_1: 11;

              then (x + 1) <= (i + 1) by A32, XXREAL_0: 2;

              

              then

               A37: (d . (i + 1)) = (g . (((y -' (x + 1)) + (i + 1)) + 1)) by A11, A20, A19, A35, Th6

              .= (g . ((((y -' (x + 1)) + i) + 1) + 1));

              i <= (((( len g) - y) + (x + 1)) - 1) by A11, A19, A24, Th2;

              then (d . i) = (g . (((y -' (x + 1)) + i) + 1)) by A11, A20, A19, A32, Th6;

              hence thesis by A9, A37, A36, NAT_1: 11;

            end;

          end;

          

           A38: Y() = (d . ( len d))

          proof

            per cases ;

              suppose

               A39: ( len d) <= x;

              now

                assume ( len d) = 0 ;

                then (x + 1) = ( 0 + 1) by A11, A19, Th3;

                hence contradiction by A10, FINSEQ_3: 24;

              end;

              then

               A40: ( 0 + 1) <= ( len d) by NAT_1: 13;

              ( len d) <= ((x + 1) - 1) by A39;

              then

               A41: (d . ( len d)) = (g . ( len d)) by A19, A40, Th4;

              (((( len g) - y) + (x + 1)) - 1) <= x by A11, A19, A39, Th2;

              then ((((( len g) - y) + x) + 1) - 1) <= x;

              then (( len g) - y) <= 0 by XREAL_1: 29;

              then ( len g) <= y by XREAL_1: 50;

              then

               A42: ( len g) = y by A17, XXREAL_0: 1;

              then x <= (((( len g) - y) + (x + 1)) - 1);

              hence thesis by A7, A11, A12, A19, A42, A41, Th2;

            end;

              suppose ( len d) > x;

              then

               A43: (x + 1) <= ( len d) by NAT_1: 13;

              ( len d) = (((( len g) - y) + (x + 1)) - 1) by A11, A19, Th2;

              

              hence (d . ( len d)) = (g . (((y -' (x + 1)) + (((( len g) - y) + (x + 1)) - 1)) + 1)) by A11, A20, A19, A43, Th6

              .= (g . (((y - (x + 1)) + ((x + 1) + ((( len g) - y) - 1))) + 1)) by A20, XREAL_1: 233

              .= Y() by A7;

            end;

          end;

          1 <= ((x + 1) - 1) by A10, FINSEQ_3: 25;

          then

           A44: X() = (d . 1) by A6, A19, Th4;

           0 < ( - ( - (y - x))) by A14, XREAL_1: 50;

          then ( - (y - x)) < 0 ;

          then (( len g) + ( - (y - x))) < (( len g) + 0 ) by XREAL_1: 8;

          then (((( len g) - y) + (x + 1)) - 1) < ( len g);

          then ( len d) < ( len g) by A11, A19, Th2;

          hence contradiction by A4, A5, A44, A38, A22;

        end;

          suppose

           A45: y < x;

          set d = ( Del (g,(y + 1),x));

          

           A46: 1 <= x by A10, FINSEQ_3: 25;

          

           A47: (y + 1) >= 1 by NAT_1: 11;

          

           A48: x <= ( len g) by A10, FINSEQ_3: 25;

          then

           A49: y < ( len g) by A45, XXREAL_0: 2;

          then (y + 1) <= ( len g) by NAT_1: 13;

          then

           A50: (y + 1) in ( dom g) by A47, FINSEQ_3: 25;

          

           A51: (y + 1) <= x by A45, NAT_1: 13;

          then

           A52: (x - (y + 1)) >= 0 by XREAL_1: 48;

          

           A53: ( rng d) c= ( rng f()) & for i be Element of NAT st 1 <= i & i < ( len d) holds P[(d . i), (d . (i + 1))]

          proof

            ( rng d) c= ( rng g) by Th1;

            hence ( rng d) c= ( rng f()) by A8;

            let i be Element of NAT ;

            assume that

             A54: 1 <= i and

             A55: i < ( len d);

            per cases by XXREAL_0: 1;

              suppose

               A56: i < y;

              then (i + 1) <= ((y + 1) - 1) by NAT_1: 13;

              then

               A57: (d . (i + 1)) = (g . (i + 1)) by A50, Th4, NAT_1: 11;

              i <= ((y + 1) - 1) by A56;

              then

               A58: (d . i) = (g . i) by A50, A54, Th4;

              i < ( len g) by A49, A56, XXREAL_0: 2;

              hence thesis by A9, A54, A58, A57;

            end;

              suppose

               A59: i = y;

              now

                assume x = ( len g);

                then y < (((( len g) - ( len g)) + (y + 1)) - 1) by A10, A50, A55, A59, Th2;

                hence contradiction;

              end;

              then

               A60: x < ( len g) by A48, XXREAL_0: 1;

              then

               A61: 0 < (( len g) - x) by XREAL_1: 50;

              then 0 < (( len g) -' x) by XREAL_0:def 2;

              then ( 0 + 1) <= (( len g) -' x) by NAT_1: 13;

              then (1 - 1) <= ((( len g) -' x) - 1) by XREAL_1: 9;

              then 0 <= ((( len g) - x) - 1) by A61, XREAL_0:def 2;

              then ((i + 1) + 0 ) <= ((i + 1) + ((( len g) - x) - 1)) by XREAL_1: 7;

              then ((i + 1) + 0 ) <= (((i + 1) + (( len g) - x)) - 1);

              

              then

               A62: (d . (i + 1)) = (g . (((x -' (y + 1)) + (i + 1)) + 1)) by A10, A51, A50, A59, Th6

              .= (g . (x + 1)) by A51, A59, XREAL_1: 235;

              i <= ((y + 1) - 1) by A59;

              then (d . i) = (g . x) by A12, A50, A54, A59, Th4;

              hence thesis by A9, A46, A60, A62;

            end;

              suppose i > y;

              then

               A63: (y + 1) <= i by NAT_1: 13;

              

               A64: (( len g) - x) >= 0 by A48, XREAL_1: 48;

              i < (((( len g) - x) + (y + 1)) - 1) by A10, A50, A55, Th2;

              then

               A65: i < (((( len g) -' x) + (y + 1)) - 1) by A64, XREAL_0:def 2;

              then (i + 1) <= ((( len g) -' x) + y) by NAT_1: 13;

              then (i + 1) <= ((((( len g) - x) + y) + 1) - 1) by A64, XREAL_0:def 2;

              then

               A66: (i + 1) <= (((( len g) - x) + (y + 1)) - 1);

              i < ((((( len g) -' x) + y) + 1) - 1) by A65;

              then i < ((( len g) - x) + y) by A64, XREAL_0:def 2;

              then (i - y) < (((( len g) - x) + y) - y) by XREAL_1: 9;

              then ((i - y) + x) < ((( len g) - x) + x) by XREAL_1: 8;

              then ((((x - y) - 1) + i) + 1) < ( len g);

              then

               A67: (((x -' (y + 1)) + i) + 1) < ( len g) by A52, XREAL_0:def 2;

              i <= (i + 1) by NAT_1: 11;

              then (y + 1) <= (i + 1) by A63, XXREAL_0: 2;

              

              then

               A68: (d . (i + 1)) = (g . (((x -' (y + 1)) + (i + 1)) + 1)) by A10, A51, A50, A66, Th6

              .= (g . ((((x -' (y + 1)) + i) + 1) + 1));

              i <= (((( len g) - x) + (y + 1)) - 1) by A10, A50, A55, Th2;

              then (d . i) = (g . (((x -' (y + 1)) + i) + 1)) by A10, A51, A50, A63, Th6;

              hence thesis by A9, A68, A67, NAT_1: 11;

            end;

          end;

          

           A69: Y() = (d . ( len d))

          proof

            per cases ;

              suppose

               A70: ( len d) <= y;

              now

                assume ( len d) = 0 ;

                then (y + 1) = ( 0 + 1) by A10, A50, Th3;

                hence contradiction by A11, FINSEQ_3: 24;

              end;

              then

               A71: ( 0 + 1) <= ( len d) by NAT_1: 13;

              ( len d) <= ((y + 1) - 1) by A70;

              then

               A72: (d . ( len d)) = (g . ( len d)) by A50, A71, Th4;

              (((( len g) - x) + (y + 1)) - 1) <= y by A10, A50, A70, Th2;

              then ((((( len g) - x) + y) + 1) - 1) <= y;

              then (( len g) - x) <= 0 by XREAL_1: 29;

              then ( len g) <= x by XREAL_1: 50;

              then

               A73: ( len g) = x by A48, XXREAL_0: 1;

              then y <= (((( len g) - x) + (y + 1)) - 1);

              hence thesis by A7, A10, A12, A50, A73, A72, Th2;

            end;

              suppose ( len d) > y;

              then

               A74: (y + 1) <= ( len d) by NAT_1: 13;

              ( len d) = (((( len g) - x) + (y + 1)) - 1) by A10, A50, Th2;

              

              hence (d . ( len d)) = (g . (((x -' (y + 1)) + (((( len g) - x) + (y + 1)) - 1)) + 1)) by A10, A51, A50, A74, Th6

              .= (g . (((x - (y + 1)) + ((y + 1) + ((( len g) - x) - 1))) + 1)) by A51, XREAL_1: 233

              .= Y() by A7;

            end;

          end;

          1 <= ((y + 1) - 1) by A11, FINSEQ_3: 25;

          then

           A75: X() = (d . 1) by A6, A50, Th4;

           0 < ( - ( - (x - y))) by A45, XREAL_1: 50;

          then ( - (x - y)) < 0 ;

          then (( len g) + ( - (x - y))) < (( len g) + 0 ) by XREAL_1: 8;

          then (((( len g) - x) + (y + 1)) - 1) < ( len g);

          then ( len d) < ( len g) by A10, A50, Th2;

          hence contradiction by A4, A5, A75, A69, A53;

        end;

      end;

      hence thesis by A6, A7, A8, A9;

    end;

    begin

    theorem :: PENCIL_2:7

    

     Th7: for I be non empty set holds for A be 1-sorted-yielding ManySortedSet of I holds for L be ManySortedSubset of ( Carrier A) holds for i be Element of I holds for S be Subset of (A . i) holds (L +* (i,S)) is ManySortedSubset of ( Carrier A)

    proof

      let I be non empty set;

      let A be 1-sorted-yielding ManySortedSet of I;

      let L be ManySortedSubset of ( Carrier A);

      let i be Element of I;

      let S be Subset of (A . i);

      

       A1: L c= ( Carrier A) by PBOOLE:def 18;

      

       A2: ( dom L) = I by PARTFUN1:def 2;

      (L +* (i,S)) c= ( Carrier A)

      proof

        let a be object;

        assume a in I;

        then

        reconsider b = a as Element of I;

        per cases ;

          suppose

           A3: a = i;

          then ((L +* (i,S)) . b) = S by A2, FUNCT_7: 31;

          then ((L +* (i,S)) . b) c= the carrier of (A . b) by A3;

          hence thesis by YELLOW_6: 2;

        end;

          suppose a <> i;

          then ((L +* (i,S)) . a) = (L . b) by FUNCT_7: 32;

          hence thesis by A1;

        end;

      end;

      hence thesis by PBOOLE:def 18;

    end;

    definition

      let I be non empty set;

      let A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I;

      :: PENCIL_2:def2

      mode Segre-Coset of A -> Subset of ( Segre_Product A) means

      : Def2: ex L be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st it = ( product L) & (L . ( indx L)) = ( [#] (A . ( indx L)));

      existence

      proof

        set L = the Segre-like non trivial-yielding ManySortedSubset of ( Carrier A);

        reconsider C = (L +* (( indx L),( [#] (A . ( indx L))))) as ManySortedSubset of ( Carrier A) by Th7;

        

         A1: ( dom ( Carrier A)) = I by PARTFUN1:def 2;

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

        then (A . ( indx L)) in ( rng A) by FUNCT_1: 3;

        then

         A2: (A . ( indx L)) is non trivial by PENCIL_1:def 17;

        then

        reconsider C as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by PENCIL_1: 27;

        C c= ( Carrier A) by PBOOLE:def 18;

        then

         A3: for a be object st a in I holds (C . a) c= (( Carrier A) . a);

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

        then

        reconsider P = ( product C) as Subset of ( Segre_Product A) by A1, A3, CARD_3: 27;

        take P;

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

        then

         A4: (C . ( indx L)) = ( [#] (A . ( indx L))) by FUNCT_7: 31;

        then ( indx C) = ( indx L) by A2, PENCIL_1:def 21;

        hence thesis by A4;

      end;

    end

    theorem :: PENCIL_2:8

    

     Th8: for I be non empty set holds for A be non-Trivial-yielding TopStruct-yielding ManySortedSet of I holds for B1,B2 be Segre-Coset of A st 2 c= ( card (B1 /\ B2)) holds B1 = B2

    proof

      let I be non empty set;

      let A be non-Trivial-yielding TopStruct-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

       A2: (L1 . ( indx L1)) = ( [#] (A . ( indx L1))) by Def2;

      consider L2 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) such that

       A3: B2 = ( product L2) and

       A4: (L2 . ( indx L2)) = ( [#] (A . ( indx L2))) by Def2;

      assume

       A5: 2 c= ( card (B1 /\ B2));

      then

       A6: ( indx L1) = ( indx L2) by A1, A3, PENCIL_1: 26;

       A7:

      now

        let i be object;

        assume i in I;

        per cases ;

          suppose i <> ( indx L1);

          hence (L1 . i) = (L2 . i) by A5, A1, A3, PENCIL_1: 26;

        end;

          suppose i = ( indx L1);

          hence (L1 . i) = (L2 . i) by A2, A4, A6;

        end;

      end;

      

       A8: ( dom L2) = I by PARTFUN1:def 2;

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

      hence thesis by A1, A3, A8, A7, FUNCT_1: 2;

    end;

    definition

      let S be TopStruct;

      let X,Y be Subset of S;

      :: PENCIL_2:def3

      pred X,Y are_joinable means ex f be FinSequence of ( bool the carrier of S) st X = (f . 1) & Y = (f . ( len f)) & (for W be Subset of S st W in ( rng f) holds W is closed_under_lines strong) & for i be Element of NAT st 1 <= i & i < ( len f) holds 2 c= ( card ((f . i) /\ (f . (i + 1))));

    end

    theorem :: PENCIL_2:9

    for S be TopStruct holds for X,Y be Subset of S st (X,Y) are_joinable holds ex f be one-to-one FinSequence of ( bool the carrier of S) st (X = (f . 1) & Y = (f . ( len f)) & (for W be Subset of S st W in ( rng f) holds W is closed_under_lines strong) & for i be Element of NAT st 1 <= i & i < ( len f) holds 2 c= ( card ((f . i) /\ (f . (i + 1)))))

    proof

      defpred P[ set, set] means 2 c= ( card ($1 /\ $2));

      let S be TopStruct;

      let X,Y be Subset of S;

      assume (X,Y) are_joinable ;

      then

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

       A1: X = (f . 1) & Y = (f . ( len f)) and

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

       A3: for i be Element of NAT st 1 <= i & i < ( len f) holds 2 c= ( card ((f . i) /\ (f . (i + 1))));

      

       A4: for i be Element of NAT , d1,d2 be set st 1 <= i & i < ( len f) & d1 = (f . i) & d2 = (f . (i + 1)) holds P[d1, d2] by A3;

      consider g be one-to-one FinSequence of ( bool the carrier of S) such that

       A5: X = (g . 1) & Y = (g . ( len g)) and

       A6: ( rng g) c= ( rng f) and

       A7: for i be Element of NAT st 1 <= i & i < ( len g) holds P[(g . i), (g . (i + 1))] from FinSeqOneToOne( A1, A4);

      take g;

      thus thesis by A2, A5, A6, A7;

    end;

    theorem :: PENCIL_2:10

    

     Th10: for S be TopStruct holds for X be Subset of S st X is closed_under_lines strong holds (X,X) are_joinable

    proof

      let S be TopStruct;

      let X be Subset of S;

      assume

       A1: X is closed_under_lines strong;

      reconsider f = <*X*> as FinSequence of ( bool the carrier of S);

      take f;

      thus X = (f . 1) by FINSEQ_1: 40;

      ( len f) = 1 by FINSEQ_1: 40;

      hence X = (f . ( len f)) by FINSEQ_1: 40;

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

      proof

        let W be Subset of S;

        assume W in ( rng f);

        then W in {X} by FINSEQ_1: 38;

        hence thesis by A1, TARSKI:def 1;

      end;

      let i be Element of NAT ;

      assume that

       A2: 1 <= i and

       A3: i < ( len f);

      thus thesis by A2, A3, FINSEQ_1: 40;

    end;

    theorem :: PENCIL_2:11

    

     Th11: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for X,Y be Subset of ( Segre_Product A) st X is non trivial closed_under_lines strong & Y is non trivial closed_under_lines strong & (X,Y) are_joinable holds for X1,Y1 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st X = ( product X1) & Y = ( product Y1) holds ( indx X1) = ( indx Y1) & for i be object st i <> ( indx X1) holds (X1 . i) = (Y1 . i)

    proof

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let X,Y be Subset of ( Segre_Product A);

      assume that

       A1: X is non trivial closed_under_lines strong and

       A2: Y is non trivial closed_under_lines strong and

       A3: (X,Y) are_joinable ;

      set B = ( bool the carrier of ( Segre_Product A));

      consider f be FinSequence of B such that

       A4: X = (f . 1) and

       A5: Y = (f . ( len f)) and

       A6: for W be Subset of ( Segre_Product A) st W in ( rng f) holds W is closed_under_lines strong and

       A7: for i be Element of NAT st 1 <= i & i < ( len f) holds 2 c= ( card ((f . i) /\ (f . (i + 1)))) by A3;

      ( len f) in ( dom f) by A2, A5, FUNCT_1:def 2;

      then

       A8: 1 <= ( len f) by FINSEQ_3: 25;

      consider B0 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) such that

       A9: X = ( product B0) and for C be Subset of (A . ( indx B0)) st C = (B0 . ( indx B0)) holds C is strong closed_under_lines by A1, PENCIL_1: 29;

      let X1,Y1 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) such that

       A10: X = ( product X1) and

       A11: Y = ( product Y1);

      defpred P[ Element of NAT ] means for H be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st (f . $1) = ( product H) holds ( indx X1) = ( indx H) & for i be object st i <> ( indx X1) holds (X1 . i) = (H . i);

      

       A12: B0 = X1 by A10, A9, PUA2MSS1: 2;

      

       A13: for j be Element of NAT st 1 <= j & j < ( len f) holds P[j] implies P[(j + 1)]

      proof

        let j be Element of NAT ;

        assume that

         A14: 1 <= j and

         A15: j < ( len f);

        j in ( dom f) by A14, A15, FINSEQ_3: 25;

        then

         A16: (f . j) in ( rng f) by FUNCT_1: 3;

        

         A17: 1 <= (j + 1) by NAT_1: 11;

        (j + 1) <= ( len f) by A15, NAT_1: 13;

        then (j + 1) in ( dom f) by A17, FINSEQ_3: 25;

        then (f . (j + 1)) in ( rng f) by FUNCT_1: 3;

        then

        reconsider fj = (f . j), fj1 = (f . (j + 1)) as Subset of ( Segre_Product A) by A16;

        

         A18: ( card (fj /\ fj1)) c= ( card fj) by CARD_1: 11, XBOOLE_1: 17;

        

         A19: 2 c= ( card (fj /\ fj1)) by A7, A14, A15;

        then 2 c= ( card fj) by A18;

        then fj is non trivial closed_under_lines strong by A6, A16, PENCIL_1: 4;

        then

        consider B1 be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) such that

         A20: fj = ( product B1) and for C be Subset of (A . ( indx B1)) st C = (B1 . ( indx B1)) holds C is strong closed_under_lines by PENCIL_1: 29;

        assume

         A21: P[j];

        then

         A22: ( indx B0) = ( indx B1) by A12, A20;

        now

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

          assume

           A23: (f . (j + 1)) = ( product H);

          hence ( indx X1) = ( indx H) by A12, A20, A22, A19, PENCIL_1: 26;

          thus for i be object st i <> ( indx X1) holds (X1 . i) = (H . i)

          proof

            let i be object;

            assume

             A24: i <> ( indx X1);

            then

             A25: i <> ( indx B1) by A21, A20;

            

            thus (X1 . i) = (B1 . i) by A21, A20, A24

            .= (H . i) by A20, A19, A23, A25, PENCIL_1: 26;

          end;

        end;

        hence thesis;

      end;

      

       A26: P[1] by A10, A4, PUA2MSS1: 2;

      for i be Element of NAT st 1 <= i & i <= ( len f) holds P[i] from INT_1:sch 7( A26, A13);

      hence thesis by A11, A5, A8;

    end;

    begin

    theorem :: PENCIL_2:12

    for S be 1-sorted holds for T be non empty 1-sorted holds for f be Function of S, T st f is bijective holds (f " ) is bijective

    proof

      let S be 1-sorted;

      let T be non empty 1-sorted;

      let f be Function of S, T;

      assume

       A1: f is bijective;

      then

       A2: ( rng f) = ( [#] T) by FUNCT_2:def 3;

      then ( rng (f " )) = ( [#] S) by A1, TOPS_2: 49;

      then

       A3: (f " ) is onto by FUNCT_2:def 3;

      (f " ) is one-to-one by A1, A2, TOPS_2: 50;

      hence thesis by A3;

    end;

    definition

      let S,T be TopStruct;

      let f be Function of S, T;

      :: PENCIL_2:def4

      attr f is isomorphic means

      : Def4: f is bijective open & (f " ) is bijective open;

    end

    registration

      let S be non empty TopStruct;

      cluster isomorphic for Function of S, S;

      existence

      proof

        take f = ( id S);

        (f " ) = ( id S) by TOPGRP_1: 2;

        hence f is isomorphic;

      end;

    end

    definition

      let S be non empty TopStruct;

      mode Collineation of S is isomorphic Function of S, S;

    end

    definition

      let S be non empty non void TopStruct;

      let f be Collineation of S;

      let l be Block of S;

      :: original: .:

      redefine

      func f .: l -> Block of S ;

      coherence

      proof

        l in the topology of S;

        then

        reconsider L = l as Subset of S;

        

         A1: L is open by PRE_TOPC:def 2;

        f is open by Def4;

        then (f .: L) is open by A1, T_0TOPSP:def 2;

        hence thesis by PRE_TOPC:def 2;

      end;

    end

    definition

      let S be non empty non void TopStruct;

      let f be Collineation of S;

      let l be Block of S;

      :: original: "

      redefine

      func f " l -> Block of S ;

      coherence

      proof

        l in the topology of S;

        then

        reconsider L = l as Subset of S;

        

         A1: L is open by PRE_TOPC:def 2;

        

         A2: f is bijective by Def4;

        (f " ) = (f qua Function " ) by A2, TOPS_2:def 4;

        then

         A3: ((f " ) .: L) = (f " L) by A2, FUNCT_1: 85;

        (f " ) is open by Def4;

        then ((f " ) .: L) is open by A1, T_0TOPSP:def 2;

        hence thesis by A3, PRE_TOPC:def 2;

      end;

    end

    theorem :: PENCIL_2:13

    

     Th13: for S be non empty TopStruct holds for f be Collineation of S holds (f " ) is Collineation of S

    proof

      let S be non empty TopStruct;

      let f be Collineation of S;

      

       A1: (f " ) is bijective open by Def4;

      

       A2: f is bijective by Def4;

      then

       A3: ( rng f) = ( [#] S) by FUNCT_2:def 3;

      then ((f " ) " ) = f by A2, TOPS_2: 51;

      then

       A4: ((f " ) " ) is open by Def4;

      ((f " ) " ) is bijective by A2, A3, TOPS_2: 51;

      hence thesis by A1, A4, Def4;

    end;

    theorem :: PENCIL_2:14

    

     Th14: for S be non empty TopStruct holds for f be Collineation of S holds for X be Subset of S st X is non trivial holds (f .: X) is non trivial

    proof

      let S be non empty TopStruct;

      let f be Collineation of S;

      let X be Subset of S;

      assume X is non trivial;

      then 2 c= ( card X) by PENCIL_1: 4;

      then

      consider x,y be object such that

       A1: x in X and

       A2: y in X and

       A3: x <> y by PENCIL_1: 2;

      

       A4: ( dom f) = the carrier of S by FUNCT_2:def 1;

      then

       A5: (f . x) in (f .: X) by A1, FUNCT_1:def 6;

      

       A6: (f . y) in (f .: X) by A4, A2, FUNCT_1:def 6;

      f is bijective by Def4;

      then (f . x) <> (f . y) by A4, A1, A2, A3, FUNCT_1:def 4;

      then 2 c= ( card (f .: X)) by A5, A6, PENCIL_1: 2;

      hence thesis by PENCIL_1: 4;

    end;

    theorem :: PENCIL_2:15

    for S be non empty TopStruct holds for f be Collineation of S holds for X be Subset of S st X is non trivial holds (f " X) is non trivial

    proof

      let S be non empty TopStruct;

      let f be Collineation of S;

      let X be Subset of S;

      assume X is non trivial;

      then 2 c= ( card X) by PENCIL_1: 4;

      then

      consider x,y be object such that

       A1: x in X and

       A2: y in X and

       A3: x <> y by PENCIL_1: 2;

      f is bijective by Def4;

      then

       A4: ( rng f) = the carrier of S by FUNCT_2:def 3;

      then

      consider fx be object such that

       A5: fx in ( dom f) and

       A6: (f . fx) = x by A1, FUNCT_1:def 3;

      consider fy be object such that

       A7: fy in ( dom f) and

       A8: (f . fy) = y by A4, A2, FUNCT_1:def 3;

      

       A9: fy in (f " X) by A2, A7, A8, FUNCT_1:def 7;

      fx in (f " X) by A1, A5, A6, FUNCT_1:def 7;

      then 2 c= ( card (f " X)) by A3, A6, A8, A9, PENCIL_1: 2;

      hence thesis by PENCIL_1: 4;

    end;

    theorem :: PENCIL_2:16

    

     Th16: for S be non empty non void TopStruct holds for f be Collineation of S holds for X be Subset of S st X is strong holds (f .: X) is strong

    proof

      let S be non empty non void TopStruct;

      let f be Collineation of S;

      let X be Subset of S;

      assume

       A1: X is strong;

      thus (f .: X) is strong

      proof

        let a,b be Point of S;

        assume that

         A2: a in (f .: X) and

         A3: b in (f .: X);

        thus (a,b) are_collinear

        proof

          per cases ;

            suppose a = b;

            hence thesis;

          end;

            suppose

             A4: a <> b;

            consider B be object such that

             A5: B in ( dom f) and

             A6: B in X and

             A7: b = (f . B) by A3, FUNCT_1:def 6;

            consider A be object such that

             A8: A in ( dom f) and

             A9: A in X and

             A10: a = (f . A) by A2, FUNCT_1:def 6;

            reconsider A, B as Point of S by A8, A5;

            (A,B) are_collinear by A1, A9, A6;

            then

            consider l be Block of S such that

             A11: {A, B} c= l by A4, A10, A7;

            B in l by A11, ZFMISC_1: 32;

            then

             A12: b in (f .: l) by A5, A7, FUNCT_1:def 6;

            A in l by A11, ZFMISC_1: 32;

            then a in (f .: l) by A8, A10, FUNCT_1:def 6;

            then {a, b} c= (f .: l) by A12, ZFMISC_1: 32;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: PENCIL_2:17

    for S be non empty non void TopStruct holds for f be Collineation of S holds for X be Subset of S st X is strong holds (f " X) is strong

    proof

      let S be non empty non void TopStruct;

      let f be Collineation of S;

      reconsider g = (f " ) as Collineation of S by Th13;

      let X be Subset of S;

      assume X is strong;

      then

       A1: (g .: X) is strong by Th16;

      

       A2: f is bijective by Def4;

      then ( rng f) = ( [#] S) by FUNCT_2:def 3;

      hence thesis by A2, A1, TOPS_2: 55;

    end;

    theorem :: PENCIL_2:18

    

     Th18: for S be non empty non void TopStruct holds for f be Collineation of S holds for X be Subset of S st X is closed_under_lines holds (f .: X) is closed_under_lines

    proof

      let S be non empty non void TopStruct;

      let f be Collineation of S;

      let X be Subset of S;

      assume

       A1: X is closed_under_lines;

      thus (f .: X) is closed_under_lines

      proof

        let l be Block of S;

        assume 2 c= ( card (l /\ (f .: X)));

        then

        consider a,b be object such that

         A2: a in (l /\ (f .: X)) and

         A3: b in (l /\ (f .: X)) and

         A4: a <> b by PENCIL_1: 2;

        b in (f .: X) by A3, XBOOLE_0:def 4;

        then

        consider B be object such that

         A5: B in ( dom f) and

         A6: B in X and

         A7: b = (f . B) by FUNCT_1:def 6;

        b in l by A3, XBOOLE_0:def 4;

        then B in (f " l) by A5, A7, FUNCT_1:def 7;

        then

         A8: B in ((f " l) /\ X) by A6, XBOOLE_0:def 4;

        a in (f .: X) by A2, XBOOLE_0:def 4;

        then

        consider A be object such that

         A9: A in ( dom f) and

         A10: A in X and

         A11: a = (f . A) by FUNCT_1:def 6;

        a in l by A2, XBOOLE_0:def 4;

        then A in (f " l) by A9, A11, FUNCT_1:def 7;

        then A in ((f " l) /\ X) by A10, XBOOLE_0:def 4;

        then 2 c= ( card ((f " l) /\ X)) by A4, A11, A7, A8, PENCIL_1: 2;

        then (f " l) c= X by A1;

        then

         A12: (f .: (f " l)) c= (f .: X) by RELAT_1: 123;

        f is bijective by Def4;

        then

         A13: ( rng f) = the carrier of S by FUNCT_2:def 3;

        l in the topology of S;

        hence thesis by A13, A12, FUNCT_1: 77;

      end;

    end;

    theorem :: PENCIL_2:19

    for S be non empty non void TopStruct holds for f be Collineation of S holds for X be Subset of S st X is closed_under_lines holds (f " X) is closed_under_lines

    proof

      let S be non empty non void TopStruct;

      let f be Collineation of S;

      reconsider g = (f " ) as Collineation of S by Th13;

      let X be Subset of S;

      assume X is closed_under_lines;

      then

       A1: (g .: X) is closed_under_lines by Th18;

      

       A2: f is bijective by Def4;

      then ( rng f) = ( [#] S) by FUNCT_2:def 3;

      hence thesis by A2, A1, TOPS_2: 55;

    end;

    theorem :: PENCIL_2:20

    

     Th20: for S be non empty non void TopStruct holds for f be Collineation of S holds for X,Y be Subset of S st X is non trivial & Y is non trivial & (X,Y) are_joinable holds ((f .: X),(f .: Y)) are_joinable

    proof

      let S be non empty non void TopStruct;

      let f be Collineation of S;

      let X,Y be Subset of S;

      assume that

       A1: X is non trivial and

       A2: Y is non trivial and

       A3: (X,Y) are_joinable ;

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

       A4: X = (g . 1) and

       A5: Y = (g . ( len g)) and

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

       A7: for i be Element of NAT st 1 <= i & i < ( len g) holds 2 c= ( card ((g . i) /\ (g . (i + 1)))) by A3;

      deffunc F( set) = (f .: (g . $1));

      consider p be FinSequence such that

       A8: ( len p) = ( len g) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

      

       A9: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

      

       A10: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      ( rng p) c= ( bool the carrier of S)

      proof

        let o be object;

        assume o in ( rng p);

        then

        consider i be object such that

         A11: i in ( dom p) and

         A12: o = (p . i) by FUNCT_1:def 3;

        reconsider i as Element of NAT by A11;

        (g . i) in ( rng g) by A8, A10, A9, A11, FUNCT_1: 3;

        then

        reconsider gi = (g . i) as Subset of S;

        (p . i) = (f .: gi) by A8, A11;

        hence thesis by A12;

      end;

      then

      reconsider p as FinSequence of ( bool the carrier of S) by FINSEQ_1:def 4;

      take p;

      1 in ( dom g) by A1, A4, FUNCT_1:def 2;

      hence (f .: X) = (p . 1) by A4, A8, A10, A9;

      ( len g) in ( dom g) by A2, A5, FUNCT_1:def 2;

      hence (f .: Y) = (p . ( len p)) by A5, A8, A10, A9;

      thus for W be Subset of S st W in ( rng p) holds W is closed_under_lines strong

      proof

        let W be Subset of S;

        assume W in ( rng p);

        then

        consider i be object such that

         A13: i in ( dom p) and

         A14: W = (p . i) by FUNCT_1:def 3;

        reconsider i as Element of NAT by A13;

        (g . i) in ( rng g) by A8, A10, A9, A13, FUNCT_1: 3;

        then

        reconsider gi = (g . i) as Subset of S;

        gi in ( rng g) by A8, A10, A9, A13, FUNCT_1: 3;

        then

         A15: gi is strong closed_under_lines by A6;

        (p . i) = (f .: gi) by A8, A13;

        hence thesis by A14, A15, Th16, Th18;

      end;

      

       A16: f is bijective by Def4;

      thus for i be Element of NAT st 1 <= i & i < ( len p) holds 2 c= ( card ((p . i) /\ (p . (i + 1))))

      proof

        let i be Element of NAT ;

        assume that

         A17: 1 <= i and

         A18: i < ( len p);

        

         A19: ((g . i) /\ (g . (i + 1))) c= (g . i) by XBOOLE_1: 17;

        i in ( dom g) by A8, A17, A18, FINSEQ_3: 25;

        then (g . i) in ( rng g) by FUNCT_1: 3;

        then

        reconsider gg = ((g . i) /\ (g . (i + 1))) as Subset of S by A19, XBOOLE_1: 1;

        2 c= ( card ((g . i) /\ (g . (i + 1)))) by A7, A8, A17, A18;

        then gg is non trivial by PENCIL_1: 4;

        then (f .: gg) is non trivial by Th14;

        then

         A20: ((f .: (g . i)) /\ (f .: (g . (i + 1)))) is non trivial by A16, FUNCT_1: 62;

        

         A21: (i + 1) <= ( len p) by A18, NAT_1: 13;

        1 <= (i + 1) by A17, NAT_1: 13;

        then (i + 1) in ( dom p) by A21, FINSEQ_3: 25;

        then

         A22: (p . (i + 1)) = (f .: (g . (i + 1))) by A8;

        i in ( dom g) by A8, A17, A18, FINSEQ_3: 25;

        then (p . i) = (f .: (g . i)) by A8, A10, A9;

        hence thesis by A22, A20, PENCIL_1: 4;

      end;

    end;

    theorem :: PENCIL_2:21

    for S be non empty non void TopStruct holds for f be Collineation of S holds for X,Y be Subset of S st X is non trivial & Y is non trivial & (X,Y) are_joinable holds ((f " X),(f " Y)) are_joinable

    proof

      let S be non empty non void TopStruct;

      let f be Collineation of S;

      let X,Y be Subset of S;

      reconsider g = (f " ) as Collineation of S by Th13;

      assume that

       A1: X is non trivial and

       A2: Y is non trivial and

       A3: (X,Y) are_joinable ;

      

       A4: f is bijective by Def4;

      then

       A5: ( rng f) = ( [#] S) by FUNCT_2:def 3;

      then

       A6: (f " Y) = (g .: Y) by A4, TOPS_2: 55;

      (f " X) = (g .: X) by A4, A5, TOPS_2: 55;

      hence thesis by A6, A1, A2, A3, Th20;

    end;

    theorem :: PENCIL_2:22

    

     Th22: for I be 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 W be Subset of ( Segre_Product A) st W is non trivial strong closed_under_lines holds ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable }) is Segre-Coset of A

    proof

      let I be 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 W be Subset of ( Segre_Product A) such that

       A2: W is non trivial strong closed_under_lines;

      consider K be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) such that

       A3: W = ( product K) and

       A4: for S be Subset of (A . ( indx K)) st S = (K . ( indx K)) holds S is strong closed_under_lines by A2, PENCIL_1: 29;

      set O = ( [#] (A . ( indx K)));

      set B = ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable });

      B c= the carrier of ( Segre_Product A)

      proof

        let a be object;

        assume a in B;

        then

        consider y be set such that

         A5: a in y and

         A6: y in { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable } by TARSKI:def 4;

        ex Y be Subset of ( Segre_Product A) st y = Y & Y is non trivial strong closed_under_lines & (W,Y) are_joinable by A6;

        hence thesis by A5;

      end;

      then

      reconsider C = B as Subset of ( Segre_Product A);

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

      then (A . ( indx K)) in ( rng A) by FUNCT_1: 3;

      then

       A7: (A . ( indx K)) is non trivial by PENCIL_1:def 17;

      then

      reconsider L = (K +* (( indx K),O)) as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by Th7, PENCIL_1: 27;

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

      then (L . ( indx K)) = O by FUNCT_7: 31;

      then

       A8: ( indx K) = ( indx L) by A7, PENCIL_1:def 21;

      

       A9: ( product L) c= C

      proof

        K c= ( Carrier A) by PBOOLE:def 18;

        then (K . ( indx K)) c= (( Carrier A) . ( indx K));

        then

        reconsider S = (K . ( indx K)) as Subset of (A . ( indx K)) by YELLOW_6: 2;

        let y be object;

        

         A10: ( dom K) = I by PARTFUN1:def 2;

        

         A11: (A . ( indx K)) is strongly_connected by A1;

        assume y in ( product L);

        then

        consider z be Function such that

         A12: z = y and

         A13: ( dom z) = ( dom L) and

         A14: for a be object st a in ( dom L) holds (z . a) in (L . a) by CARD_3:def 5;

        

         A15: ( dom L) = I by PARTFUN1:def 2;

        then

        reconsider z as ManySortedSet of I by A13, PARTFUN1:def 2, RELAT_1:def 18;

        (z . ( indx K)) in (L . ( indx K)) by A14, A15;

        then

        reconsider zi = (z . ( indx K)) as Point of (A . ( indx K)) by A10, FUNCT_7: 31;

        S is non trivial strong closed_under_lines by A4, PENCIL_1:def 21;

        then

        consider f be FinSequence of ( bool the carrier of (A . ( indx K))) such that

         A16: S = (f . 1) and

         A17: zi in (f . ( len f)) and

         A18: for Z be Subset of (A . ( indx K)) st Z in ( rng f) holds Z is closed_under_lines strong and

         A19: for i be Nat st 1 <= i & i < ( len f) holds 2 c= ( card ((f . i) /\ (f . (i + 1)))) by A11;

        

         A20: ( len f) in ( dom f) by A17, FUNCT_1:def 2;

        then 1 in ( dom f) by FINSEQ_5: 6, RELAT_1: 38;

        then

         A21: 1 in ( Seg ( len f)) by FINSEQ_1:def 3;

        

         A22: (f . ( len f)) is non trivial

        proof

          reconsider l1 = (( len f) - 1) as Element of NAT by A20, FINSEQ_3: 26;

          

           A23: 1 <= ( len f) by A20, FINSEQ_3: 25;

          per cases by A23, XXREAL_0: 1;

            suppose ( len f) = 1;

            hence thesis by A16, PENCIL_1:def 21;

          end;

            suppose ( len f) > 1;

            then (1 + 1) <= ( len f) by NAT_1: 13;

            then

             A24: (2 - 1) <= l1 by XREAL_1: 9;

            

             A25: ( card ((f . l1) /\ (f . (l1 + 1)))) c= ( card (f . (l1 + 1))) by CARD_1: 11, XBOOLE_1: 17;

            l1 < (( len f) - 0 ) by XREAL_1: 15;

            then 2 c= ( card ((f . l1) /\ (f . (l1 + 1)))) by A19, A24;

            then 2 c= ( card (f . (l1 + 1))) by A25;

            hence thesis by PENCIL_1: 4;

          end;

        end;

        then

        reconsider ff = (f . ( len f)) as non trivial set;

        (L . ( indx K)) = O by A10, FUNCT_7: 31;

        then ( indx K) = ( indx L) by A7, PENCIL_1:def 21;

        then

        reconsider EL = (L +* (( indx K),ff)) as Segre-like non trivial-yielding ManySortedSet of I by PENCIL_1: 27;

        

         A26: ( dom z) = ( dom (L +* (( indx K),(f . ( len f))))) by A13, FUNCT_7: 30;

        deffunc F( set) = ( product (L +* (( indx K),(f . $1))));

        consider g be FinSequence such that

         A27: ( len g) = ( len f) & for k be Nat st k in ( dom g) holds (g . k) = F(k) from FINSEQ_1:sch 2;

        

         A28: ( rng g) c= ( bool the carrier of ( Segre_Product A))

        proof

          let a be object;

          reconsider aa = a as set by TARSKI: 1;

          

           A29: ( dom ( Carrier A)) = I by PARTFUN1:def 2;

          assume a in ( rng g);

          then

          consider k be object such that

           A30: k in ( dom g) and

           A31: a = (g . k) by FUNCT_1:def 3;

          reconsider k as Element of NAT by A30;

          

           A32: k in ( Seg ( len f)) by A27, A30, FINSEQ_1:def 3;

           A33:

          now

            let o be object;

            assume

             A34: o in I;

            

             A35: k in ( dom f) by A32, FINSEQ_1:def 3;

            per cases ;

              suppose

               A36: o <> ( indx K);

              then ((L +* (( indx K),(f . k))) . o) = (L . o) by FUNCT_7: 32;

              then

               A37: ((L +* (( indx K),(f . k))) . o) = (K . o) by A36, FUNCT_7: 32;

              K c= ( Carrier A) by PBOOLE:def 18;

              hence ((L +* (( indx K),(f . k))) . o) c= (( Carrier A) . o) by A34, A37;

            end;

              suppose

               A38: o = ( indx K);

              then ((L +* (( indx K),(f . k))) . o) = (f . k) by A15, FUNCT_7: 31;

              then ((L +* (( indx K),(f . k))) . o) in ( rng f) by A35, FUNCT_1: 3;

              then ((L +* (( indx K),(f . k))) . o) c= the carrier of (A . ( indx K));

              hence ((L +* (( indx K),(f . k))) . o) c= (( Carrier A) . o) by A38, YELLOW_6: 2;

            end;

          end;

          ( dom (L +* (( indx K),(f . k)))) = I by PARTFUN1:def 2;

          then ( product (L +* (( indx K),(f . k)))) c= ( product ( Carrier A)) by A29, A33, CARD_3: 27;

          then aa c= ( product ( Carrier A)) by A27, A30, A31;

          hence thesis;

        end;

        

         A39: ( dom g) = ( Seg ( len f)) by A27, FINSEQ_1:def 3;

        reconsider g as FinSequence of ( bool the carrier of ( Segre_Product A)) by A28, FINSEQ_1:def 4;

        ( len f) in ( dom g) by A20, A27, FINSEQ_3: 29;

        then

         A40: (g . ( len f)) in ( rng g) by FUNCT_1: 3;

        then

        reconsider Yb = (g . ( len f)) as Subset of ( Segre_Product A);

         A41:

        now

          let o be object;

          assume o in I;

          per cases ;

            suppose

             A42: o <> ( indx K);

            then ((L +* (( indx K),(f . 1))) . o) = (L . o) by FUNCT_7: 32;

            hence ((L +* (( indx K),(f . 1))) . o) = (K . o) by A42, FUNCT_7: 32;

          end;

            suppose o = ( indx K);

            hence ((L +* (( indx K),(f . 1))) . o) = (K . o) by A15, A16, FUNCT_7: 31;

          end;

        end;

        

         A43: for V be Subset of ( Segre_Product A) st V in ( rng g) holds V is closed_under_lines strong

        proof

          let V be Subset of ( Segre_Product A);

          assume V in ( rng g);

          then

          consider n1 be object such that

           A44: n1 in ( dom g) and

           A45: V = (g . n1) by FUNCT_1:def 3;

          reconsider n = n1 as Element of NAT by A44;

          n in ( Seg ( len f)) by A27, A44, FINSEQ_1:def 3;

          then

           A46: n in ( dom f) by FINSEQ_1:def 3;

          (f . n) is non trivial

          proof

            

             A47: n <= ( len f) by A46, FINSEQ_3: 25;

            per cases by A46, A47, FINSEQ_3: 25, XXREAL_0: 1;

              suppose 1 <= n & n = ( len f);

              hence thesis by A22;

            end;

              suppose

               A48: 1 <= n & n < ( len f);

              

               A49: ( card ((f . n) /\ (f . (n + 1)))) c= ( card (f . n)) by CARD_1: 11, XBOOLE_1: 17;

              2 c= ( card ((f . n) /\ (f . (n + 1)))) by A19, A48;

              then 2 c= ( card (f . n)) by A49;

              hence thesis by PENCIL_1: 4;

            end;

          end;

          then

          reconsider fn = (f . n) as non trivial set;

          

           A50: (L +* (( indx K),(f . n))) c= ( Carrier A)

          proof

            let o be object;

            assume

             A51: o in I;

            per cases ;

              suppose

               A52: o <> ( indx K);

              

               A53: L c= ( Carrier A) by PBOOLE:def 18;

              ((L +* (( indx K),(f . n))) . o) = (L . o) by A52, FUNCT_7: 32;

              hence thesis by A51, A53;

            end;

              suppose

               A54: o = ( indx K);

              then ((L +* (( indx K),(f . n))) . o) = (f . n) by A15, FUNCT_7: 31;

              then ((L +* (( indx K),(f . n))) . o) in ( rng f) by A46, FUNCT_1: 3;

              then ((L +* (( indx K),(f . n))) . o) c= the carrier of (A . ( indx K));

              hence thesis by A54, YELLOW_6: 2;

            end;

          end;

          (L . ( indx K)) = O by A10, FUNCT_7: 31;

          then ( indx K) = ( indx L) by A7, PENCIL_1:def 21;

          then

          reconsider LI = (L +* (( indx K),fn)) as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by A50, PBOOLE:def 18, PENCIL_1: 27;

          reconsider LI as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A);

          

           A55: (LI . ( indx K)) = fn by A15, FUNCT_7: 31;

          then

           A56: ( indx LI) = ( indx K) by PENCIL_1:def 21;

           A57:

          now

            let D be Subset of (A . ( indx LI));

            assume D = (LI . ( indx LI));

            then D in ( rng f) by A46, A55, A56, FUNCT_1: 3;

            hence D is strong closed_under_lines by A18, A56;

          end;

          (g . n) = ( product (L +* (( indx K),(f . n)))) by A27, A44;

          hence thesis by A45, A57, PENCIL_1: 29;

        end;

        

         A58: ( len f) in ( Seg ( len f)) by A20, FINSEQ_1:def 3;

        then Yb = ( product EL) by A27, A39;

        then

         A59: Yb is non trivial strong closed_under_lines by A40, A43;

        

         A60: for i be Element of NAT st 1 <= i & i < ( len g) holds 2 c= ( card ((g . i) /\ (g . (i + 1))))

        proof

          consider l1 be object such that

           A61: l1 in ( product L) by XBOOLE_0:def 1;

          let i be Element of NAT ;

          assume that

           A62: 1 <= i and

           A63: i < ( len g);

          i in ( Seg ( len f)) by A27, A62, A63, FINSEQ_1: 1;

          then

           A64: (g . i) = ( product (L +* (( indx K),(f . i)))) by A27, A39;

          2 c= ( card ((f . i) /\ (f . (i + 1)))) by A19, A27, A62, A63;

          then

          consider a,b be object such that

           A65: a in ((f . i) /\ (f . (i + 1))) and

           A66: b in ((f . i) /\ (f . (i + 1))) and

           A67: a <> b by PENCIL_1: 2;

          consider l be Function such that l = l1 and

           A68: ( dom l) = ( dom L) and

           A69: for o be object st o in ( dom L) holds (l . o) in (L . o) by A61, CARD_3:def 5;

          reconsider l as ManySortedSet of I by A15, A68, PARTFUN1:def 2, RELAT_1:def 18;

          set l1 = (l +* (( indx K),a)), l2 = (l +* (( indx K),b));

          

           A70: (i + 1) <= ( len g) by A63, NAT_1: 13;

           A71:

          now

            let o be object;

            assume o in ( dom (L +* (( indx K),(f . i))));

            then

             A72: o in I;

            then

             A73: o in ( dom l) by PARTFUN1:def 2;

            per cases ;

              suppose

               A74: o = ( indx K);

              then (l1 . o) = a by A73, FUNCT_7: 31;

              then (l1 . o) in (f . i) by A65, XBOOLE_0:def 4;

              hence (l1 . o) in ((L +* (( indx K),(f . i))) . o) by A15, A74, FUNCT_7: 31;

            end;

              suppose

               A75: o <> ( indx K);

              then

               A76: (l1 . o) = (l . o) by FUNCT_7: 32;

              (l . o) in (L . o) by A15, A69, A72;

              hence (l1 . o) in ((L +* (( indx K),(f . i))) . o) by A75, A76, FUNCT_7: 32;

            end;

          end;

          1 <= (i + 1) by A62, NAT_1: 13;

          then (i + 1) in ( Seg ( len f)) by A27, A70, FINSEQ_1: 1;

          then

           A77: (g . (i + 1)) = ( product (L +* (( indx K),(f . (i + 1))))) by A27, A39;

           A78:

          now

            let o be object;

            assume o in ( dom (L +* (( indx K),(f . i))));

            then

             A79: o in I;

            then

             A80: o in ( dom l) by PARTFUN1:def 2;

            per cases ;

              suppose

               A81: o = ( indx K);

              then (l2 . o) = b by A80, FUNCT_7: 31;

              then (l2 . o) in (f . i) by A66, XBOOLE_0:def 4;

              hence (l2 . o) in ((L +* (( indx K),(f . i))) . o) by A15, A81, FUNCT_7: 31;

            end;

              suppose

               A82: o <> ( indx K);

              then

               A83: (l2 . o) = (l . o) by FUNCT_7: 32;

              (l . o) in (L . o) by A15, A69, A79;

              hence (l2 . o) in ((L +* (( indx K),(f . i))) . o) by A82, A83, FUNCT_7: 32;

            end;

          end;

           A84:

          now

            let o be object;

            assume o in ( dom (L +* (( indx K),(f . (i + 1)))));

            then

             A85: o in I;

            then

             A86: o in ( dom l) by PARTFUN1:def 2;

            per cases ;

              suppose

               A87: o = ( indx K);

              then (l1 . o) = a by A86, FUNCT_7: 31;

              then (l1 . o) in (f . (i + 1)) by A65, XBOOLE_0:def 4;

              hence (l1 . o) in ((L +* (( indx K),(f . (i + 1)))) . o) by A15, A87, FUNCT_7: 31;

            end;

              suppose

               A88: o <> ( indx K);

              then

               A89: (l1 . o) = (l . o) by FUNCT_7: 32;

              (l . o) in (L . o) by A15, A69, A85;

              hence (l1 . o) in ((L +* (( indx K),(f . (i + 1)))) . o) by A88, A89, FUNCT_7: 32;

            end;

          end;

          ( dom l1) = I by PARTFUN1:def 2

          .= ( dom (L +* (( indx K),(f . (i + 1))))) by PARTFUN1:def 2;

          then

           A90: l1 in ( product (L +* (( indx K),(f . (i + 1))))) by A84, CARD_3: 9;

           A91:

          now

            let o be object;

            assume o in ( dom (L +* (( indx K),(f . (i + 1)))));

            then

             A92: o in I;

            then

             A93: o in ( dom l) by PARTFUN1:def 2;

            per cases ;

              suppose

               A94: o = ( indx K);

              then (l2 . o) = b by A93, FUNCT_7: 31;

              then (l2 . o) in (f . (i + 1)) by A66, XBOOLE_0:def 4;

              hence (l2 . o) in ((L +* (( indx K),(f . (i + 1)))) . o) by A15, A94, FUNCT_7: 31;

            end;

              suppose

               A95: o <> ( indx K);

              then

               A96: (l2 . o) = (l . o) by FUNCT_7: 32;

              (l . o) in (L . o) by A15, A69, A92;

              hence (l2 . o) in ((L +* (( indx K),(f . (i + 1)))) . o) by A95, A96, FUNCT_7: 32;

            end;

          end;

          ( dom l2) = I by PARTFUN1:def 2

          .= ( dom (L +* (( indx K),(f . (i + 1))))) by PARTFUN1:def 2;

          then

           A97: l2 in ( product (L +* (( indx K),(f . (i + 1))))) by A91, CARD_3: 9;

          ( dom l2) = I by PARTFUN1:def 2

          .= ( dom (L +* (( indx K),(f . i)))) by PARTFUN1:def 2;

          then l2 in ( product (L +* (( indx K),(f . i)))) by A78, CARD_3: 9;

          then

           A98: l2 in ((g . i) /\ (g . (i + 1))) by A64, A77, A97, XBOOLE_0:def 4;

          (l1 . ( indx K)) = a by A15, A68, FUNCT_7: 31;

          then

           A99: l1 <> l2 by A15, A67, A68, FUNCT_7: 31;

          ( dom l1) = I by PARTFUN1:def 2

          .= ( dom (L +* (( indx K),(f . i)))) by PARTFUN1:def 2;

          then l1 in ( product (L +* (( indx K),(f . i)))) by A71, CARD_3: 9;

          then l1 in ((g . i) /\ (g . (i + 1))) by A64, A77, A90, XBOOLE_0:def 4;

          hence thesis by A99, A98, PENCIL_1: 2;

        end;

         A100:

        now

          let o be object;

          assume o in ( dom (L +* (( indx K),(f . ( len f)))));

          then

           A101: o in I;

          per cases ;

            suppose o = ( indx K);

            hence (z . o) in ((L +* (( indx K),(f . ( len f)))) . o) by A15, A17, FUNCT_7: 31;

          end;

            suppose

             A102: o <> ( indx K);

            (z . o) in (L . o) by A14, A15, A101;

            hence (z . o) in ((L +* (( indx K),(f . ( len f)))) . o) by A102, FUNCT_7: 32;

          end;

        end;

        (L +* (( indx K),(f . 1))) = K by A41;

        then W = (g . 1) by A3, A27, A39, A21;

        then (W,Yb) are_joinable by A27, A43, A60;

        then

         A103: Yb in { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable } by A59;

        Yb = ( product (L +* (( indx K),(f . ( len f))))) by A27, A39, A58;

        then y in Yb by A12, A26, A100, CARD_3: 9;

        hence thesis by A103, TARSKI:def 4;

      end;

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

      then

       A104: (L . ( indx L)) = ( [#] (A . ( indx L))) by A8, FUNCT_7: 31;

      C c= ( product L)

      proof

        let c be object;

        assume c in C;

        then

        consider y be set such that

         A105: c in y and

         A106: y in { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable } by TARSKI:def 4;

        consider Y be Subset of ( Segre_Product A) such that

         A107: y = Y and

         A108: Y is non trivial strong closed_under_lines and

         A109: (W,Y) are_joinable by A106;

        reconsider c1 = c as ManySortedSet of I by A105, A107, PENCIL_1: 14;

        consider M be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) such that

         A110: Y = ( product M) and for S be Subset of (A . ( indx M)) st S = (M . ( indx M)) holds S is strong closed_under_lines by A108, PENCIL_1: 29;

        

         A111: ( dom M) = I by PARTFUN1:def 2

        .= ( dom L) by PARTFUN1:def 2;

        

         A112: ( dom K) = I by PARTFUN1:def 2

        .= ( dom L) by PARTFUN1:def 2;

        

         A113: for a be object st a in ( dom L) holds (c1 . a) in (L . a)

        proof

          let a be object;

          assume

           A114: a in ( dom L);

          then

          reconsider a1 = a as Element of I;

          per cases ;

            suppose

             A115: a = ( indx K);

            M c= ( Carrier A) by PBOOLE:def 18;

            then (M . a1) c= (( Carrier A) . a1);

            then

             A116: (M . a1) c= the carrier of (A . a1) by YELLOW_6: 2;

            (c1 . a) in (M . a) by A105, A107, A110, A111, A114, CARD_3: 9;

            then (c1 . a) in O by A115, A116;

            hence thesis by A112, A114, A115, FUNCT_7: 31;

          end;

            suppose

             A117: a <> ( indx K);

            (c1 . a) in (M . a) by A105, A107, A110, A111, A114, CARD_3: 9;

            then (c1 . a) in (K . a) by A2, A3, A108, A109, A110, A117, Th11;

            hence thesis by A117, FUNCT_7: 32;

          end;

        end;

        ( dom c1) = I by PARTFUN1:def 2

        .= ( dom L) by PARTFUN1:def 2;

        hence thesis by A113, CARD_3: 9;

      end;

      then C = ( product L) by A9;

      hence thesis by A104, Def2;

    end;

    theorem :: PENCIL_2:23

    

     Th23: for I be 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 B be set holds B is Segre-Coset of A iff ex W be Subset of ( Segre_Product A) st W is non trivial strong closed_under_lines & B = ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable })

    proof

      let I be 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 B be set;

      thus B is Segre-Coset of A implies ex W be Subset of ( Segre_Product A) st W is non trivial strong closed_under_lines & B = ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable })

      proof

        assume B is Segre-Coset of A;

        then

        reconsider BB = B as Segre-Coset of A;

        consider L be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) such that

         A2: BB = ( product L) and

         A3: (L . ( indx L)) = ( [#] (A . ( indx L))) by Def2;

        set K1 = the Block of (A . ( indx L));

        consider V be object such that

         A4: V in ( product L) by XBOOLE_0:def 1;

        K1 in the topology of (A . ( indx L));

        then

        reconsider K = K1 as Subset of (A . ( indx L));

        

         A5: ex g be Function st g = V & ( dom g) = ( dom L) & for i be object st i in ( dom L) holds (g . i) in (L . i) by A4, CARD_3:def 5;

        

         A6: ( dom L) = I by PARTFUN1:def 2;

        then

        reconsider V as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;

        for i be object st i in I holds (V . i) is Element of (( Carrier A) . i)

        proof

          let i be object;

          assume

           A7: i in I;

          L c= ( Carrier A) by PBOOLE:def 18;

          then

           A8: (L . i) c= (( Carrier A) . i) by A7;

          (V . i) in (L . i) by A6, A5, A7;

          hence thesis by A8;

        end;

        then

        reconsider V as Element of ( Carrier A) by PBOOLE:def 14;

        reconsider VV = {V} as ManySortedSubset of ( Carrier A) by PENCIL_1: 11;

        reconsider X = (VV +* (( indx L),K)) as ManySortedSubset of ( Carrier A) by Th7;

        2 c= ( card K) by PENCIL_1:def 6;

        then

         A9: K is non trivial by PENCIL_1: 4;

        then

        reconsider X as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by PENCIL_1: 9, PENCIL_1: 10;

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

        then

         A10: (X . ( indx L)) = K by FUNCT_7: 31;

        then ( indx X) = ( indx L) by A9, PENCIL_1:def 21;

        then

        reconsider pX = ( product X) as Block of ( Segre_Product A) by A10, PENCIL_1: 24;

        

         A11: for i be object st i in I holds (X . i) c= (L . i)

        proof

          let i be object;

          assume

           A12: i in I;

          per cases ;

            suppose i <> ( indx L);

            then (X . i) = (VV . i) by FUNCT_7: 32;

            then

             A13: (X . i) = {(V . i)} by A12, PZFMISC1:def 1;

            (V . i) in (L . i) by A6, A5, A12;

            hence thesis by A13, ZFMISC_1: 31;

          end;

            suppose i = ( indx L);

            hence thesis by A3, A10;

          end;

        end;

        pX in the topology of ( Segre_Product A);

        then

        reconsider psX = pX as Subset of ( Segre_Product A);

        take psX;

        thus

         A14: psX is non trivial strong closed_under_lines by PENCIL_1: 20, PENCIL_1: 21;

        then

        reconsider Z = ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (psX,Y) are_joinable }) as Segre-Coset of A by A1, Th22;

        (psX,psX) are_joinable by A14, Th10;

        then

         A15: psX in { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (psX,Y) are_joinable } by A14;

        

         A16: psX c= Z by A15, TARSKI:def 4;

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

        then psX c= B by A2, A6, A11, CARD_3: 27;

        then psX c= (B /\ Z) by A16, XBOOLE_1: 19;

        then

         A17: ( card psX) c= ( card (B /\ Z)) by CARD_1: 11;

        2 c= ( card pX) by PENCIL_1:def 6;

        then BB = Z by A17, Th8, XBOOLE_1: 1;

        hence thesis;

      end;

      given W be Subset of ( Segre_Product A) such that

       A18: W is non trivial strong closed_under_lines and

       A19: B = ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable });

      thus thesis by A1, A18, A19, Th22;

    end;

    theorem :: PENCIL_2:24

    

     Th24: for I be 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 B be Segre-Coset of A holds for f be Collineation of ( Segre_Product A) holds (f .: B) is Segre-Coset of A

    proof

      let I be 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 B be Segre-Coset of A;

      consider W be Subset of ( Segre_Product A) such that

       A2: W is non trivial strong closed_under_lines and

       A3: B = ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable }) by A1, Th23;

      let f be Collineation of ( Segre_Product A);

      reconsider g = (f " ) as Collineation of ( Segre_Product A) by Th13;

      

       A4: ( dom f) = the carrier of ( Segre_Product A) by FUNCT_2:def 1;

      

       A5: ( dom g) = the carrier of ( Segre_Product A) by FUNCT_2:def 1;

      

       A6: f is bijective by Def4;

      then

       A7: ( rng f) = the carrier of ( Segre_Product A) by FUNCT_2:def 3;

      

       A8: ( rng f) = ( [#] ( Segre_Product A)) by A6, FUNCT_2:def 3;

      

       A9: (f .: B) = ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & ((f .: W),Y) are_joinable })

      proof

        

         A10: W c= (f " (f .: W)) by A4, FUNCT_1: 76;

        (f " (f .: W)) c= W by A6, FUNCT_1: 82;

        then

         A11: (f " (f .: W)) = W by A10;

        thus (f .: B) c= ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & ((f .: W),Y) are_joinable })

        proof

          let o be object;

          assume o in (f .: B);

          then

          consider u be object such that

           A12: u in ( dom f) and

           A13: u in B and

           A14: o = (f . u) by FUNCT_1:def 6;

          consider y be set such that

           A15: u in y and

           A16: y in { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & (W,Y) are_joinable } by A3, A13, TARSKI:def 4;

          consider Y be Subset of ( Segre_Product A) such that

           A17: y = Y and

           A18: Y is non trivial strong closed_under_lines and

           A19: (W,Y) are_joinable by A16;

          

           A20: ((f .: W),(f .: Y)) are_joinable by A2, A18, A19, Th20;

          (f .: Y) is non trivial strong closed_under_lines by A18, Th14, Th16, Th18;

          then

           A21: (f .: Y) in { Z where Z be Subset of ( Segre_Product A) : Z is non trivial strong closed_under_lines & ((f .: W),Z) are_joinable } by A20;

          o in (f .: Y) by A12, A14, A15, A17, FUNCT_1:def 6;

          hence thesis by A21, TARSKI:def 4;

        end;

        let o be object;

        assume o in ( union { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & ((f .: W),Y) are_joinable });

        then

        consider u be set such that

         A22: o in u and

         A23: u in { Y where Y be Subset of ( Segre_Product A) : Y is non trivial strong closed_under_lines & ((f .: W),Y) are_joinable } by TARSKI:def 4;

        consider Y be Subset of ( Segre_Product A) such that

         A24: u = Y and

         A25: Y is non trivial strong closed_under_lines and

         A26: ((f .: W),Y) are_joinable by A23;

        

         A27: (g .: Y) is non trivial strong closed_under_lines by A25, Th14, Th16, Th18;

        (f .: W) is non trivial strong closed_under_lines by A2, Th14, Th16, Th18;

        then ((g .: (f .: W)),(g .: Y)) are_joinable by A25, A26, Th20;

        then (W,(g .: Y)) are_joinable by A6, A8, A11, TOPS_2: 55;

        then

         A28: (g .: Y) in { Z where Z be Subset of ( Segre_Product A) : Z is non trivial strong closed_under_lines & (W,Z) are_joinable } by A27;

        (g . o) in (g .: Y) by A5, A22, A24, FUNCT_1:def 6;

        then

         A29: (g . o) in B by A3, A28, TARSKI:def 4;

        o = (f . ((f qua Function " ) . o)) by A6, A7, A22, A24, FUNCT_1: 35;

        then o = (f . (g . o)) by A6, TOPS_2:def 4;

        hence thesis by A4, A29, FUNCT_1:def 6;

      end;

      (f .: W) is non trivial strong closed_under_lines by A2, Th14, Th16, Th18;

      hence thesis by A1, A9, Th23;

    end;

    theorem :: PENCIL_2:25

    for I be 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 B be Segre-Coset of A holds for f be Collineation of ( Segre_Product A) holds (f " B) is Segre-Coset of A

    proof

      let I be 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 B be Segre-Coset of A;

      let f be Collineation of ( Segre_Product A);

      reconsider g = (f " ) as Collineation of ( Segre_Product A) by Th13;

      

       A2: f is bijective by Def4;

      then ( rng f) = ( [#] ( Segre_Product A)) by FUNCT_2:def 3;

      then (f " B) = (g .: B) by A2, TOPS_2: 55;

      hence thesis by A1, Th24;

    end;