pencil_1.miz



    begin

    theorem :: PENCIL_1:1

    

     Th1: for f,g be Function st ( product f) = ( product g) holds f is non-empty implies g is non-empty

    proof

      let f,g be Function;

      assume

       A1: ( product f) = ( product g);

      now

        assume that

         A2: f is non-empty and

         A3: not g is non-empty;

        ex n be object st n in ( dom g) & (g . n) is empty by A3, FUNCT_1:def 9;

        then {} in ( rng g) by FUNCT_1:def 3;

        then ( product g) = {} by CARD_3: 26;

        then {} in ( rng f) by A1, CARD_3: 26;

        then ex n be object st n in ( dom f) & (f . n) = {} by FUNCT_1:def 3;

        hence contradiction by A2, FUNCT_1:def 9;

      end;

      hence thesis;

    end;

    theorem :: PENCIL_1:2

    

     Th2: for X be set holds 2 c= ( card X) iff ex x,y be object st x in X & y in X & x <> y

    proof

      let X be set;

      thus 2 c= ( card X) implies ex x,y be object st x in X & y in X & x <> y

      proof

        assume 2 c= ( card X);

        then ( card 2) c= ( card X);

        then

        consider f be Function such that

         A1: f is one-to-one and

         A2: ( dom f) = 2 and

         A3: ( rng f) c= X by CARD_1: 10;

        take x = (f . 0 );

        take y = (f . 1);

        

         A4: 0 in ( dom f) by A2, CARD_1: 50, TARSKI:def 2;

        then (f . 0 ) in ( rng f) by FUNCT_1:def 3;

        hence x in X by A3;

        

         A5: 1 in ( dom f) by A2, CARD_1: 50, TARSKI:def 2;

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

        hence y in X by A3;

        thus thesis by A1, A4, A5, FUNCT_1:def 4;

      end;

      given x,y be object such that

       A6: x in X & y in X and

       A7: x <> y;

       {x, y} c= X by A6, TARSKI:def 2;

      then ( card {x, y}) c= ( card X) by CARD_1: 11;

      hence thesis by A7, CARD_2: 57;

    end;

    theorem :: PENCIL_1:3

    

     Th3: for X be set st 2 c= ( card X) holds for x be object holds ex y be object st y in X & x <> y

    proof

      let X be set;

      assume 2 c= ( card X);

      then

      consider a,b be object such that

       A1: a in X and

       A2: b in X & a <> b by Th2;

      let x be object;

      per cases ;

        suppose

         A3: x = a;

        take b;

        thus thesis by A2, A3;

      end;

        suppose

         A4: x <> a;

        take a;

        thus thesis by A1, A4;

      end;

    end;

    theorem :: PENCIL_1:4

    

     Th4: for X be set holds 2 c= ( card X) iff X is non trivial

    proof

      let X be set;

      set z = the Element of X;

      thus 2 c= ( card X) implies X is non trivial

      proof

        assume 2 c= ( card X);

        then

        consider x,y be object such that

         A1: x in X and

         A2: y in X and

         A3: x <> y by Th2;

        now

          given z be object such that

           A4: X = {z};

          

          thus x = z by A1, A4, TARSKI:def 1

          .= y by A2, A4, TARSKI:def 1;

        end;

        hence thesis by A1, A3, ZFMISC_1: 131;

      end;

      assume

       A5: X is non trivial;

      then X c= {z} implies X = {z};

      then

      consider w be object such that

       A6: w in X and

       A7: not w in {z} by A5;

      w <> z by A7, TARSKI:def 1;

      hence thesis by A6, Th2;

    end;

    theorem :: PENCIL_1:5

    

     Th5: for X be set holds 3 c= ( card X) iff ex x,y,z be object st x in X & y in X & z in X & x <> y & x <> z & y <> z

    proof

      let X be set;

      thus 3 c= ( card X) implies ex x,y,z be object st x in X & y in X & z in X & x <> y & x <> z & y <> z

      proof

        assume 3 c= ( card X);

        then ( card 3) c= ( card X);

        then

        consider f be Function such that

         A1: f is one-to-one and

         A2: ( dom f) = 3 and

         A3: ( rng f) c= X by CARD_1: 10;

        take x = (f . 0 );

        take y = (f . 1);

        take z = (f . 2);

        

         A4: 0 in ( dom f) by A2, ENUMSET1:def 1, YELLOW11: 1;

        then (f . 0 ) in ( rng f) by FUNCT_1:def 3;

        hence x in X by A3;

        

         A5: 1 in ( dom f) by A2, ENUMSET1:def 1, YELLOW11: 1;

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

        hence y in X by A3;

        

         A6: 2 in ( dom f) by A2, ENUMSET1:def 1, YELLOW11: 1;

        then (f . 2) in ( rng f) by FUNCT_1:def 3;

        hence z in X by A3;

        thus x <> y by A1, A4, A5, FUNCT_1:def 4;

        thus x <> z by A1, A4, A6, FUNCT_1:def 4;

        thus thesis by A1, A5, A6, FUNCT_1:def 4;

      end;

      given x,y,z be object such that

       A7: x in X & y in X & z in X and

       A8: x <> y & x <> z & y <> z;

       {x, y, z} c= X by A7, ENUMSET1:def 1;

      then ( card {x, y, z}) c= ( card X) by CARD_1: 11;

      hence thesis by A8, CARD_2: 58;

    end;

    theorem :: PENCIL_1:6

    

     Th6: for X be set st 3 c= ( card X) holds for x,y be object holds ex z be object st z in X & x <> z & y <> z

    proof

      let X be set;

      assume 3 c= ( card X);

      then

      consider a,b,c be object such that

       A1: a in X and

       A2: b in X and

       A3: c in X and

       A4: a <> b and

       A5: a <> c & b <> c by Th5;

      let x,y be object;

      per cases ;

        suppose x <> a & y <> a;

        hence thesis by A1;

      end;

        suppose x <> a & y = a & x = b;

        hence thesis by A3, A5;

      end;

        suppose x <> a & y = a & x <> b;

        hence thesis by A2, A4;

      end;

        suppose x = a & y <> a & y = b;

        hence thesis by A3, A5;

      end;

        suppose x = a & y <> a & y <> b;

        hence thesis by A2, A4;

      end;

        suppose x = a & y = a;

        hence thesis by A2, A4;

      end;

    end;

    begin

    definition

      let S be TopStruct;

      mode Block of S is Element of the topology of S;

    end

    definition

      let S be TopStruct;

      let x,y be Point of S;

      :: PENCIL_1:def1

      pred x,y are_collinear means x = y or ex l be Block of S st {x, y} c= l;

    end

    definition

      let S be TopStruct;

      let T be Subset of S;

      :: PENCIL_1:def2

      attr T is closed_under_lines means for l be Block of S st 2 c= ( card (l /\ T)) holds l c= T;

      :: PENCIL_1:def3

      attr T is strong means for x,y be Point of S st x in T & y in T holds (x,y) are_collinear ;

    end

    definition

      let S be TopStruct;

      :: PENCIL_1:def4

      attr S is void means

      : Def4: the topology of S is empty;

      :: PENCIL_1:def5

      attr S is degenerated means the carrier of S is Block of S;

      :: PENCIL_1:def6

      attr S is with_non_trivial_blocks means

      : Def6: for k be Block of S holds 2 c= ( card k);

      :: PENCIL_1:def7

      attr S is identifying_close_blocks means

      : Def7: for k,l be Block of S st 2 c= ( card (k /\ l)) holds k = l;

      :: PENCIL_1:def8

      attr S is truly-partial means ex x,y be Point of S st not (x,y) are_collinear ;

      :: PENCIL_1:def9

      attr S is without_isolated_points means

      : Def9: for x be Point of S holds ex l be Block of S st x in l;

      :: PENCIL_1:def10

      attr S is connected means for x,y be Point of S holds ex f be FinSequence of the carrier of S st x = (f . 1) & y = (f . ( len f)) & for i be Nat st 1 <= i & i < ( len f) holds for a,b be Point of S st a = (f . i) & b = (f . (i + 1)) holds (a,b) are_collinear ;

      :: PENCIL_1:def11

      attr S is strongly_connected means for x be Point of S holds for X be Subset of S st X is closed_under_lines strong holds ex f be FinSequence of ( bool the carrier of S) st X = (f . 1) & x in (f . ( len f)) & (for W be Subset of S st W in ( rng f) holds W is closed_under_lines strong) & for i be Nat st 1 <= i & i < ( len f) holds 2 c= ( card ((f . i) /\ (f . (i + 1))));

    end

    theorem :: PENCIL_1:7

    

     Th7: for X be non empty set st 3 c= ( card X) holds for S be TopStruct st the carrier of S = X & the topology of S = { L where L be Subset of X : 2 = ( card L) } holds S is non empty non void non degenerated non truly-partial with_non_trivial_blocks identifying_close_blocks without_isolated_points

    proof

      let X be non empty set;

      assume

       A1: 3 c= ( card X);

      

       A2: ( Segm 2) c= ( Segm 3) by NAT_1: 39;

      then 2 c= ( card X) by A1;

      then

      consider x,y be object such that

       A3: x in X & y in X and

       A4: x <> y by Th2;

       {x, y} c= X by A3, TARSKI:def 2;

      then

      reconsider l = {x, y} as Subset of X;

      let S be TopStruct;

      assume that

       A5: the carrier of S = X and

       A6: the topology of S = { L where L be Subset of X : 2 = ( card L) };

      thus S is non empty by A5;

      2 = ( card l) by A4, CARD_2: 57;

      then

       A7: l in the topology of S by A6;

      then

      reconsider F = { L where L be Subset of X : 2 = ( card L) } as non empty set by A6;

      thus S is non void by A7;

      now

        assume X in F;

        then ex L be Subset of X st X = L & 2 = ( card L);

        then ( Segm 3) c= ( Segm 2) by A1;

        hence contradiction by NAT_1: 39;

      end;

      then not X is Element of F;

      hence S is non degenerated by A5, A6;

      for x,y be Point of S holds (x,y) are_collinear

      proof

        let x,y be Point of S;

        per cases ;

          suppose

           A8: x = y;

          consider z be object such that

           A9: z in X and

           A10: z <> x by A1, A2, Th3, XBOOLE_1: 1;

          reconsider z as Point of S by A5, A9;

          

           A11: {x, y} c= {x, z}

          proof

            let a be object;

            assume a in {x, y};

            then a = x or a = y by TARSKI:def 2;

            hence thesis by A8, TARSKI:def 2;

          end;

           {x, z} c= X

          proof

            let a be object;

            assume a in {x, z};

            then a = x or a = z by TARSKI:def 2;

            hence thesis by A5;

          end;

          then

          reconsider l = {x, z} as Subset of X;

          ( card l) = 2 by A10, CARD_2: 57;

          then l in the topology of S by A6;

          hence thesis by A11;

        end;

          suppose

           A12: x <> y;

           {x, y} c= X

          proof

            let a be object;

            assume a in {x, y};

            then a = x or a = y by TARSKI:def 2;

            hence thesis by A5;

          end;

          then

          reconsider l = {x, y} as Subset of X;

          ( card {x, y}) = 2 by A12, CARD_2: 57;

          then l in the topology of S by A6;

          hence thesis;

        end;

      end;

      hence S is non truly-partial;

      thus S is with_non_trivial_blocks

      proof

        let k be Block of S;

        k in the topology of S by A7;

        then ex m be Subset of X st m = k & ( card m) = 2 by A6;

        hence thesis;

      end;

      thus S is identifying_close_blocks

      proof

        let k,l be Block of S;

        assume 2 c= ( card (k /\ l));

        then

        consider a,b be object such that

         A13: a in (k /\ l) & b in (k /\ l) and

         A14: a <> b by Th2;

        

         A15: {a, b} c= (k /\ l) by A13, TARSKI:def 2;

        l in the topology of S by A7;

        then

         A16: ex n be Subset of X st n = l & ( card n) = 2 by A6;

        then

        reconsider l1 = l as finite set;

        

         A17: (k /\ l) c= l1 by XBOOLE_1: 17;

        k in the topology of S by A7;

        then

         A18: ex m be Subset of X st m = k & ( card m) = 2 by A6;

        then

        reconsider k1 = k as finite set;

        

         A19: ( card {a, b}) = 2 by A14, CARD_2: 57;

        (k /\ l) c= k1 by XBOOLE_1: 17;

        then {a, b} = k1 by A18, A15, A19, CARD_2: 102, XBOOLE_1: 1;

        hence thesis by A15, A19, A16, A17, CARD_2: 102, XBOOLE_1: 1;

      end;

      thus S is without_isolated_points

      proof

        let x be Point of S;

        consider z be object such that

         A20: z in X and

         A21: z <> x by A1, A2, Th3, XBOOLE_1: 1;

         {x, z} c= X

        proof

          let a be object;

          assume a in {x, z};

          then a = x or a = z by TARSKI:def 2;

          hence thesis by A5, A20;

        end;

        then

        reconsider l = {x, z} as Subset of X;

        ( card {x, z}) = 2 by A21, CARD_2: 57;

        then l in the topology of S by A6;

        then

        reconsider l as Block of S;

        take l;

        thus thesis by TARSKI:def 2;

      end;

    end;

    theorem :: PENCIL_1:8

    

     Th8: for X be non empty set st 3 c= ( card X) holds for K be Subset of X st ( card K) = 2 holds for S be TopStruct st the carrier of S = X & the topology of S = ({ L where L be Subset of X : 2 = ( card L) } \ {K}) holds S is non empty non void non degenerated truly-partial with_non_trivial_blocks identifying_close_blocks without_isolated_points

    proof

      let X be non empty set;

      assume

       A1: 3 c= ( card X);

      let K be Subset of X;

      assume

       A2: ( card K) = 2;

      then

      reconsider K9 = K as finite Subset of X;

      consider x,y be object such that

       A3: x <> y and

       A4: K9 = {x, y} by A2, CARD_2: 60;

      let S be TopStruct;

      assume that

       A5: the carrier of S = X and

       A6: the topology of S = ({ L where L be Subset of X : 2 = ( card L) } \ {K});

      reconsider x, y as Point of S by A5, A4, ZFMISC_1: 32;

      consider z be object such that

       A7: z in X and

       A8: z <> x and

       A9: z <> y by A1, Th6;

       {x, z} c= X

      proof

        let a be object;

        assume a in {x, z};

        then a = x or a = z by TARSKI:def 2;

        hence thesis by A5, A7;

      end;

      then

      reconsider l = {x, z} as Subset of X;

      ( card l) = 2 by A8, CARD_2: 57;

      then

       A10: z in l & l in { L where L be Subset of X : 2 = ( card L) } by TARSKI:def 2;

      thus S is non empty by A5;

       not z in K9 by A4, A8, A9, TARSKI:def 2;

      then

       A11: not { L where L be Subset of X : 2 = ( card L) } c= {K} by A10, TARSKI:def 1;

      then

       A12: ({ L where L be Subset of X : 2 = ( card L) } \ {K}) is non empty by XBOOLE_1: 37;

      hence S is non void by A6;

      reconsider F = ({ L where L be Subset of X : 2 = ( card L) } \ {K}) as non empty set by A11, XBOOLE_1: 37;

      now

        assume X in F;

        then X in { L where L be Subset of X : 2 = ( card L) };

        then ex L be Subset of X st X = L & 2 = ( card L);

        then ( Segm 3) c= ( Segm 2) by A1;

        hence contradiction by NAT_1: 39;

      end;

      then not X is Element of F;

      hence S is non degenerated by A5, A6;

      thus S is truly-partial

      proof

        take x, y;

        for l be Block of S holds not {x, y} c= l

        proof

          let l be Block of S;

          l in { L where L be Subset of X : 2 = ( card L) } by A6, A12, XBOOLE_0:def 5;

          then

          consider L be Subset of X such that

           A13: l = L and

           A14: ( card L) = 2;

          reconsider L9 = L as finite Subset of X by A14;

          consider a,b be object such that a <> b and

           A15: L9 = {a, b} by A14, CARD_2: 60;

          

           A16: not l in {K} by A6, A12, XBOOLE_0:def 5;

          now

            assume

             A17: {x, y} c= l;

            then y in L9 by A13, ZFMISC_1: 32;

            then

             A18: y = a or y = b by A15, TARSKI:def 2;

            x in L9 by A13, A17, ZFMISC_1: 32;

            then x = a or x = b by A15, TARSKI:def 2;

            hence contradiction by A3, A4, A16, A13, A15, A18, TARSKI:def 1;

          end;

          hence thesis;

        end;

        hence thesis by A3;

      end;

      thus S is with_non_trivial_blocks

      proof

        let k be Block of S;

        k in { L where L be Subset of X : 2 = ( card L) } by A6, A12, XBOOLE_0:def 5;

        then ex m be Subset of X st m = k & ( card m) = 2;

        hence thesis;

      end;

      thus S is identifying_close_blocks

      proof

        let k,l be Block of S;

        assume 2 c= ( card (k /\ l));

        then

        consider a,b be object such that

         A19: a in (k /\ l) & b in (k /\ l) and

         A20: a <> b by Th2;

        

         A21: {a, b} c= (k /\ l) by A19, TARSKI:def 2;

        l in { L where L be Subset of X : 2 = ( card L) } by A6, A12, XBOOLE_0:def 5;

        then

         A22: ex n be Subset of X st n = l & ( card n) = 2;

        then

        reconsider l1 = l as finite set;

        

         A23: (k /\ l) c= l1 by XBOOLE_1: 17;

        k in { L where L be Subset of X : 2 = ( card L) } by A6, A12, XBOOLE_0:def 5;

        then

         A24: ex m be Subset of X st m = k & ( card m) = 2;

        then

        reconsider k1 = k as finite set;

        

         A25: ( card {a, b}) = 2 by A20, CARD_2: 57;

        (k /\ l) c= k1 by XBOOLE_1: 17;

        then {a, b} = k1 by A24, A21, A25, CARD_2: 102, XBOOLE_1: 1;

        hence thesis by A21, A25, A22, A23, CARD_2: 102, XBOOLE_1: 1;

      end;

      

       A26: ( Segm 2) c= ( Segm 3) by NAT_1: 39;

      thus S is without_isolated_points

      proof

        let p be Point of S;

        per cases ;

          suppose

           A27: p <> x & p <> y;

          consider z be object such that

           A28: z in X and

           A29: z <> p by A1, A26, Th3, XBOOLE_1: 1;

           {p, z} c= X

          proof

            let a be object;

            assume a in {p, z};

            then a = p or a = z by TARSKI:def 2;

            hence thesis by A5, A28;

          end;

          then

          reconsider el = {p, z} as Subset of X;

          ( card {p, z}) = 2 by A29, CARD_2: 57;

          then

           A30: el in { L where L be Subset of X : 2 = ( card L) };

          p in el by TARSKI:def 2;

          then el <> K by A4, A27, TARSKI:def 2;

          then not el in {K} by TARSKI:def 1;

          then

          reconsider el as Block of S by A6, A30, XBOOLE_0:def 5;

          take el;

          thus thesis by TARSKI:def 2;

        end;

          suppose

           A31: p = x or p = y;

          consider z be object such that

           A32: z in X and

           A33: z <> x & z <> y by A1, Th6;

           {p, z} c= X

          proof

            let a be object;

            assume a in {p, z};

            then a = p or a = z by TARSKI:def 2;

            hence thesis by A5, A32;

          end;

          then

          reconsider el = {p, z} as Subset of X;

          ( card {p, z}) = 2 by A31, A33, CARD_2: 57;

          then

           A34: el in { L where L be Subset of X : 2 = ( card L) };

          z in el by TARSKI:def 2;

          then el <> K by A4, A33, TARSKI:def 2;

          then not el in {K} by TARSKI:def 1;

          then

          reconsider el as Block of S by A6, A34, XBOOLE_0:def 5;

          take el;

          thus thesis by TARSKI:def 2;

        end;

      end;

    end;

    registration

      cluster strict non empty non void non degenerated non truly-partial with_non_trivial_blocks identifying_close_blocks without_isolated_points for TopStruct;

      existence

      proof

        { L where L be Subset of ( Segm 3) : 2 = ( card L) } c= ( bool 3)

        proof

          let x be object;

          assume x in { L where L be Subset of ( Segm 3) : 2 = ( card L) };

          then ex L be Subset of 3 st x = L & 2 = ( card L);

          hence thesis;

        end;

        then

        reconsider B = { L where L be Subset of 3 : 2 = ( card L) } as Subset-Family of 3;

        take TopStruct (# 3, B #);

        3 = ( card 3);

        then for S be TopStruct st the carrier of S = ( Segm 3) & the topology of S = { L where L be Subset of ( Segm 3) : 2 = ( card L) } holds S is non empty non void non degenerated non truly-partial with_non_trivial_blocks identifying_close_blocks without_isolated_points by Th7;

        hence thesis;

      end;

      cluster strict non empty non void non degenerated truly-partial with_non_trivial_blocks identifying_close_blocks without_isolated_points for TopStruct;

      existence

      proof

        ( Segm 2) c= ( Segm 3) & ( card 2) = 2 by NAT_1: 39;

        then

        consider K be Subset of 3 such that

         A1: ( card K) = 2;

        { L where L be Subset of 3 : 2 = ( card L) } c= ( bool 3)

        proof

          let x be object;

          assume x in { L where L be Subset of 3 : 2 = ( card L) };

          then ex L be Subset of 3 st x = L & 2 = ( card L);

          hence thesis;

        end;

        then

        reconsider B = ({ L where L be Subset of ( Segm 3) : 2 = ( card L) } \ {K}) as Subset-Family of ( Segm 3) by XBOOLE_1: 1;

        take TopStruct (# ( Segm 3), B #);

        3 c= ( card 3);

        then for K be Subset of ( Segm 3) st ( card K) = 2 holds for S be TopStruct st the carrier of S = ( Segm 3) & the topology of S = ({ L where L be Subset of ( Segm 3) : 2 = ( card L) } \ {K}) holds S is non empty non void non degenerated truly-partial with_non_trivial_blocks identifying_close_blocks without_isolated_points by Th8;

        hence thesis by A1;

      end;

    end

    registration

      let S be non void TopStruct;

      cluster the topology of S -> non empty;

      coherence by Def4;

    end

    definition

      let S be without_isolated_points TopStruct;

      let x,y be Point of S;

      :: original: are_collinear

      redefine

      :: PENCIL_1:def12

      pred x,y are_collinear means ex l be Block of S st {x, y} c= l;

      compatibility

      proof

        thus (x,y) are_collinear implies ex l be Block of S st {x, y} c= l

        proof

          assume

           A1: (x,y) are_collinear ;

          per cases ;

            suppose

             A2: x = y;

            consider l be Block of S such that

             A3: x in l by Def9;

            take l;

            thus thesis by A2, A3, ZFMISC_1: 32;

          end;

            suppose x <> y;

            hence thesis by A1;

          end;

        end;

        given l be Block of S such that

         A4: {x, y} c= l;

        thus thesis by A4;

      end;

    end

    definition

      mode PLS is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct;

    end

    definition

      ::$Canceled

      let F be Relation;

      :: PENCIL_1:def14

      attr F is non-void-yielding means for S be TopStruct st S in ( rng F) holds S is non void;

    end

    definition

      let F be TopStruct-yielding Function;

      :: original: non-void-yielding

      redefine

      :: PENCIL_1:def15

      attr F is non-void-yielding means for i be set st i in ( rng F) holds i is non void TopStruct;

      compatibility by WAYBEL18:def 1;

    end

    definition

      let F be Relation;

      :: PENCIL_1:def16

      attr F is trivial-yielding means

      : Def16: for S be set st S in ( rng F) holds S is trivial;

    end

    definition

      let F be Relation;

      :: PENCIL_1:def17

      attr F is non-Trivial-yielding means

      : Def17: for S be 1-sorted st S in ( rng F) holds S is non trivial;

    end

    registration

      cluster non-Trivial-yielding -> non-Empty for Relation;

      coherence ;

    end

    definition

      let F be 1-sorted-yielding Function;

      :: original: non-Trivial-yielding

      redefine

      :: PENCIL_1:def18

      attr F is non-Trivial-yielding means for i be set st i in ( rng F) holds i is non trivial 1-sorted;

      compatibility

      proof

        hereby

          assume

           A1: F is non-Trivial-yielding;

          let i be set;

          assume

           A2: i in ( rng F);

          then ex x be object st x in ( dom F) & i = (F . x) by FUNCT_1:def 3;

          hence i is non trivial 1-sorted by A1, A2, PRALG_1:def 11;

        end;

        assume

         A3: for i be set st i in ( rng F) holds i is non trivial 1-sorted;

        let S be 1-sorted;

        thus thesis by A3;

      end;

    end

    definition

      let I be non empty set;

      let A be TopStruct-yielding ManySortedSet of I;

      let j be Element of I;

      :: original: .

      redefine

      func A . j -> TopStruct ;

      coherence

      proof

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

        then (A . j) in ( rng A) by FUNCT_1:def 3;

        hence thesis;

      end;

    end

    definition

      let F be Relation;

      :: PENCIL_1:def19

      attr F is PLS-yielding means

      : Def19: for x be set st x in ( rng F) holds x is PLS;

    end

    registration

      cluster PLS-yielding -> non-Empty TopStruct-yielding for Function;

      coherence ;

      cluster PLS-yielding -> non-void-yielding for TopStruct-yielding Function;

      coherence ;

      cluster PLS-yielding -> non-Trivial-yielding for TopStruct-yielding Function;

      coherence

      proof

        let f be TopStruct-yielding Function such that

         A1: f is PLS-yielding;

        let x be set;

        assume x in ( rng f);

        then

        reconsider S1 = x as with_non_trivial_blocks non void non empty TopStruct by A1;

        consider s be object such that

         A2: s in the topology of S1 by XBOOLE_0:def 1;

        reconsider s as Block of S1 by A2;

        2 c= ( card s) by Def6;

        then ex s1,s2 be object st s1 in s & s2 in s & s1 <> s2 by Th2;

        hence thesis by A2, STRUCT_0:def 10;

      end;

    end

    registration

      let I be set;

      cluster PLS-yielding for ManySortedSet of I;

      existence

      proof

        set R = the PLS;

        take (I --> R);

        let v be set;

        assume

         A1: v in ( rng (I --> R));

        ( rng (I --> R)) c= {R} by FUNCOP_1: 13;

        hence thesis by A1, TARSKI:def 1;

      end;

    end

    definition

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let j be Element of I;

      :: original: .

      redefine

      func A . j -> PLS ;

      coherence

      proof

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

        then (A . j) in ( rng A) by FUNCT_1:def 3;

        hence thesis by Def19;

      end;

    end

    definition

      let I be set;

      let A be ManySortedSet of I;

      :: PENCIL_1:def20

      attr A is Segre-like means

      : Def20: ex i be Element of I st for j be Element of I st i <> j holds (A . j) is 1 -element;

    end

    registration

      let I be set;

      let A be ManySortedSet of I;

      cluster {A} -> trivial-yielding;

      coherence

      proof

        let a be set;

        assume a in ( rng {A});

        then

        consider i be object such that

         A1: i in ( dom {A}) & a = ( {A} . i) by FUNCT_1:def 3;

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

        then a = {(A . i)} by A1, PZFMISC1:def 1;

        hence thesis;

      end;

    end

    theorem :: PENCIL_1:9

    for I be non empty set holds for A be ManySortedSet of I holds for i be Element of I holds for S be non trivial set holds (A +* (i,S)) is non trivial-yielding

    proof

      let I be non empty set;

      let A be ManySortedSet of I;

      let i be Element of I;

      let S be non trivial set;

      take a = ((A +* (i,S)) . i);

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

      then i in ( dom A);

      then i in ( dom (A +* (i,S))) by FUNCT_7: 30;

      hence a in ( rng (A +* (i,S))) by FUNCT_1:def 3;

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

      hence thesis by FUNCT_7: 31;

    end;

    registration

      let I be non empty set;

      let A be ManySortedSet of I;

      cluster {A} -> Segre-like;

      coherence

      proof

        set i = the Element of I;

        take i;

        let j be Element of I such that i <> j;

        ( {A} . j) = {(A . j)} by PZFMISC1:def 1;

        hence thesis;

      end;

    end

    theorem :: PENCIL_1:10

    for I be non empty set holds for A be ManySortedSet of I holds for i,S be set holds ( {A} +* (i,S)) is Segre-like

    proof

      let I be non empty set;

      let A be ManySortedSet of I;

      let i,S be set;

      per cases ;

        suppose not i in I;

        then not i in ( dom {A}) by PARTFUN1:def 2;

        hence thesis by FUNCT_7:def 3;

      end;

        suppose i in I;

        then

        reconsider i as Element of I;

        take i;

        let j be Element of I such that

         A1: i <> j;

        ( {A} . j) = {(A . j)} by PZFMISC1:def 1;

        hence thesis by A1, FUNCT_7: 32;

      end;

    end;

    theorem :: PENCIL_1:11

    

     Th11: for I be non empty set holds for A be non-Empty 1-sorted-yielding ManySortedSet of I holds for B be Element of ( Carrier A) holds {B} is ManySortedSubset of ( Carrier A)

    proof

      let I be non empty set;

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

      let B be Element of ( Carrier A);

       {B} c= ( Carrier A)

      proof

        let i be object;

        assume

         A1: i in I;

        then

        reconsider j = i as Element of I;

        j in ( dom A) by A1, PARTFUN1:def 2;

        then (A . j) in ( rng A) by FUNCT_1:def 3;

        then

         A2: (A . j) is non empty by YELLOW_6:def 2;

        (B . j) is Element of (( Carrier A) . j) by PBOOLE:def 14;

        then (B . j) is Element of (A . j) by YELLOW_6: 2;

        then {(B . j)} c= the carrier of (A . j) by A2, ZFMISC_1: 31;

        then ( {B} . j) c= the carrier of (A . j) by PZFMISC1:def 1;

        hence thesis by YELLOW_6: 2;

      end;

      hence thesis by PBOOLE:def 18;

    end;

    registration

      let I be non empty set;

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

      cluster Segre-like trivial-yielding non-empty for ManySortedSubset of ( Carrier A);

      existence

      proof

        set B = the Element of ( Carrier A);

        reconsider C = {B} as ManySortedSubset of ( Carrier A) by Th11;

        take C;

        thus thesis;

      end;

    end

    registration

      let I be non empty set;

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

      cluster Segre-like non trivial-yielding non-empty for ManySortedSubset of ( Carrier A);

      existence

      proof

        set B = the Element of ( Carrier A);

        set i1 = the Element of I;

        

         A1: ex R be 1-sorted st R = (A . i1) & the carrier of R = (( Carrier A) . i1) by PRALG_1:def 15;

        then

        reconsider b1 = (B . i1) as Element of (A . i1) by PBOOLE:def 14;

        reconsider B as ManySortedSet of I;

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

        then (A . i1) in ( rng A) by FUNCT_1:def 3;

        then (A . i1) is non trivial by Def17;

        then

        reconsider Ai1 = the carrier of (A . i1) as non trivial set;

        ex x1,x2 be Element of Ai1 st x1 <> x2 by SUBSET_1:def 7;

        then 2 c= ( card the carrier of (A . i1)) by Th2;

        then

        consider b2 be object such that

         A2: b2 in the carrier of (A . i1) and

         A3: b1 <> b2 by Th3;

        reconsider b2 as Element of (A . i1) by A2;

        set B1 = (B +* (i1,b2));

        

         A4: for i be set st i in I holds (B1 . i) is Element of (( Carrier A) . i)

        proof

          let i be set such that

           A5: i in I;

          per cases ;

            suppose i <> i1;

            then (B1 . i) = (B . i) by FUNCT_7: 32;

            hence thesis by A5, PBOOLE:def 14;

          end;

            suppose

             A6: i = i1;

            then i1 in ( dom B) by A5, PARTFUN1:def 2;

            hence thesis by A1, A6, FUNCT_7: 31;

          end;

        end;

         {B, B1} c= ( Carrier A)

        proof

          let i be object;

          assume

           A7: i in I;

          then

          reconsider j = i as Element of I;

          j in ( dom A) by A7, PARTFUN1:def 2;

          then (A . j) in ( rng A) by FUNCT_1:def 3;

          then

           A8: (A . j) is non empty by YELLOW_6:def 2;

          (B . j) is Element of (( Carrier A) . j) by PBOOLE:def 14;

          then

           A9: (B . j) is Element of (A . j) by YELLOW_6: 2;

          (B1 . j) is Element of (( Carrier A) . j) by A4;

          then (B1 . j) is Element of (A . j) by YELLOW_6: 2;

          then {(B . j), (B1 . j)} c= the carrier of (A . j) by A8, A9, ZFMISC_1: 32;

          then ( {B, B1} . j) c= the carrier of (A . j) by PZFMISC1:def 2;

          hence thesis by YELLOW_6: 2;

        end;

        then

        reconsider C = {B, B1} as ManySortedSubset of ( Carrier A) by PBOOLE:def 18;

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

        then (B1 . i1) = b2 by FUNCT_7: 31;

        then

         A10: (C . i1) = {b1, b2} by PZFMISC1:def 2;

         A11:

        now

          assume (C . i1) is trivial;

          then (C . i1) is empty or ex x be object st (C . i1) = {x} by ZFMISC_1: 131;

          hence contradiction by A3, A10, ZFMISC_1: 5;

        end;

        take C;

        thus C is Segre-like

        proof

          take i1;

          let j be Element of I;

          assume i1 <> j;

          then (B . j) = (B1 . j) by FUNCT_7: 32;

          

          then (C . j) = {(B . j), (B . j)} by PZFMISC1:def 2

          .= {(B . j)} by ENUMSET1: 29;

          hence thesis;

        end;

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

        then (C . i1) in ( rng C) by FUNCT_1:def 3;

        hence C is non trivial-yielding by A11;

        thus thesis;

      end;

    end

    registration

      let I be non empty set;

      cluster Segre-like non trivial-yielding for ManySortedSet of I;

      existence

      proof

        set B = the ManySortedSet of I;

        set i = the Element of I;

        take C = ( {B} +* (i, { 0 , 1}));

        thus C is Segre-like

        proof

          take i;

          let j be Element of I;

          assume j <> i;

          then

           A1: (C . j) = ( {B} . j) by FUNCT_7: 32;

          j in I;

          then

           A2: j in ( dom {B}) by PARTFUN1:def 2;

          then (C . j) in ( rng {B}) by A1, FUNCT_1:def 3;

          then (C . j) is non empty trivial by A2, A1, Def16, FUNCT_1:def 9;

          hence (C . j) is 1 -element;

        end;

        thus C is non trivial-yielding

        proof

          take S = (C . i);

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

          hence S in ( rng C) by FUNCT_1:def 3;

          ( dom {B}) = I by PARTFUN1:def 2;

          then

           A3: (C . i) = { 0 , 1} by FUNCT_7: 31;

           0 in { 0 , 1} & 1 in { 0 , 1} by TARSKI:def 2;

          then 2 c= ( card { 0 , 1}) by Th2;

          hence thesis by A3, Th4;

        end;

      end;

    end

    definition

      let I be non empty set;

      let B be Segre-like non trivial-yielding ManySortedSet of I;

      :: PENCIL_1:def21

      func indx (B) -> Element of I means

      : Def21: (B . it ) is non trivial;

      existence

      proof

        consider i be Element of I such that

         A1: for j be Element of I st i <> j holds (B . j) is 1 -element by Def20;

        take i;

        now

          assume

           A2: (B . i) is trivial;

          for S be set st S in ( rng B) holds S is trivial

          proof

            let S be set;

            assume S in ( rng B);

            then

            consider j be object such that

             A3: j in ( dom B) and

             A4: S = (B . j) by FUNCT_1:def 3;

            reconsider j as Element of I by A3, PARTFUN1:def 2;

            per cases ;

              suppose i = j;

              hence thesis by A2, A4;

            end;

              suppose i <> j;

              then (B . j) is 1 -element by A1;

              hence thesis by A4;

            end;

          end;

          hence contradiction by Def16;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let i1,i2 be Element of I;

        assume that

         A5: (B . i1) is non trivial and

         A6: (B . i2) is non trivial;

        consider i be Element of I such that

         A7: for j be Element of I st i <> j holds (B . j) is 1 -element by Def20;

        

         A8: not (B . i2) is 1 -element by A6;

         not (B . i1) is 1 -element by A5;

        

        hence i1 = i by A7

        .= i2 by A7, A8;

      end;

    end

    theorem :: PENCIL_1:12

    

     Th12: for I be non empty set holds for A be Segre-like non trivial-yielding ManySortedSet of I holds for i be Element of I st i <> ( indx A) holds (A . i) is 1 -element

    proof

      let I be non empty set;

      let A be Segre-like non trivial-yielding ManySortedSet of I;

      let i be Element of I;

      consider j be Element of I such that

       A1: for k be Element of I st k <> j holds (A . k) is 1 -element by Def20;

       A2:

      now

        assume ( indx A) <> j;

        then (A . ( indx A)) is 1 -element by A1;

        hence contradiction by Def21;

      end;

      assume i <> ( indx A);

      hence thesis by A1, A2;

    end;

    registration

      let I be non empty set;

      cluster Segre-like non trivial-yielding -> non-empty for ManySortedSet of I;

      coherence

      proof

        let f be ManySortedSet of I;

        assume f is Segre-like non trivial-yielding;

        then

        reconsider g = f as Segre-like non trivial-yielding ManySortedSet of I;

        now

          assume {} in ( rng g);

          then

          consider i be object such that

           A1: i in ( dom f) and

           A2: (g . i) = {} by FUNCT_1:def 3;

          reconsider i as Element of I by A1, PARTFUN1:def 2;

          per cases ;

            suppose i = ( indx g);

            hence contradiction by A2, Def21;

          end;

            suppose i <> ( indx g);

            then (g . i) is 1 -element by Th12;

            hence contradiction by A2;

          end;

        end;

        hence thesis by RELAT_1:def 9;

      end;

    end

    theorem :: PENCIL_1:13

    

     Th13: for I be non empty set holds for A be ManySortedSet of I holds 2 c= ( card ( product A)) iff A is non-empty non trivial-yielding

    proof

      let I be non empty set;

      let A be ManySortedSet of I;

      

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

      thus 2 c= ( card ( product A)) implies A is non-empty non trivial-yielding

      proof

        assume 2 c= ( card ( product A));

        then

        consider a,b be object such that

         A2: a in ( product A) and

         A3: b in ( product A) and

         A4: a <> b by Th2;

        consider a1 be Function such that

         A5: a = a1 & ( dom a1) = ( dom A) and

         A6: for e be object st e in ( dom A) holds (a1 . e) in (A . e) by A2, CARD_3:def 5;

        thus A is non-empty by A1, A6;

        consider b1 be Function such that

         A7: b = b1 & ( dom b1) = ( dom A) and

         A8: for e be object st e in ( dom A) holds (b1 . e) in (A . e) by A3, CARD_3:def 5;

        consider e be object such that

         A9: e in ( dom A) and

         A10: (b1 . e) <> (a1 . e) by A4, A5, A7, FUNCT_1: 2;

        thus A is non trivial-yielding

        proof

          take (A . e);

          thus (A . e) in ( rng A) by A9, FUNCT_1:def 3;

          (a1 . e) in (A . e) & (b1 . e) in (A . e) by A6, A8, A9;

          then 2 c= ( card (A . e)) by A10, Th2;

          hence thesis by Th4;

        end;

      end;

      assume

       A11: A is non-empty non trivial-yielding;

      then

      consider r be set such that

       A12: r in ( rng A) and

       A13: r is non trivial;

      now

        assume {} in ( rng A);

        then ex o be object st o in ( dom A) & (A . o) = {} by FUNCT_1:def 3;

        hence contradiction by A1, A11;

      end;

      then ( product A) is non empty by CARD_3: 26;

      then

      consider a1 be object such that

       A14: a1 in ( product A);

      consider p be object such that

       A15: p in ( dom A) and

       A16: r = (A . p) by A12, FUNCT_1:def 3;

      consider a be Function such that

       A17: a = a1 and

       A18: ( dom a) = ( dom A) and

       A19: for o be object st o in ( dom A) holds (a . o) in (A . o) by A14, CARD_3:def 5;

      reconsider a as ManySortedSet of I by A1, A18, PARTFUN1:def 2, RELAT_1:def 18;

      2 c= ( card r) by A13, Th4;

      then

      consider t be object such that

       A20: t in r and

       A21: t <> (a . p) by Th3;

      reconsider p as Element of I by A15, PARTFUN1:def 2;

      set b = (a +* (p,t));

       A22:

      now

        let o be object;

        assume

         A23: o in ( dom A);

        per cases ;

          suppose o <> p;

          then (b . o) = (a . o) by FUNCT_7: 32;

          hence (b . o) in (A . o) by A19, A23;

        end;

          suppose o = p;

          hence (b . o) in (A . o) by A18, A15, A16, A20, FUNCT_7: 31;

        end;

      end;

      ( dom b) = I by PARTFUN1:def 2

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

      then

       A24: b in ( product A) by A22, CARD_3: 9;

      (b . p) = t by A18, A15, FUNCT_7: 31;

      hence thesis by A14, A17, A21, A24, Th2;

    end;

    registration

      let I be non empty set;

      let B be Segre-like non trivial-yielding ManySortedSet of I;

      cluster ( product B) -> non trivial;

      coherence

      proof

        consider f be object such that

         A1: f in ( product B) by XBOOLE_0:def 1;

        

         A2: ex g be Function st g = f & ( dom g) = ( dom B) & for x be object st x in ( dom B) holds (g . x) in (B . x) by A1, CARD_3:def 5;

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

        then

        reconsider f as ManySortedSet of I by A2, PARTFUN1:def 2, RELAT_1:def 18;

        (B . ( indx B)) is non trivial by Def21;

        then 2 c= ( card (B . ( indx B))) by Th4;

        then

        consider y be object such that

         A3: y in (B . ( indx B)) and

         A4: y <> (f . ( indx B)) by Th3;

        set l = (f +* (( indx B),y));

        

         A5: for x be object st x in ( dom B) holds (l . x) in (B . x)

        proof

          let x be object;

          assume

           A6: x in ( dom B);

          then x in I by PARTFUN1:def 2;

          then

           A7: x in ( dom f) by PARTFUN1:def 2;

          per cases ;

            suppose x = ( indx B);

            hence thesis by A3, A7, FUNCT_7: 31;

          end;

            suppose x <> ( indx B);

            then (l . x) = (f . x) by FUNCT_7: 32;

            hence thesis by A2, A6;

          end;

        end;

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

        then

         A8: (l . ( indx B)) = y by FUNCT_7: 31;

        ( dom l) = I by PARTFUN1:def 2

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

        then l in ( product B) by A5, CARD_3:def 5;

        then 2 c= ( card ( product B)) by A1, A4, A8, Th2;

        hence thesis by Th4;

      end;

    end

    begin

    definition

      let I be non empty set;

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

      :: PENCIL_1:def22

      func Segre_Blocks (A) -> Subset-Family of ( product ( Carrier A)) means

      : Def22: for x be set holds x in it iff ex B be Segre-like ManySortedSubset of ( Carrier A) st x = ( product B) & ex i be Element of I st (B . i) is Block of (A . i);

      existence

      proof

        defpred P[ object] means ex B be Segre-like ManySortedSubset of ( Carrier A) st $1 = ( product B) & ex i be Element of I st (B . i) is Block of (A . i);

        consider S be set such that

         A1: for x be object holds x in S iff x in ( bool ( product ( Carrier A))) & P[x] from XBOOLE_0:sch 1;

        S c= ( bool ( product ( Carrier A))) by A1;

        then

        reconsider S as Subset-Family of ( product ( Carrier A));

        take S;

        let x be set;

        thus x in S implies ex B be Segre-like ManySortedSubset of ( Carrier A) st x = ( product B) & ex i be Element of I st (B . i) is Block of (A . i) by A1;

        given B be Segre-like ManySortedSubset of ( Carrier A) such that

         A2: x = ( product B) and

         A3: ex i be Element of I st (B . i) is Block of (A . i);

        x c= ( product ( Carrier A))

        proof

          let a be object;

          assume a in x;

          then

          consider g be Function such that

           A4: g = a and

           A5: ( dom g) = ( dom B) and

           A6: for y be object st y in ( dom B) holds (g . y) in (B . y) by A2, CARD_3:def 5;

          

           A7: for y be object st y in ( dom ( Carrier A)) holds (g . y) in (( Carrier A) . y)

          proof

            let y be object;

            assume y in ( dom ( Carrier A));

            then

             A8: y in I by PARTFUN1:def 2;

            then y in ( dom g) by A5, PARTFUN1:def 2;

            then

             A9: (g . y) in (B . y) by A5, A6;

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

            then (B . y) c= (( Carrier A) . y) by A8;

            hence thesis by A9;

          end;

          ( dom g) = I by A5, PARTFUN1:def 2

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

          hence thesis by A4, A7, CARD_3:def 5;

        end;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let S1,S2 be Subset-Family of ( product ( Carrier A)) such that

         A10: for x be set holds x in S1 iff ex B be Segre-like ManySortedSubset of ( Carrier A) st x = ( product B) & ex i be Element of I st (B . i) is Block of (A . i) and

         A11: for x be set holds x in S2 iff ex B be Segre-like ManySortedSubset of ( Carrier A) st x = ( product B) & ex i be Element of I st (B . i) is Block of (A . i);

        for x be object holds x in S1 iff x in S2

        proof

          let x be object;

          x in S1 iff ex B be Segre-like ManySortedSubset of ( Carrier A) st x = ( product B) & ex i be Element of I st (B . i) is Block of (A . i) by A10;

          hence thesis by A11;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let I be non empty set;

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

      :: PENCIL_1:def23

      func Segre_Product A -> non empty TopStruct equals TopStruct (# ( product ( Carrier A)), ( Segre_Blocks A) #);

      correctness ;

    end

    theorem :: PENCIL_1:14

    

     Th14: for I be non empty set holds for A be non-Empty TopStruct-yielding ManySortedSet of I holds for x be Point of ( Segre_Product A) holds x is ManySortedSet of I

    proof

      let I be non empty set;

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

      let x be Point of ( Segre_Product A);

      ex f be Function st x = f & ( dom f) = ( dom ( Carrier A)) & for a be object st a in ( dom ( Carrier A)) holds (f . a) in (( Carrier A) . a) by CARD_3:def 5;

      hence thesis;

    end;

    theorem :: PENCIL_1:15

    

     Th15: for I be non empty set holds for A be non-Empty TopStruct-yielding ManySortedSet of I st ex i be Element of I st (A . i) is non void holds ( Segre_Product A) is non void

    proof

      let I be non empty set;

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

      set B = the trivial-yielding non-empty ManySortedSubset of ( Carrier A);

      given i be Element of I such that

       A1: (A . i) is non void;

      set l = the Block of (A . i);

      

       A2: the topology of (A . i) is non empty by A1;

      

       A3: (B +* (i,l)) c= ( Carrier A)

      proof

        let i1 be object;

        assume

         A4: i1 in I;

        then

         A5: i1 in ( dom B) by PARTFUN1:def 2;

        per cases ;

          suppose

           A6: i = i1;

          then ((B +* (i,l)) . i1) = l by A5, FUNCT_7: 31;

          then

           A7: ((B +* (i,l)) . i1) in the topology of (A . i) by A2;

          ex R be 1-sorted st R = (A . i1) & the carrier of R = (( Carrier A) . i1) by A4, PRALG_1:def 15;

          hence thesis by A6, A7;

        end;

          suppose

           A8: i1 <> i;

          

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

          ((B +* (i,l)) . i1) = (B . i1) by A8, FUNCT_7: 32;

          hence thesis by A4, A9;

        end;

      end;

      for j be Element of I st i <> j holds ((B +* (i,l)) . j) is 1 -element

      proof

        let j be Element of I;

        assume i <> j;

        then

         A10: ((B +* (i,l)) . j) = (B . j) by FUNCT_7: 32;

        j in I;

        then

         A11: j in ( dom B) by PARTFUN1:def 2;

        then ((B +* (i,l)) . j) in ( rng B) by A10, FUNCT_1:def 3;

        then ((B +* (i,l)) . j) is non empty trivial by A11, A10, Def16, FUNCT_1:def 9;

        hence thesis;

      end;

      then

      reconsider C = (B +* (i,l)) as Segre-like ManySortedSubset of ( Carrier A) by A3, Def20, PBOOLE:def 18;

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

      then (C . i) is Block of (A . i) by FUNCT_7: 31;

      then ( product C) in ( Segre_Blocks A) by Def22;

      hence thesis;

    end;

    theorem :: PENCIL_1:16

    

     Th16: for I be non empty set holds for A be non-Empty TopStruct-yielding ManySortedSet of I st for i be Element of I holds (A . i) is non degenerated & ex i be Element of I st (A . i) is non void holds ( Segre_Product A) is non degenerated

    proof

      let I be non empty set;

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

      assume

       A1: for i be Element of I holds (A . i) is non degenerated & ex i be Element of I st (A . i) is non void;

      then ( Segre_Product A) is non void by Th15;

      then

      reconsider SB = ( Segre_Blocks A) as non empty set;

      now

        assume ( product ( Carrier A)) in SB;

        then

        consider B be Segre-like ManySortedSubset of ( Carrier A) such that

         A2: ( product ( Carrier A)) = ( product B) and

         A3: ex i be Element of I st (B . i) is Block of (A . i) by Def22;

        consider i be Element of I such that

         A4: (B . i) is Block of (A . i) by A3;

        B is non-empty by A2, Th1;

        then (ex R be 1-sorted st R = (A . i) & the carrier of R = (( Carrier A) . i)) & (( Carrier A) . i) is Block of (A . i) by A2, A4, PRALG_1:def 15, PUA2MSS1: 2;

        then (A . i) is degenerated;

        hence contradiction by A1;

      end;

      then not ( product ( Carrier A)) is Element of SB;

      hence thesis;

    end;

    theorem :: PENCIL_1:17

    

     Th17: for I be non empty set holds for A be non-Empty TopStruct-yielding ManySortedSet of I st for i be Element of I holds (A . i) is with_non_trivial_blocks & ex i be Element of I st (A . i) is non void holds ( Segre_Product A) is with_non_trivial_blocks

    proof

      let I be non empty set;

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

      assume

       A1: for i be Element of I holds (A . i) is with_non_trivial_blocks & ex i be Element of I st (A . i) is non void;

      for k be Block of ( Segre_Product A) holds 2 c= ( card k)

      proof

        let k be Block of ( Segre_Product A);

        ( Segre_Product A) is non void by A1, Th15;

        then

        consider B be Segre-like ManySortedSubset of ( Carrier A) such that

         A2: k = ( product B) and

         A3: ex i be Element of I st (B . i) is Block of (A . i) by Def22;

        consider i be Element of I such that

         A4: (B . i) is Block of (A . i) by A3;

        (A . i) is with_non_trivial_blocks by A1;

        then 2 c= ( card (B . i)) by A4;

        then

         A5: (B . i) is non trivial by Th4;

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

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

        then

        reconsider BB = B as Segre-like non trivial-yielding ManySortedSet of I by A5, Def16;

        ( product BB) is non trivial;

        hence thesis by A2, Th4;

      end;

      hence thesis;

    end;

    theorem :: PENCIL_1:18

    

     Th18: for I be non empty set holds for A be non-Empty TopStruct-yielding ManySortedSet of I st for i be Element of I holds (A . i) is identifying_close_blocks with_non_trivial_blocks & ex i be Element of I st (A . i) is non void holds ( Segre_Product A) is identifying_close_blocks

    proof

      let I be non empty set;

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

      assume

       A1: for i be Element of I holds (A . i) is identifying_close_blocks with_non_trivial_blocks & ex i be Element of I st (A . i) is non void;

      for k,l be Block of ( Segre_Product A) st 2 c= ( card (k /\ l)) holds k = l

      proof

        let k,l be Block of ( Segre_Product A);

        assume 2 c= ( card (k /\ l));

        then

        consider a,b be object such that

         A2: a in (k /\ l) and

         A3: b in (k /\ l) and

         A4: a <> b by Th2;

        ( Segre_Product A) is non void by A1, Th15;

        then

        consider B be Segre-like ManySortedSubset of ( Carrier A) such that

         A5: k = ( product B) and

         A6: ex i be Element of I st (B . i) is Block of (A . i) by Def22;

        

         A7: b in ( product B) by A5, A3, XBOOLE_0:def 4;

        then

        reconsider b as Function by CARD_3: 48;

        

         A8: ( dom b) = ( dom B) by A7, CARD_3: 9

        .= I by PARTFUN1:def 2;

        then

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

        

         A9: a in ( product B) by A5, A2, XBOOLE_0:def 4;

        consider i be Element of I such that

         A10: (B . i) is Block of (A . i) by A6;

        

         A11: for j be Element of I st j <> i holds (B . j) is 1 -element

        proof

          let j be Element of I;

          assume

           A12: j <> i;

          consider i1 be Element of I such that

           A13: for j1 be Element of I st j1 <> i1 holds (B . j1) is 1 -element by Def20;

          (A . i) is with_non_trivial_blocks by A1;

          then 2 c= ( card (B . i)) by A10;

          then not (B . i) is 1 -element by Th4;

          then i1 = i by A13;

          hence thesis by A12, A13;

        end;

        ( Segre_Product A) is non void by A1, Th15;

        then

        consider C be Segre-like ManySortedSubset of ( Carrier A) such that

         A14: l = ( product C) and

         A15: ex i be Element of I st (C . i) is Block of (A . i) by Def22;

        

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

        consider j be Element of I such that

         A17: (C . j) is Block of (A . j) by A15;

        reconsider a as Function by A9, CARD_3: 48;

        

         A18: ( dom a) = ( dom B) by A9, CARD_3: 9

        .= I by PARTFUN1:def 2;

        then

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

        consider x be object such that

         A19: x in I and

         A20: (a . x) <> (b . x) by A4, A18, A8, FUNCT_1: 2;

        reconsider x as Element of I by A19;

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

        then

         A21: (b . x) in (B . x) by A7, CARD_3: 9;

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

        then

         A22: (a . x) in (B . x) by A9, CARD_3: 9;

        then 2 c= ( card (B . x)) by A20, A21, Th2;

        then not (B . x) is 1 -element by Th4;

        then

         A23: x = i by A11;

        b in ( product C) by A14, A3, XBOOLE_0:def 4;

        then

         A24: (b . x) in (C . x) by A16, CARD_3: 9;

        

         A25: a in ( product C) by A14, A2, XBOOLE_0:def 4;

        

         A26: for i be Element of I st j <> i holds (C . i) is 1 -element

        proof

          let i be Element of I;

          assume

           A27: j <> i;

          consider j1 be Element of I such that

           A28: for i1 be Element of I st j1 <> i1 holds (C . i1) is 1 -element by Def20;

          (A . j) is with_non_trivial_blocks by A1;

          then 2 c= ( card (C . j)) by A17;

          then not (C . j) is 1 -element by Th4;

          then j1 = j by A28;

          hence thesis by A27, A28;

        end;

        

         A29: ( dom B) = I by PARTFUN1:def 2

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

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

        then

         A30: (a . x) in (C . x) by A25, CARD_3: 9;

        then 2 c= ( card (C . x)) by A20, A24, Th2;

        then not (C . x) is 1 -element by Th4;

        then

         A31: x = j by A26;

        for s be object st s in ( dom B) holds (B . s) c= (C . s)

        proof

          let s be object;

          assume

           A32: s in ( dom B);

          then

          reconsider t = s as Element of I by PARTFUN1:def 2;

          per cases ;

            suppose

             A33: t = x;

            then

            reconsider Ct = (C . t) as Block of (A . t) by A17, A31;

            reconsider Bt = (B . t) as Block of (A . t) by A10, A23, A33;

            (a . t) in (Bt /\ Ct) & (b . t) in (Bt /\ Ct) by A22, A21, A30, A24, A33, XBOOLE_0:def 4;

            then

             A34: 2 c= ( card (Bt /\ Ct)) by A20, A33, Th2;

            (A . t) is identifying_close_blocks by A1;

            hence thesis by A34;

          end;

            suppose s <> x;

            then (B . t) is 1 -element by A11, A23;

            then

            consider y be object such that

             A35: (B . t) = {y} by ZFMISC_1: 131;

            

             A36: (a . t) in (C . t) by A25, A29, A32, CARD_3: 9;

            (a . t) in (B . t) by A9, A32, CARD_3: 9;

            then (a . t) = y by A35, TARSKI:def 1;

            hence thesis by A35, A36, ZFMISC_1: 31;

          end;

        end;

        hence k c= l by A5, A14, A29, CARD_3: 27;

        for s be object st s in ( dom C) holds (C . s) c= (B . s)

        proof

          let s be object;

          assume

           A37: s in ( dom C);

          then

          reconsider t = s as Element of I by PARTFUN1:def 2;

          per cases ;

            suppose

             A38: t = x;

            then

            reconsider Ct = (C . t) as Block of (A . t) by A17, A31;

            reconsider Bt = (B . t) as Block of (A . t) by A10, A23, A38;

            (a . t) in (Bt /\ Ct) & (b . t) in (Bt /\ Ct) by A22, A21, A30, A24, A38, XBOOLE_0:def 4;

            then

             A39: 2 c= ( card (Bt /\ Ct)) by A20, A38, Th2;

            (A . t) is identifying_close_blocks by A1;

            hence thesis by A39;

          end;

            suppose s <> x;

            then (C . t) is 1 -element by A26, A31;

            then

            consider y be object such that

             A40: (C . t) = {y} by ZFMISC_1: 131;

            

             A41: (a . t) in (B . t) by A9, A29, A37, CARD_3: 9;

            (a . t) in (C . t) by A25, A37, CARD_3: 9;

            then (a . t) = y by A40, TARSKI:def 1;

            hence thesis by A40, A41, ZFMISC_1: 31;

          end;

        end;

        hence thesis by A5, A14, A29, CARD_3: 27;

      end;

      hence thesis;

    end;

    registration

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      cluster ( Segre_Product A) -> non void non degenerated with_non_trivial_blocks identifying_close_blocks;

      coherence

      proof

        

         A1: (for j be Element of I holds (A . j) is with_non_trivial_blocks) & for j be Element of I holds (A . j) is identifying_close_blocks;

        (A . the Element of I) is non void & for j be Element of I holds (A . j) is non degenerated;

        hence thesis by A1, Th15, Th16, Th17, Th18;

      end;

    end

    theorem :: PENCIL_1:19

    for T be TopStruct holds for S be Subset of T holds S is trivial implies S is strong closed_under_lines

    proof

      let T be TopStruct;

      let S be Subset of T;

      assume

       A1: S is trivial;

      thus S is strong

      proof

        let x,y be Point of T;

        assume

         A2: x in S & y in S;

        thus (x,y) are_collinear

        proof

          per cases ;

            suppose x = y;

            hence thesis;

          end;

            suppose x <> y;

            then 2 c= ( card S) by A2, Th2;

            hence thesis by A1, Th4;

          end;

        end;

      end;

      thus S is closed_under_lines

      proof

        let l be Block of T;

        

         A3: ( card (l /\ S)) c= ( card S) by CARD_1: 11, XBOOLE_1: 17;

        assume 2 c= ( card (l /\ S));

        then 2 c= ( card S) by A3;

        hence thesis by A1, Th4;

      end;

    end;

    theorem :: PENCIL_1:20

    

     Th20: for S be identifying_close_blocks TopStruct, l be Block of S holds for L be Subset of S st L = l holds L is closed_under_lines by Def7;

    theorem :: PENCIL_1:21

    

     Th21: for S be TopStruct, l be Block of S holds for L be Subset of S st L = l holds L is strong

    proof

      let S be TopStruct;

      let l be Block of S;

      let L be Subset of S;

      assume

       A1: L = l;

      thus L is strong

      proof

        let x,y be Point of S;

        assume x in L & y in L;

        then {x, y} c= l by A1, ZFMISC_1: 32;

        hence thesis;

      end;

    end;

    theorem :: PENCIL_1:22

    for S be non void TopStruct holds ( [#] S) is closed_under_lines

    proof

      let S be non void TopStruct;

      thus ( [#] S) is closed_under_lines

      proof

        let K be Block of S;

        assume 2 c= ( card (K /\ ( [#] S)));

        K in the topology of S;

        hence thesis;

      end;

    end;

    theorem :: PENCIL_1:23

    

     Th23: for I be non empty set holds for A be Segre-like non trivial-yielding ManySortedSet of I holds for x,y be ManySortedSet of I st x in ( product A) & y in ( product A) holds for i be object st i <> ( indx A) holds (x . i) = (y . i)

    proof

      let I be non empty set;

      let A be Segre-like non trivial-yielding ManySortedSet of I;

      let x,y be ManySortedSet of I such that

       A1: x in ( product A) and

       A2: y in ( product A);

      let i be object;

      

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

      assume

       A4: i <> ( indx A);

      per cases ;

        suppose

         A5: not i in I;

        then

         A6: not i in ( dom y) by PARTFUN1:def 2;

         not i in ( dom x) by A5, PARTFUN1:def 2;

        

        hence (x . i) = {} by FUNCT_1:def 2

        .= (y . i) by A6, FUNCT_1:def 2;

      end;

        suppose i in I;

        then

        reconsider ii = i as Element of I;

        consider j be Element of I such that

         A7: for k be Element of I st k <> j holds (A . k) is 1 -element by Def20;

        now

          assume j <> ( indx A);

          then (A . ( indx A)) is 1 -element by A7;

          hence contradiction by Def21;

        end;

        then (A . ii) is 1 -element by A4, A7;

        then

        consider o be object such that

         A8: (A . i) = {o} by ZFMISC_1: 131;

        

         A9: (x . ii) in (A . ii) by A1, A3, CARD_3: 9;

        (y . ii) in (A . ii) by A2, A3, CARD_3: 9;

        

        hence (y . i) = o by A8, TARSKI:def 1

        .= (x . i) by A8, A9, TARSKI:def 1;

      end;

    end;

    theorem :: PENCIL_1:24

    

     Th24: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for x be set holds x is Block of ( Segre_Product A) iff ex L be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st x = ( product L) & (L . ( indx L)) is Block of (A . ( indx L))

    proof

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let x be set;

      thus x is Block of ( Segre_Product A) implies ex L be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st x = ( product L) & (L . ( indx L)) is Block of (A . ( indx L))

      proof

        assume

         A1: x is Block of ( Segre_Product A);

        then

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

         A2: x = ( product L) and

         A3: ex i be Element of I st (L . i) is Block of (A . i) by Def22;

        2 c= ( card ( product L)) by A1, A2, Def6;

        then

        reconsider L as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by Th13;

        consider i be Element of I such that

         A4: (L . i) is Block of (A . i) by A3;

        now

          assume i <> ( indx L);

          then

           A5: (L . i) is 1 -element by Th12;

          2 c= ( card (L . i)) by A4, Def6;

          hence contradiction by A5, Th4;

        end;

        hence thesis by A2, A4;

      end;

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

       A6: x = ( product L) & (L . ( indx L)) is Block of (A . ( indx L));

      thus thesis by A6, Def22;

    end;

    theorem :: PENCIL_1:25

    

     Th25: for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for P be ManySortedSet of I st P is Point of ( Segre_Product A) holds for i be Element of I holds for p be Point of (A . i) holds (P +* (i,p)) is Point of ( Segre_Product A)

    proof

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let P be ManySortedSet of I such that

       A1: P is Point of ( Segre_Product A);

      let j be Element of I;

      let p be Point of (A . j);

      

       A2: for i be object st i in ( dom ( Carrier A)) holds ((P +* (j,p)) . i) in (( Carrier A) . i)

      proof

        let i be object;

        assume

         A3: i in ( dom ( Carrier A));

        then i in I by PARTFUN1:def 2;

        then

         A4: i in ( dom P) by PARTFUN1:def 2;

        per cases ;

          suppose i <> j;

          then ((P +* (j,p)) . i) = (P . i) by FUNCT_7: 32;

          hence thesis by A1, A3, CARD_3: 9;

        end;

          suppose

           A5: i = j;

          

           A6: p in the carrier of (A . j);

          ((P +* (j,p)) . i) = p by A4, A5, FUNCT_7: 31;

          hence thesis by A5, A6, YELLOW_6: 2;

        end;

      end;

      ( dom (P +* (j,p))) = I by PARTFUN1:def 2

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

      hence thesis by A2, CARD_3: 9;

    end;

    theorem :: PENCIL_1:26

    

     Th26: for I be non empty set holds for A,B be Segre-like non trivial-yielding ManySortedSet of I st 2 c= ( card (( product A) /\ ( product B))) holds ( indx A) = ( indx B) & for i be object st i <> ( indx A) holds (A . i) = (B . i)

    proof

      let I be non empty set;

      let A,B be Segre-like non trivial-yielding ManySortedSet of I;

      

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

      assume 2 c= ( card (( product A) /\ ( product B)));

      then

      consider a,b be object such that

       A2: a in (( product A) /\ ( product B)) and

       A3: b in (( product A) /\ ( product B)) and

       A4: a <> b by Th2;

      b in ( product A) by A3, XBOOLE_0:def 4;

      then

      consider b1 be Function such that

       A5: b1 = b and

       A6: ( dom b1) = ( dom A) and

       A7: for o be object st o in ( dom A) holds (b1 . o) in (A . o) by CARD_3:def 5;

      a in ( product A) by A2, XBOOLE_0:def 4;

      then

      consider a1 be Function such that

       A8: a1 = a and

       A9: ( dom a1) = ( dom A) and

       A10: for o be object st o in ( dom A) holds (a1 . o) in (A . o) by CARD_3:def 5;

      consider o be object such that

       A11: o in ( dom A) and

       A12: (a1 . o) <> (b1 . o) by A4, A8, A9, A5, A6, FUNCT_1: 2;

      reconsider o as Element of I by A11, PARTFUN1:def 2;

      b in ( product B) by A3, XBOOLE_0:def 4;

      then

       A13: (b1 . o) in (B . o) by A5, A1, CARD_3: 9;

      

       A14: a in ( product B) by A2, XBOOLE_0:def 4;

      then (a1 . o) in (B . o) by A8, A1, CARD_3: 9;

      then 2 c= ( card (B . o)) by A12, A13, Th2;

      then

       A15: (B . o) is non trivial by Th4;

      then

       A16: o = ( indx B) by Def21;

      

       A17: (b1 . o) in (A . o) by A7, A11;

      (a1 . o) in (A . o) by A10, A11;

      then 2 c= ( card (A . o)) by A12, A17, Th2;

      then (A . o) is non trivial by Th4;

      then

       A18: o = ( indx A) by Def21;

      hence ( indx A) = ( indx B) by A15, Def21;

      let i be object;

      assume

       A19: i <> ( indx A);

      per cases ;

        suppose

         A20: i in I;

        then (B . i) is 1 -element by A18, A16, A19, Th12;

        then

         A21: ex y be object st (B . i) = {y} by ZFMISC_1: 131;

        (A . i) is 1 -element by A19, A20, Th12;

        then

        consider x be object such that

         A22: (A . i) = {x} by ZFMISC_1: 131;

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

        then

         A23: (a1 . i) in (B . i) by A8, A14, A20, CARD_3: 9;

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

        then (a1 . i) in (A . i) by A10, A20;

        then (a1 . i) = x by A22, TARSKI:def 1;

        hence thesis by A22, A21, A23, TARSKI:def 1;

      end;

        suppose

         A24: not i in I;

        then

         A25: not i in ( dom B) by PARTFUN1:def 2;

         not i in ( dom A) by A24, PARTFUN1:def 2;

        

        hence (A . i) = {} by FUNCT_1:def 2

        .= (B . i) by A25, FUNCT_1:def 2;

      end;

    end;

    theorem :: PENCIL_1:27

    

     Th27: for I be non empty set holds for A be Segre-like non trivial-yielding ManySortedSet of I holds for N be non trivial set holds (A +* (( indx A),N)) is Segre-like non trivial-yielding

    proof

      let I be non empty set;

      let A be Segre-like non trivial-yielding ManySortedSet of I;

      let N be non trivial set;

      thus (A +* (( indx A),N)) is Segre-like

      proof

        take ( indx A);

        let i be Element of I;

        assume

         A1: i <> ( indx A);

        then ((A +* (( indx A),N)) . i) = (A . i) by FUNCT_7: 32;

        hence thesis by A1, Th12;

      end;

      thus (A +* (( indx A),N)) is non trivial-yielding

      proof

        take ((A +* (( indx A),N)) . ( indx A));

        ( dom (A +* (( indx A),N))) = I by PARTFUN1:def 2;

        hence ((A +* (( indx A),N)) . ( indx A)) in ( rng (A +* (( indx A),N))) by FUNCT_1:def 3;

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

        hence thesis by FUNCT_7: 31;

      end;

    end;

    theorem :: PENCIL_1:28

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

    proof

      let S be non empty non void identifying_close_blocks without_isolated_points TopStruct;

      assume

       A1: S is strongly_connected;

      thus S is connected

      proof

        let x,y be Point of S;

        

         A2: ( len <*x*>) = 1 by FINSEQ_1: 39;

        

         A3: ( len <*y*>) = 1 by FINSEQ_1: 39;

        consider K be Block of S such that

         A4: x in K by Def9;

        K in the topology of S;

        then

        reconsider L = K as Subset of S;

        L is closed_under_lines strong by Th20, Th21;

        then

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

         A5: L = (f . 1) and

         A6: y in (f . ( len f)) and

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

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

        

         A9: ( len f) in ( dom f) by A6, FUNCT_1:def 2;

        

         A10: 1 in ( dom f) by A4, A5, FUNCT_1:def 2;

        then

        reconsider n = (( len f) - 1) as Nat by FINSEQ_3: 26;

        deffunc F( Nat) = ((f . $1) /\ (f . ($1 + 1)));

        reconsider n as Element of NAT by ORDINAL1:def 12;

        consider h be FinSequence such that

         A11: ( len h) = n & for k be Nat st k in ( dom h) holds (h . k) = F(k) from FINSEQ_1:sch 2;

        

         A12: ( dom h) = ( Seg n) by A11, FINSEQ_1:def 3;

        

         A13: (( len h) + 1) = ( len f) by A11;

        now

          assume {} in ( rng h);

          then

          consider i be object such that

           A14: i in ( dom h) and

           A15: (h . i) = {} by FUNCT_1:def 3;

          reconsider i as Element of NAT by A14;

          

           A16: i <= ( len h) by A14, FINSEQ_3: 25;

          then

           A17: i < ( len f) by A13, NAT_1: 13;

          

           A18: 1 <= i by A14, FINSEQ_3: 25;

          then i in ( Seg n) by A11, A16, FINSEQ_1: 1;

          then (h . i) = ((f . i) /\ (f . (i + 1))) by A11, A12;

          then 2 c= ( card (h . i)) by A8, A18, A17;

          hence contradiction by A15;

        end;

        then ( product h) <> {} by CARD_3: 26;

        then

        consider c be object such that

         A19: c in ( product h) by XBOOLE_0:def 1;

        

         A20: ex ce be Function st ce = c & ( dom ce) = ( dom h) & for a be object st a in ( dom h) holds (ce . a) in (h . a) by A19, CARD_3:def 5;

        then

        reconsider c as Function;

        

         A21: ( dom h) = ( Seg n) by A11, FINSEQ_1:def 3;

        then

        reconsider c as FinSequence by A20, FINSEQ_1:def 2;

        

         A22: ( rng f) c= ( bool the carrier of S) by FINSEQ_1:def 4;

        ( rng (( <*x*> ^ c) ^ <*y*>)) c= the carrier of S

        proof

          let r be object;

          assume r in ( rng (( <*x*> ^ c) ^ <*y*>));

          then r in (( rng ( <*x*> ^ c)) \/ ( rng <*y*>)) by FINSEQ_1: 31;

          then r in ( rng ( <*x*> ^ c)) or r in ( rng <*y*>) by XBOOLE_0:def 3;

          then

           A23: r in (( rng <*x*>) \/ ( rng c)) or r in ( rng <*y*>) by FINSEQ_1: 31;

          per cases by A23, XBOOLE_0:def 3;

            suppose r in ( rng <*x*>);

            then r in {x} by FINSEQ_1: 38;

            hence thesis;

          end;

            suppose r in ( rng c);

            then

            consider o be object such that

             A24: o in ( dom c) and

             A25: r = (c . o) by FUNCT_1:def 3;

            reconsider o as Element of NAT by A24;

            (h . o) = ((f . o) /\ (f . (o + 1))) by A11, A20, A24;

            then r in ((f . o) /\ (f . (o + 1))) by A20, A24, A25;

            then

             A26: r in (f . o) by XBOOLE_0:def 4;

            ( len h) <= ( len f) by A13, NAT_1: 11;

            then ( dom h) c= ( dom f) by FINSEQ_3: 30;

            then (f . o) in ( rng f) by A20, A24, FUNCT_1:def 3;

            hence thesis by A22, A26;

          end;

            suppose r in ( rng <*y*>);

            then r in {y} by FINSEQ_1: 38;

            hence thesis;

          end;

        end;

        then

        reconsider g = (( <*x*> ^ c) ^ <*y*>) as FinSequence of the carrier of S by FINSEQ_1:def 4;

        

         A27: ( len ( <*x*> ^ c)) = (( len <*x*>) + ( len c)) by FINSEQ_1: 22;

        then

         A28: ( len ( <*x*> ^ c)) = (( len c) + 1) by FINSEQ_1: 39;

        take g;

        

         A29: g = ( <*x*> ^ (c ^ <*y*>)) by FINSEQ_1: 32;

        hence x = (g . 1) by FINSEQ_1: 41;

        ( len g) = (( len ( <*x*> ^ c)) + ( len <*y*>)) by FINSEQ_1: 22;

        then

         A30: (( len ( <*x*> ^ c)) + 1) = ( len g) by FINSEQ_1: 39;

        hence

         A31: y = (g . ( len g)) by FINSEQ_1: 42;

        let i be Nat;

        assume that

         A32: 1 <= i and

         A33: i < ( len g);

        

         A34: i <= ( len ( <*x*> ^ c)) by A30, A33, NAT_1: 13;

        let a,b be Point of S;

        assume that

         A35: a = (g . i) and

         A36: b = (g . (i + 1));

        reconsider i as Element of NAT by ORDINAL1:def 12;

        per cases by A28, A32, A34, NAT_1: 8, XXREAL_0: 1;

          suppose

           A37: i = 1 & i <= ( len c);

          ( len (c ^ <*y*>)) = (( len c) + 1) & ( len ( <*x*> ^ (c ^ <*y*>))) = (( len <*x*>) + ( len (c ^ <*y*>))) by A3, FINSEQ_1: 22;

          then

           A38: ( len ( <*x*> ^ (c ^ <*y*>))) = ((1 + 1) + ( len c)) by A2;

          

           A39: 1 in ( dom c) by A37, FINSEQ_3: 25;

          b = (( <*x*> ^ (c ^ <*y*>)) . 2) by A36, A37, FINSEQ_1: 32;

          then b = ((c ^ <*y*>) . (2 - ( len <*x*>))) by A2, A38, FINSEQ_1: 24, NAT_1: 11;

          then b = ((c ^ <*y*>) . (2 - 1)) by FINSEQ_1: 39;

          then

           A40: b = (c . 1) by A39, FINSEQ_1:def 7;

          (c . 1) in (h . 1) & (h . 1) = ((f . 1) /\ (f . (1 + 1))) by A11, A20, A39;

          then

           A41: b in (f . 1) by A40, XBOOLE_0:def 4;

          

           A42: (f . 1) in ( rng f) by A10, FUNCT_1:def 3;

          then

          reconsider f1 = (f . 1) as Subset of S by A22;

          

           A43: f1 is closed_under_lines strong by A7, A42;

          a = x by A29, A35, A37, FINSEQ_1: 41;

          hence thesis by A4, A5, A41, A43;

        end;

          suppose

           A44: i = 1 & i = (( len c) + 1);

          

           A45: (f . 1) in ( rng f) by A10, FUNCT_1:def 3;

          then

          reconsider f1 = (f . 1) as Subset of S by A22;

          

           A46: f1 is closed_under_lines strong by A7, A45;

          ( len <*x*>) = 1 by FINSEQ_1: 39;

          then

           A47: ( len g) = (i + 1) by A30, A44, FINSEQ_1: 22;

          ( len h) = 0 by A20, A44, FINSEQ_3: 29;

          then (x,y) are_collinear by A4, A5, A6, A11, A46;

          hence thesis by A29, A31, A35, A36, A44, A47, FINSEQ_1: 41;

        end;

          suppose

           A48: 1 < i & i <= ( len c);

          

           A49: ( len h) <= (( len h) + 1) & ( len c) = ( len h) by A20, FINSEQ_3: 29, NAT_1: 11;

          then i <= (( len h) + 1) by A48, XXREAL_0: 2;

          then

           A50: i in ( dom f) by A11, A48, FINSEQ_3: 25;

          then

          reconsider j = (i - 1) as Nat by FINSEQ_3: 26;

          i <= (( len c) + 1) by A48, A49, XXREAL_0: 2;

          then i in ( dom ( <*x*> ^ c)) by A28, A48, FINSEQ_3: 25;

          then

           A51: a = (( <*x*> ^ c) . i) by A35, FINSEQ_1:def 7;

          i <= ( len ( <*x*> ^ c)) by A27, A2, A48, NAT_1: 13;

          then

           A52: a = (c . j) by A2, A48, A51, FINSEQ_1: 24;

          (j + 1) = i;

          then

           A53: 1 <= j by A48, NAT_1: 13;

          

           A54: (f . i) in ( rng f) by A50, FUNCT_1:def 3;

          then

          reconsider ff = (f . i) as Subset of S by A22;

          

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

          

           A56: ( len <*x*>) < (i + 1) & (i + 1) <= (( len c) + 1) by A2, A48, NAT_1: 13, XREAL_1: 6;

          then (i + 1) in ( dom ( <*x*> ^ c)) by A27, A2, FINSEQ_3: 25;

          then b = (( <*x*> ^ c) . (i + 1)) by A36, FINSEQ_1:def 7;

          then

           A57: b = (c . ((i + 1) - ( len <*x*>))) by A28, A56, FINSEQ_1: 24;

          i <= ( len h) by A20, A48, FINSEQ_3: 29;

          then

           A58: i in ( Seg n) by A11, A48, FINSEQ_1: 1;

          then (c . i) in (h . i) by A20, A21;

          then b in ((f . i) /\ (f . (i + 1))) by A11, A12, A2, A58, A57;

          then

           A59: b in ff by XBOOLE_0:def 4;

          i <= ( len h) by A20, A48, FINSEQ_3: 29;

          then j <= n by A11, A55, XXREAL_0: 2;

          then

           A60: j in ( Seg n) by A53, FINSEQ_1: 1;

          then (c . j) in (h . j) by A20, A21;

          then a in ((f . j) /\ (f . (j + 1))) by A11, A12, A60, A52;

          then

           A61: a in ff by XBOOLE_0:def 4;

          ff is closed_under_lines strong by A7, A54;

          hence thesis by A61, A59;

        end;

          suppose

           A62: 1 < i & i = (( len c) + 1);

          then ( 0 + 1) < (( len c) + 1);

          then ex k be Nat st ( len c) = (k + 1) by NAT_1: 6;

          then 1 <= ( len c) by NAT_1: 11;

          then

           A63: ( len c) in ( dom h) by A20, FINSEQ_3: 25;

          

           A64: ( len ( <*x*> ^ c)) = (1 + ( len c)) by A2, FINSEQ_1: 22;

          then i in ( dom ( <*x*> ^ c)) by A62, FINSEQ_3: 25;

          

          then a = (( <*x*> ^ c) . i) by A35, FINSEQ_1:def 7

          .= (c . ((( len c) + 1) - 1)) by A2, A62, A64, FINSEQ_1: 24

          .= (c . ( len c));

          then a in (h . ( len c)) by A20, A63;

          then

           A65: a in ((f . ( len c)) /\ (f . (( len c) + 1))) by A11, A63;

          

           A66: (f . ( len f)) in ( rng f) by A9, FUNCT_1:def 3;

          then

          reconsider ff = (f . ( len f)) as Subset of S by A22;

          

           A67: ff is closed_under_lines strong by A7, A66;

          ( len c) = ( len h) by A20, FINSEQ_3: 29;

          then

           A68: a in ff by A11, A65, XBOOLE_0:def 4;

          b = y by A36, A62, A64, FINSEQ_1: 42;

          hence thesis by A6, A67, A68;

        end;

      end;

    end;

    theorem :: PENCIL_1:29

    for I be non empty set holds for A be PLS-yielding ManySortedSet of I holds for S be Subset of ( Segre_Product A) holds S is non trivial strong closed_under_lines iff ex B be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st S = ( product B) & for C be Subset of (A . ( indx B)) st C = (B . ( indx B)) holds C is strong closed_under_lines

    proof

      let I be non empty set;

      let A be PLS-yielding ManySortedSet of I;

      let S be Subset of ( Segre_Product A);

      thus S is non trivial strong closed_under_lines implies ex B be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) st S = ( product B) & for C be Subset of (A . ( indx B)) st C = (B . ( indx B)) holds C is strong closed_under_lines

      proof

        assume

         A1: S is non trivial strong closed_under_lines;

        then 2 c= ( card S) by Th4;

        then

        consider a,b be object such that

         A2: a in S and

         A3: b in S and

         A4: a <> b by Th2;

        reconsider a, b as Point of ( Segre_Product A) by A2, A3;

        (a,b) are_collinear by A1, A2, A3;

        then

        consider C be Block of ( Segre_Product A) such that

         A5: {a, b} c= C by A4;

        consider CC be Segre-like ManySortedSubset of ( Carrier A) such that

         A6: C = ( product CC) and ex i be Element of I st (CC . i) is Block of (A . i) by Def22;

        a in ( product CC) & b in ( product CC) by A5, A6, ZFMISC_1: 32;

        then 2 c= ( card ( product CC)) by A4, Th2;

        then

        reconsider CC as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by Th13;

        

         A7: ( dom CC) = I by PARTFUN1:def 2;

        reconsider a1 = a, b1 = b as ManySortedSet of I by Th14;

        

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

        

         A9: ( dom b1) = I by PARTFUN1:def 2;

         A10:

        now

          assume

           A11: (a1 . ( indx CC)) = (b1 . ( indx CC));

          for i be object st i in I holds (a1 . i) = (b1 . i)

          proof

            let i be object;

            assume i in I;

            per cases ;

              suppose i = ( indx CC);

              hence thesis by A11;

            end;

              suppose

               A12: i <> ( indx CC);

              a1 in ( product CC) & b1 in ( product CC) by A5, A6, ZFMISC_1: 32;

              hence thesis by A12, Th23;

            end;

          end;

          hence contradiction by A4, A8, A9, FUNCT_1: 2;

        end;

        

         A13: for f be ManySortedSet of I st f in S holds for i be Element of I st i <> ( indx CC) holds (f . i) in (CC . i)

        proof

          let f be ManySortedSet of I;

          assume

           A14: f in S;

          then

          reconsider f1 = f as Point of ( Segre_Product A);

          let i be Element of I;

          assume

           A15: i <> ( indx CC);

          now

            b1 in ( product CC) by A5, A6, ZFMISC_1: 32;

            then

             A16: (b1 . i) in (CC . i) by A7, CARD_3: 9;

            assume

             A17: not (f . i) in (CC . i);

            (f1,b) are_collinear by A1, A3, A14;

            then

            consider lb be Block of ( Segre_Product A) such that

             A18: {f1, b} c= lb by A17, A16;

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

             A19: lb = ( product Lb) and (Lb . ( indx Lb)) is Block of (A . ( indx Lb)) by Th24;

            

             A20: b1 in ( product Lb) by A18, A19, ZFMISC_1: 32;

            

             A21: f in ( product Lb) by A18, A19, ZFMISC_1: 32;

            then ( indx Lb) = i by A17, A16, A20, Th23;

            then (Lb . ( indx CC)) is 1 -element by A15, Th12;

            then

            consider cb be object such that

             A22: (Lb . ( indx CC)) = {cb} by ZFMISC_1: 131;

            

             A23: ( dom Lb) = I by PARTFUN1:def 2;

            then (b1 . ( indx CC)) in {cb} by A20, A22, CARD_3: 9;

            then

             A24: (b1 . ( indx CC)) = cb by TARSKI:def 1;

            a1 in ( product CC) by A5, A6, ZFMISC_1: 32;

            then

             A25: (a1 . i) in (CC . i) by A7, CARD_3: 9;

            (f1,a) are_collinear by A1, A2, A14;

            then

            consider la be Block of ( Segre_Product A) such that

             A26: {f1, a} c= la by A17, A25;

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

             A27: la = ( product La) and (La . ( indx La)) is Block of (A . ( indx La)) by Th24;

            

             A28: a1 in ( product La) by A26, A27, ZFMISC_1: 32;

            

             A29: f in ( product La) by A26, A27, ZFMISC_1: 32;

            then ( indx La) = i by A17, A25, A28, Th23;

            then (La . ( indx CC)) is 1 -element by A15, Th12;

            then

            consider ca be object such that

             A30: (La . ( indx CC)) = {ca} by ZFMISC_1: 131;

            

             A31: ( dom La) = I by PARTFUN1:def 2;

            then (a1 . ( indx CC)) in {ca} by A28, A30, CARD_3: 9;

            then

             A32: ca <> cb by A10, A24, TARSKI:def 1;

            (f . ( indx CC)) in {ca} by A29, A30, A31, CARD_3: 9;

            then

             A33: (f . ( indx CC)) <> cb by A32, TARSKI:def 1;

            (f . ( indx CC)) in {cb} by A21, A22, A23, CARD_3: 9;

            hence contradiction by A33, TARSKI:def 1;

          end;

          hence thesis;

        end;

        (a1 . ( indx CC)) in ( pi (S,( indx CC))) & (b1 . ( indx CC)) in ( pi (S,( indx CC))) by A2, A3, CARD_3:def 6;

        then 2 c= ( card ( pi (S,( indx CC)))) by A10, Th2;

        then

        reconsider p = ( pi (S,( indx CC))) as non trivial set by Th4;

        (CC +* (( indx CC),p)) c= ( Carrier A)

        proof

          let i be object;

          assume

           A34: i in I;

          per cases ;

            suppose

             A35: i <> ( indx CC);

            

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

            ((CC +* (( indx CC),p)) . i) = (CC . i) by A35, FUNCT_7: 32;

            hence thesis by A34, A36;

          end;

            suppose

             A37: i = ( indx CC);

            

             A38: p c= (( Carrier A) . i)

            proof

              let y be object;

              assume y in p;

              then

               A39: ex f be Function st f in S & y = (f . i) by A37, CARD_3:def 6;

              i in ( dom ( Carrier A)) by A34, PARTFUN1:def 2;

              hence thesis by A39, CARD_3: 9;

            end;

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

            hence thesis by A37, A38, FUNCT_7: 31;

          end;

        end;

        then

        reconsider B = (CC +* (( indx CC),p)) as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by Th27, PBOOLE:def 18;

        take B;

        

         A40: ( dom B) = I by PARTFUN1:def 2;

        

         A41: (B . ( indx CC)) = p by A7, FUNCT_7: 31;

        thus

         A42: S = ( product B)

        proof

          thus S c= ( product B)

          proof

            let e be object;

            assume

             A43: e in S;

            then

            reconsider f = e as ManySortedSet of I by Th14;

             A44:

            now

              let i be object;

              assume i in I;

              then

              reconsider j = i as Element of I;

              per cases ;

                suppose j = ( indx CC);

                hence (f . i) in (B . i) by A41, A43, CARD_3:def 6;

              end;

                suppose

                 A45: j <> ( indx CC);

                then (f . j) in (CC . j) by A13, A43;

                hence (f . i) in (B . i) by A45, FUNCT_7: 32;

              end;

            end;

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

            hence thesis by A40, A44, CARD_3: 9;

          end;

          let e be object;

          assume e in ( product B);

          then

          consider f be Function such that

           A46: e = f & ( dom f) = I and

           A47: for i be object st i in I holds (f . i) in (B . i) by A40, CARD_3:def 5;

          (f . ( indx CC)) in p by A41, A47;

          then

          consider g be Function such that

           A48: g in S and

           A49: (f . ( indx CC)) = (g . ( indx CC)) by CARD_3:def 6;

          reconsider g as ManySortedSet of I by A48;

           A50:

          now

            let i be object;

            assume i in I;

            then

            reconsider j = i as Element of I;

            per cases ;

              suppose i = ( indx CC);

              hence (f . i) = (g . i) by A49;

            end;

              suppose

               A51: i <> ( indx CC);

              then (CC . j) is 1 -element by Th12;

              then

              consider c be object such that

               A52: (CC . i) = {c} by ZFMISC_1: 131;

              

               A53: (g . j) in (CC . j) by A13, A48, A51;

              (f . j) in (B . j) by A47;

              then (f . j) in {c} by A51, A52, FUNCT_7: 32;

              

              hence (f . i) = c by TARSKI:def 1

              .= (g . i) by A52, A53, TARSKI:def 1;

            end;

          end;

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

          hence thesis by A46, A48, A50, FUNCT_1: 2;

        end;

        let SS be Subset of (A . ( indx B));

        assume

         A54: SS = (B . ( indx B));

        thus SS is strong

        proof

          let q,r be Point of (A . ( indx B));

          assume that

           A55: q in SS and

           A56: r in SS;

          thus (q,r) are_collinear

          proof

            per cases ;

              suppose q = r;

              hence thesis;

            end;

              suppose

               A57: q <> r;

              reconsider R = (a1 +* (( indx B),r)) as Point of ( Segre_Product A) by Th25;

              reconsider Q = (a1 +* (( indx B),q)) as Point of ( Segre_Product A) by Th25;

              reconsider Q1 = Q, R1 = R as ManySortedSet of I;

               A58:

              now

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

                then

                 A59: (Q1 . ( indx B)) = q by FUNCT_7: 31;

                

                 A60: ( dom a1) = I by PARTFUN1:def 2;

                assume Q = R;

                hence contradiction by A57, A59, A60, FUNCT_7: 31;

              end;

              

               A61: for i be object st i in ( dom B) holds (Q1 . i) in (B . i)

              proof

                let i be object;

                assume

                 A62: i in ( dom B);

                then i in I by PARTFUN1:def 2;

                then

                 A63: i in ( dom a1) by PARTFUN1:def 2;

                per cases ;

                  suppose i <> ( indx B);

                  then (Q1 . i) = (a1 . i) by FUNCT_7: 32;

                  hence thesis by A2, A42, A62, CARD_3: 9;

                end;

                  suppose i = ( indx B);

                  hence thesis by A54, A55, A63, FUNCT_7: 31;

                end;

              end;

              

               A64: for i be object st i in ( dom B) holds (R1 . i) in (B . i)

              proof

                let i be object;

                assume

                 A65: i in ( dom B);

                then i in I by PARTFUN1:def 2;

                then

                 A66: i in ( dom a1) by PARTFUN1:def 2;

                per cases ;

                  suppose i <> ( indx B);

                  then (R1 . i) = (a1 . i) by FUNCT_7: 32;

                  hence thesis by A2, A42, A65, CARD_3: 9;

                end;

                  suppose i = ( indx B);

                  hence thesis by A54, A56, A66, FUNCT_7: 31;

                end;

              end;

              ( dom R1) = I by PARTFUN1:def 2

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

              then

               A67: R in ( product B) by A64, CARD_3: 9;

              ( dom Q1) = I by PARTFUN1:def 2

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

              then Q in ( product B) by A61, CARD_3: 9;

              then (Q,R) are_collinear by A1, A42, A67;

              then

              consider L be Block of ( Segre_Product A) such that

               A68: {Q, R} c= L by A58;

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

              then

               A69: (R1 . ( indx B)) = r by FUNCT_7: 31;

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

               A70: L = ( product L1) and

               A71: (L1 . ( indx L1)) is Block of (A . ( indx L1)) by Th24;

              

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

              Q1 in ( product L1) by A68, A70, ZFMISC_1: 32;

              then

               A73: (Q1 . ( indx B)) in (L1 . ( indx B)) by A72, CARD_3: 9;

              

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

              R1 in ( product L1) by A68, A70, ZFMISC_1: 32;

              then

               A75: (R1 . ( indx B)) in (L1 . ( indx B)) by A74, CARD_3: 9;

              now

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

                then

                 A76: (Q1 . ( indx B)) = q by FUNCT_7: 31;

                

                 A77: ( dom a1) = I by PARTFUN1:def 2;

                assume (Q1 . ( indx B)) = (R1 . ( indx B));

                hence contradiction by A57, A76, A77, FUNCT_7: 31;

              end;

              then 2 c= ( card (L1 . ( indx B))) by A73, A75, Th2;

              then

               A78: (L1 . ( indx B)) is non trivial by Th4;

              then

              reconsider LI = (L1 . ( indx L1)) as Block of (A . ( indx B)) by A71, Def21;

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

              then

               A79: (Q1 . ( indx B)) = q by FUNCT_7: 31;

              ( indx B) = ( indx L1) by A78, Def21;

              then {q, r} c= LI by A73, A75, A79, A69, ZFMISC_1: 32;

              hence thesis;

            end;

          end;

        end;

        thus SS is closed_under_lines

        proof

          let L be Block of (A . ( indx B));

          

           A80: ( dom B) = I by PARTFUN1:def 2;

          2 c= ( card L) by Def6;

          then

          reconsider L1 = L as non trivial set by Th4;

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

          then

           A81: L c= the carrier of (A . ( indx B));

          (B +* (( indx B),L1)) c= ( Carrier A)

          proof

            let o be object;

            assume

             A82: o in I;

            thus ((B +* (( indx B),L1)) . o) c= (( Carrier A) . o)

            proof

              per cases ;

                suppose

                 A83: o <> ( indx B);

                

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

                ((B +* (( indx B),L1)) . o) = (B . o) by A83, FUNCT_7: 32;

                hence thesis by A82, A84;

              end;

                suppose

                 A85: o = ( indx B);

                then ((B +* (( indx B),L1)) . o) = L by A40, FUNCT_7: 31;

                hence thesis by A81, A85, YELLOW_6: 2;

              end;

            end;

          end;

          then

          reconsider L2 = (B +* (( indx B),L1)) as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by Th27, PBOOLE:def 18;

          

           A86: (L2 . ( indx B)) = L1 by A40, FUNCT_7: 31;

          then ( indx B) = ( indx L2) by Def21;

          then (L2 . ( indx L2)) is Block of (A . ( indx L2)) by A80, FUNCT_7: 31;

          then

          reconsider L3 = ( product L2) as Block of ( Segre_Product A) by Th24;

          assume 2 c= ( card (L /\ SS));

          then

          consider x,y be object such that

           A87: x in (L /\ SS) and

           A88: y in (L /\ SS) and

           A89: x <> y by Th2;

          set y1 = (a1 +* (( indx B),y));

          

           A90: ( dom y1) = I by PARTFUN1:def 2;

          now

            let o be object;

            assume

             A91: o in I;

            per cases ;

              suppose o <> ( indx B);

              then (y1 . o) = (a1 . o) by FUNCT_7: 32;

              hence (y1 . o) in (B . o) by A2, A40, A42, A91, CARD_3: 9;

            end;

              suppose

               A92: o = ( indx B);

              then (y1 . o) = y by A8, FUNCT_7: 31;

              hence (y1 . o) in (B . o) by A54, A88, A92, XBOOLE_0:def 4;

            end;

          end;

          then

           A93: y1 in S by A40, A42, A90, CARD_3: 9;

          

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

          now

            let o be object;

            assume

             A95: o in ( dom L2);

            per cases ;

              suppose

               A96: o <> ( indx B);

              then

               A97: (y1 . o) = (a1 . o) by FUNCT_7: 32;

              (a1 . o) in (B . o) by A2, A40, A42, A94, A95, CARD_3: 9;

              hence (y1 . o) in (L2 . o) by A96, A97, FUNCT_7: 32;

            end;

              suppose

               A98: o = ( indx B);

              then (y1 . o) = y by A8, FUNCT_7: 31;

              hence (y1 . o) in (L2 . o) by A88, A86, A98, XBOOLE_0:def 4;

            end;

          end;

          then y1 in L3 by A94, A90, CARD_3: 9;

          then

           A99: y1 in (L3 /\ S) by A93, XBOOLE_0:def 4;

          set x1 = (a1 +* (( indx B),x));

          

           A100: ( dom x1) = I by PARTFUN1:def 2;

          now

            let o be object;

            assume

             A101: o in I;

            per cases ;

              suppose o <> ( indx B);

              then (x1 . o) = (a1 . o) by FUNCT_7: 32;

              hence (x1 . o) in (B . o) by A2, A40, A42, A101, CARD_3: 9;

            end;

              suppose

               A102: o = ( indx B);

              then (x1 . o) = x by A8, FUNCT_7: 31;

              hence (x1 . o) in (B . o) by A54, A87, A102, XBOOLE_0:def 4;

            end;

          end;

          then

           A103: x1 in S by A40, A42, A100, CARD_3: 9;

          

           A104: (x1 . ( indx B)) = x & (y1 . ( indx B)) = y by A8, FUNCT_7: 31;

          now

            let o be object;

            assume

             A105: o in ( dom L2);

            per cases ;

              suppose

               A106: o <> ( indx B);

              then

               A107: (x1 . o) = (a1 . o) by FUNCT_7: 32;

              (a1 . o) in (B . o) by A2, A40, A42, A94, A105, CARD_3: 9;

              hence (x1 . o) in (L2 . o) by A106, A107, FUNCT_7: 32;

            end;

              suppose

               A108: o = ( indx B);

              then (x1 . o) = x by A8, FUNCT_7: 31;

              hence (x1 . o) in (L2 . o) by A87, A86, A108, XBOOLE_0:def 4;

            end;

          end;

          then x1 in L3 by A94, A100, CARD_3: 9;

          then x1 in (L3 /\ S) by A103, XBOOLE_0:def 4;

          then 2 c= ( card (L3 /\ S)) by A89, A104, A99, Th2;

          then

           A109: L3 c= S by A1;

          thus L c= SS

          proof

            let e be object;

            consider f be object such that

             A110: f in L3 by XBOOLE_0:def 1;

            

             A111: ex F be Function st F = f & ( dom F) = I & for o be object st o in I holds (F . o) in (L2 . o) by A94, A110, CARD_3:def 5;

            then

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

            assume

             A112: e in L;

             A113:

            now

              let o be object;

              assume

               A114: o in ( dom L2);

              per cases ;

                suppose o <> ( indx B);

                then ((f +* (( indx B),e)) . o) = (f . o) by FUNCT_7: 32;

                hence ((f +* (( indx B),e)) . o) in (L2 . o) by A94, A111, A114;

              end;

                suppose

                 A115: o = ( indx B);

                then ((f +* (( indx B),e)) . o) = e by A111, FUNCT_7: 31;

                hence ((f +* (( indx B),e)) . o) in (L2 . o) by A40, A112, A115, FUNCT_7: 31;

              end;

            end;

            ( dom (f +* (( indx B),e))) = ( dom L2) by A94, PARTFUN1:def 2;

            then (f +* (( indx B),e)) in L3 by A113, CARD_3: 9;

            then ((f +* (( indx B),e)) . ( indx B)) in (B . ( indx B)) by A40, A42, A109, CARD_3: 9;

            hence thesis by A54, A111, FUNCT_7: 31;

          end;

        end;

      end;

      given B be Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) such that

       A116: S = ( product B) and

       A117: for C be Subset of (A . ( indx B)) st C = (B . ( indx B)) holds C is strong closed_under_lines;

      thus S is non trivial by A116;

      

       A118: ( dom B) = I by PARTFUN1:def 2;

      

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

      thus S is strong

      proof

        let x,y be Point of ( Segre_Product A);

        assume that

         A120: x in S and

         A121: y in S;

        per cases ;

          suppose x = y;

          hence thesis;

        end;

          suppose

           A122: x <> y;

          consider y1 be Function such that

           A123: y1 = y and

           A124: ( dom y1) = ( dom ( Carrier A)) and

           A125: for a be object st a in ( dom ( Carrier A)) holds (y1 . a) in (( Carrier A) . a) by CARD_3:def 5;

          

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

          then

          reconsider y1 as ManySortedSet of I by A124, PARTFUN1:def 2, RELAT_1:def 18;

          consider x1 be Function such that

           A127: x1 = x and

           A128: ( dom x1) = ( dom ( Carrier A)) and

           A129: for a be object st a in ( dom ( Carrier A)) holds (x1 . a) in (( Carrier A) . a) by CARD_3:def 5;

          reconsider x1 as ManySortedSet of I by A128, A126, PARTFUN1:def 2, RELAT_1:def 18;

           A130:

          now

            assume

             A131: (x1 . ( indx B)) = (y1 . ( indx B));

            now

              let i be object;

              assume i in ( dom ( Carrier A));

              per cases ;

                suppose i <> ( indx B);

                hence (x1 . i) = (y1 . i) by A116, A120, A121, A127, A123, Th23;

              end;

                suppose i = ( indx B);

                hence (x1 . i) = (y1 . i) by A131;

              end;

            end;

            hence contradiction by A122, A127, A128, A123, A124, FUNCT_1: 2;

          end;

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

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

          then

          reconsider C = (B . ( indx B)) as Subset of (A . ( indx B)) by YELLOW_6: 2;

          

           A132: C is strong by A117;

          (y1 . ( indx B)) in (( Carrier A) . ( indx B)) by A119, A125;

          then

          reconsider y1i = (y1 . ( indx B)) as Point of (A . ( indx B)) by YELLOW_6: 2;

          

           A133: y1i in C by A116, A118, A121, A123, CARD_3: 9;

          (x1 . ( indx B)) in (( Carrier A) . ( indx B)) by A119, A129;

          then

          reconsider x1i = (x1 . ( indx B)) as Point of (A . ( indx B)) by YELLOW_6: 2;

          x1i in C by A116, A118, A120, A127, CARD_3: 9;

          then (x1i,y1i) are_collinear by A133, A132;

          then

          consider l be Block of (A . ( indx B)) such that

           A134: {x1i, y1i} c= l by A130;

          

           A135: ( dom {x1}) = I by PARTFUN1:def 2;

          

           A136: for a be object st a in ( dom ( {x1} +* (( indx B),l))) holds (y1 . a) in (( {x1} +* (( indx B),l)) . a)

          proof

            let a be object;

            assume a in ( dom ( {x1} +* (( indx B),l)));

            then

             A137: a in I by PARTFUN1:def 2;

            per cases ;

              suppose

               A138: a = ( indx B);

              then (( {x1} +* (( indx B),l)) . a) = l by A135, FUNCT_7: 31;

              hence thesis by A134, A138, ZFMISC_1: 32;

            end;

              suppose

               A139: a <> ( indx B);

              (x1 . a) in {(x1 . a)} by TARSKI:def 1;

              then (x1 . a) in ( {x1} . a) by A137, PZFMISC1:def 1;

              then (y1 . a) in ( {x1} . a) by A116, A120, A121, A127, A123, A139, Th23;

              hence thesis by A139, FUNCT_7: 32;

            end;

          end;

          ( {x1} +* (( indx B),l)) c= ( Carrier A)

          proof

            let i be object;

            assume

             A140: i in I;

            then

            reconsider i1 = i as Element of I;

            thus (( {x1} +* (( indx B),l)) . i) c= (( Carrier A) . i)

            proof

              per cases ;

                suppose

                 A141: i = ( indx B);

                then (( {x1} +* (( indx B),l)) . i) = l by A135, FUNCT_7: 31;

                then (( {x1} +* (( indx B),l)) . i) in the topology of (A . ( indx B));

                then (( {x1} +* (( indx B),l)) . i) c= the carrier of (A . ( indx B));

                hence thesis by A141, YELLOW_6: 2;

              end;

                suppose

                 A142: i <> ( indx B);

                (x1 . i) in (( Carrier A) . i1) by A119, A129;

                then (x1 . i) in the carrier of (A . i1) by YELLOW_6: 2;

                then

                 A143: {(x1 . i)} c= the carrier of (A . i1) by ZFMISC_1: 31;

                (( {x1} +* (( indx B),l)) . i) = ( {x1} . i) by A142, FUNCT_7: 32

                .= {(x1 . i)} by A140, PZFMISC1:def 1;

                hence thesis by A143, YELLOW_6: 2;

              end;

            end;

          end;

          then

           A144: ( {x1} +* (( indx B),l)) is ManySortedSubset of ( Carrier A) by PBOOLE:def 18;

          for i be Element of I st i <> ( indx B) holds (( {x1} +* (( indx B),l)) . i) is 1 -element

          proof

            let i be Element of I;

            assume i <> ( indx B);

            

            then (( {x1} +* (( indx B),l)) . i) = ( {x1} . i) by FUNCT_7: 32

            .= {(x1 . i)} by PZFMISC1:def 1;

            hence thesis;

          end;

          then

           A145: ( {x1} +* (( indx B),l)) is Segre-like;

          

           A146: for a be object st a in ( dom ( {x1} +* (( indx B),l))) holds (x1 . a) in (( {x1} +* (( indx B),l)) . a)

          proof

            let a be object;

            assume a in ( dom ( {x1} +* (( indx B),l)));

            then

             A147: a in I by PARTFUN1:def 2;

            per cases ;

              suppose

               A148: a = ( indx B);

              then (( {x1} +* (( indx B),l)) . a) = l by A135, FUNCT_7: 31;

              hence thesis by A134, A148, ZFMISC_1: 32;

            end;

              suppose

               A149: a <> ( indx B);

              (x1 . a) in {(x1 . a)} by TARSKI:def 1;

              then (x1 . a) in ( {x1} . a) by A147, PZFMISC1:def 1;

              hence thesis by A149, FUNCT_7: 32;

            end;

          end;

          (( {x1} +* (( indx B),l)) . ( indx B)) is Block of (A . ( indx B)) by A135, FUNCT_7: 31;

          then

          reconsider L = ( product ( {x1} +* (( indx B),l))) as Block of ( Segre_Product A) by A145, A144, Def22;

          ( dom y1) = I by PARTFUN1:def 2

          .= ( dom ( {x1} +* (( indx B),l))) by PARTFUN1:def 2;

          then

           A150: y1 in L by A136, CARD_3: 9;

          ( dom x1) = I by PARTFUN1:def 2

          .= ( dom ( {x1} +* (( indx B),l))) by PARTFUN1:def 2;

          then x1 in L by A146, CARD_3: 9;

          then {x, y} c= L by A127, A123, A150, ZFMISC_1: 32;

          hence thesis;

        end;

      end;

      thus S is closed_under_lines

      proof

        let l be Block of ( Segre_Product A);

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

         A151: l = ( product L) and

         A152: ex i be Element of I st (L . i) is Block of (A . i) by Def22;

        assume

         A153: 2 c= ( card (l /\ S));

        then

        consider a,b be object such that

         A154: a in (l /\ S) and

         A155: b in (l /\ S) and

         A156: a <> b by Th2;

        ( card (l /\ S)) c= ( card l) by CARD_1: 11, XBOOLE_1: 17;

        then 2 c= ( card l) by A153;

        then

        reconsider L as Segre-like non trivial-yielding ManySortedSubset of ( Carrier A) by A151, Th13;

        reconsider a1 = a, b1 = b as ManySortedSet of I by A154, A155, Th14;

        

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

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

        

         A158: ( indx B) = ( indx L) by A116, A153, A151, Th26;

        for a be object st a in ( dom L) holds (L . a) c= (B . a)

        proof

          let a be object;

          assume a in ( dom L);

          per cases ;

            suppose a <> ( indx B);

            hence thesis by A116, A153, A151, Th26;

          end;

            suppose

             A159: a = ( indx B);

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

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

            then

            reconsider C = (B . ( indx B)) as Subset of (A . ( indx B)) by YELLOW_6: 2;

            consider j be Element of I such that

             A160: (L . j) is Block of (A . j) by A152;

            2 c= ( card (L . j)) by A160, Def6;

            then (L . j) is non trivial by Th4;

            then j = ( indx L) by Def21;

            then

            reconsider Li = (L . ( indx B)) as Block of (A . ( indx B)) by A158, A160;

            

             A161: C is closed_under_lines by A117;

            a1 in ( product L) by A154, A151, XBOOLE_0:def 4;

            then

             A162: (a1 . ( indx B)) in (L . ( indx B)) by A118, A157, CARD_3: 9;

            b1 in ( product L) by A155, A151, XBOOLE_0:def 4;

            then

             A163: (b1 . ( indx B)) in (L . ( indx B)) by A118, A157, CARD_3: 9;

            

             A164: b1 in ( product B) by A116, A155, XBOOLE_0:def 4;

            then (b1 . ( indx B)) in (B . ( indx B)) by A118, CARD_3: 9;

            then

             A165: (b1 . ( indx B)) in (Li /\ C) by A163, XBOOLE_0:def 4;

            

             A166: a1 in ( product B) by A116, A154, XBOOLE_0:def 4;

             A167:

            now

              assume

               A168: (a1 . ( indx B)) = (b1 . ( indx B));

              

               A169: for o be object st o in ( dom a1) holds (a1 . o) = (b1 . o)

              proof

                let o be object;

                assume o in ( dom a1);

                per cases ;

                  suppose o <> ( indx B);

                  hence thesis by A166, A164, Th23;

                end;

                  suppose o = ( indx B);

                  hence thesis by A168;

                end;

              end;

              ( dom a1) = I by PARTFUN1:def 2

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

              hence contradiction by A156, A169, FUNCT_1: 2;

            end;

            (a1 . ( indx B)) in (B . ( indx B)) by A118, A166, CARD_3: 9;

            then (a1 . ( indx B)) in (Li /\ C) by A162, XBOOLE_0:def 4;

            then 2 c= ( card (Li /\ C)) by A167, A165, Th2;

            hence thesis by A159, A161;

          end;

        end;

        hence thesis by A116, A151, A157, CARD_3: 27;

      end;

    end;