polyform.miz



    begin

    theorem :: POLYFORM:1

    

     Th1: for X be set, c,d be object st (ex a,b be object st a <> b & X = {a, b}) & c in X & d in X & c <> d holds X = {c, d}

    proof

      let X be set, c,d be object such that

       A1: ex a,b be object st a <> b & X = {a, b} and

       A2: c in X and

       A3: d in X and

       A4: c <> d;

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

       A5: X = {a, b} by A1;

      

       A6: X c= {c, d}

      proof

        

         A7: d = a or d = b by A3, A5, TARSKI:def 2;

        

         A8: c = a or c = b by A2, A5, TARSKI:def 2;

        let x be object such that

         A9: x in X;

        per cases by A5, A9, TARSKI:def 2;

          suppose x = a;

          hence thesis by A4, A8, A7, TARSKI:def 2;

        end;

          suppose x = b;

          hence thesis by A4, A8, A7, TARSKI:def 2;

        end;

      end;

       {c, d} c= X by A2, A3, ZFMISC_1: 32;

      hence thesis by A6;

    end;

    begin

    reserve n for Nat,

k for Integer;

    ::$Canceled

    theorem :: POLYFORM:3

    

     Th2: 1 <= k implies k is Nat

    proof

      assume 1 <= k;

      then

      reconsider k as Element of NAT by INT_1: 3;

      k is Nat;

      hence thesis;

    end;

    theorem :: POLYFORM:4

    

     Th3: 1 is odd

    proof

      1 = ((2 * 0 ) + 1);

      hence thesis;

    end;

    theorem :: POLYFORM:5

    

     Th4: 2 is even

    proof

      2 = (2 * 1);

      hence thesis;

    end;

    theorem :: POLYFORM:6

    

     Th5: 3 is odd

    proof

      3 = ((2 * 1) + 1);

      hence thesis;

    end;

    theorem :: POLYFORM:7

    

     Th6: 4 is even

    proof

      4 = (2 * 2);

      hence thesis;

    end;

    theorem :: POLYFORM:8

    

     Th7: n is even implies (( - 1) |^ n) = 1

    proof

      assume

       A1: n is even;

      (( - 1) |^ n) = (( - 1) to_power n) by POWER: 41;

      hence thesis by A1, FIB_NUM2: 3;

    end;

    theorem :: POLYFORM:9

    

     Th8: n is odd implies (( - 1) |^ n) = ( - 1)

    proof

      assume

       A1: n is odd;

      (( - 1) |^ n) = (( - 1) to_power n) by POWER: 41;

      hence thesis by A1, FIB_NUM2: 2;

    end;

    ::$Canceled

    

     Lm1: for x be Element of NAT st 0 < x holds ( 0 qua Nat + 1) <= x by NAT_1: 13;

    theorem :: POLYFORM:11

    

     Th9: for p,q,r be FinSequence holds ( len (p ^ q)) <= ( len (p ^ (q ^ r)))

    proof

      let p,q,r be FinSequence;

      ( len ((p ^ q) ^ r)) = ( len (p ^ (q ^ r))) by FINSEQ_1: 32;

      hence thesis by CALCUL_1: 6;

    end;

    theorem :: POLYFORM:12

    

     Th10: 1 < (n + 2)

    proof

       0 < (n + 1) implies 1 < (n + 2)

      proof

        assume 0 < (n + 1);

        ( 0 qua Nat + 1) = 1;

        hence thesis by XREAL_1: 8;

      end;

      hence thesis;

    end;

    theorem :: POLYFORM:13

    

     Th11: (( - 1) |^ 2) = 1

    proof

      (( - 1) |^ 2) = (( - 1) |^ (1 + 1))

      .= ((( - 1) |^ 1) * (( - 1) |^ 1)) by NEWTON: 8

      .= ((( - 1) |^ 1) * ( - 1))

      .= (( - 1) * ( - 1));

      hence thesis;

    end;

    theorem :: POLYFORM:14

    

     Th12: for n be Nat holds (( - 1) |^ n) = (( - 1) |^ (n + 2))

    proof

      let n be Nat;

      (( - 1) |^ (n + 2)) = ((( - 1) |^ n) * (( - 1) |^ 2)) by NEWTON: 8

      .= (( - 1) |^ n) by Th11;

      hence thesis;

    end;

    begin

    theorem :: POLYFORM:15

    

     Th13: for a,b,s be FinSequence of INT st ( len s) > 0 & ( len a) = ( len s) & ( len b) = ( len s) & (for n be Nat st 1 <= n & n <= ( len s) holds (s . n) = ((a . n) + (b . n))) & (for k be Nat st 1 <= k & k < ( len s) holds (b . k) = ( - (a . (k + 1)))) holds ( Sum s) = ((a . 1) + (b . ( len s)))

    proof

      defpred P[ FinSequence of INT ] means ( len $1) > 0 implies for a,b be FinSequence of INT st ( len a) = ( len $1) & ( len b) = ( len $1) & (for n be Nat st 1 <= n & n <= ( len $1) holds ($1 . n) = ((a . n) + (b . n))) & (for k be Nat st 1 <= k & k < ( len $1) holds (b . k) = ( - (a . (k + 1)))) holds ( Sum $1) = ((a . 1) + (b . ( len $1)));

      

       A1: for p be FinSequence of INT , x be Element of INT st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence of INT , x be Element of INT such that

         A2: P[p];

        set t = (p ^ <*x*>);

        assume ( len t) > 0 ;

        let a,b be FinSequence of INT such that

         A3: ( len a) = ( len t) and

         A4: ( len b) = ( len t) and

         A5: for n be Nat st 1 <= n & n <= ( len t) holds (t . n) = ((a . n) + (b . n)) and

         A6: for k be Nat st 1 <= k & k < ( len t) holds (b . k) = ( - (a . (k + 1)));

        

         A7: ( Sum t) = (( Sum p) + x) by RVSUM_1: 74;

        per cases ;

          suppose

           A8: ( len p) = 0 ;

          reconsider egy = 1 as Nat;

          p = {} by A8;

          then

           A9: t = <*x*> by FINSEQ_1: 34;

          then egy <= ( len t) by FINSEQ_1: 39;

          then

           A10: (t . egy) = ((a . egy) + (b . egy)) by A5;

          

           A11: p = {} by A8;

          ( len t) = 1 by A9, FINSEQ_1: 39;

          hence thesis by A7, A11, A9, A10, FINSEQ_1: 40, GR_CY_1: 3;

        end;

          suppose

           A12: ( len p) > 0 ;

          set m = ( len p);

          set a9 = (a | m);

          

           A13: (a9 . 1) = (a . 1)

          proof

            reconsider egy = 1 as Element of NAT ;

            ( 0 qua Nat + 1) = 1;

            then egy <= ( len p) by A12, INT_1: 7;

            hence thesis by FINSEQ_3: 112;

          end;

          set b9 = (b | m);

          

           A14: (b . ( len p)) = (b9 . ( len p)) by FINSEQ_3: 112;

          

           A15: for n be Nat st 1 <= n & n < ( len p) holds (b9 . n) = ( - (a9 . (n + 1)))

          proof

            let n be Nat such that

             A16: 1 <= n and

             A17: n < ( len p);

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

            

             A18: (b9 . n) = (b . n) by A17, FINSEQ_3: 112;

            (n + 1) <= ( len p) by A17, INT_1: 7;

            then

             A19: (a9 . (n + 1)) = (a . (n + 1)) by FINSEQ_3: 112;

            ( len p) <= ( len t) by CALCUL_1: 6;

            then n < ( len t) by A17, XXREAL_0: 2;

            hence thesis by A6, A16, A18, A19;

          end;

          

           A20: for n be Nat st 1 <= n & n <= ( len p) holds (p . n) = ((a9 . n) + (b9 . n))

          proof

            let n be Nat such that

             A21: 1 <= n and

             A22: n <= ( len p);

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

            then

             A23: n in ( dom p) by A21, A22;

            ( len p) <= ( len t) by CALCUL_1: 6;

            then

             A24: n <= ( len t) by A22, XXREAL_0: 2;

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

            (p . n) = (t . n) by A23, FINSEQ_1:def 7

            .= ((a . n) + (b . n)) by A5, A21, A24

            .= ((a9 . n) + (b . n)) by A22, FINSEQ_3: 112

            .= ((a9 . n) + (b9 . n)) by A22, FINSEQ_3: 112;

            hence thesis;

          end;

          

           A25: 1 <= ( len p) by A12, Lm1;

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

          then

           A26: ( len t) = (( len p) + 1) by FINSEQ_1: 22;

          ( 0 qua Nat + ( len p)) = ( len p);

          then ( len p) < ( len t) by A26, XREAL_1: 6;

          then

           A27: (b . ( len p)) = ( - (a . (( len p) + 1))) by A6, A25;

          ( 0 qua Nat + 1) = 1;

          then

           A28: 1 <= ( len t) by A26, XREAL_1: 6;

          

           A29: x = (t . (( len p) + 1)) by FINSEQ_1: 42

          .= (( - (b9 . ( len p))) + (b . ( len t))) by A5, A26, A28, A27, A14;

          m <= ( len b) by A4, CALCUL_1: 6;

          then

           A30: ( len b9) = ( len p) by FINSEQ_1: 59;

          m <= ( len a) by A3, CALCUL_1: 6;

          then ( len a9) = ( len p) by FINSEQ_1: 59;

          then ( Sum p) = ((a9 . 1) + (b9 . ( len p))) by A2, A12, A30, A20, A15;

          hence thesis by A7, A13, A29;

        end;

      end;

      

       A31: P[( <*> INT )];

      

       A32: for p be FinSequence of INT holds P[p] from FINSEQ_2:sch 2( A31, A1);

      let a,b,s be FinSequence of INT ;

      assume ( len s) > 0 & ( len a) = ( len s) & (( len b) = ( len s) & for n be Nat st 1 <= n & n <= ( len s) holds (s . n) = ((a . n) + (b . n))) & for k be Nat st 1 <= k & k < ( len s) holds (b . k) = ( - (a . (k + 1)));

      hence thesis by A32;

    end;

    theorem :: POLYFORM:16

    

     Th14: for p,q,r be FinSequence holds ( len ((p ^ q) ^ r)) = ((( len p) + ( len q)) + ( len r))

    proof

      let p,q,r be FinSequence;

      ( len ((p ^ q) ^ r)) = (( len (p ^ q)) + ( len r)) by FINSEQ_1: 22

      .= ((( len p) + ( len q)) + ( len r)) by FINSEQ_1: 22;

      hence thesis;

    end;

    theorem :: POLYFORM:17

    

     Th15: for x be set, p,q be FinSequence holds ((( <*x*> ^ p) ^ q) . 1) = x

    proof

      let x be set, p,q be FinSequence;

      (( <*x*> ^ p) ^ q) = ( <*x*> ^ (p ^ q)) by FINSEQ_1: 32;

      hence thesis by FINSEQ_1: 41;

    end;

    theorem :: POLYFORM:18

    

     Th16: for x be set, p,q be FinSequence holds (((p ^ q) ^ <*x*>) . ((( len p) + ( len q)) + 1)) = x

    proof

      let x be set, p,q be FinSequence;

      set s = (p ^ q);

      ((s ^ <*x*>) . (( len s) + 1)) = x by FINSEQ_1: 42;

      hence thesis by FINSEQ_1: 22;

    end;

    theorem :: POLYFORM:19

    

     Th17: for p,q,r be FinSequence, k be Nat st ( len p) < k & k <= ( len (p ^ q)) holds (((p ^ q) ^ r) . k) = (q . (k - ( len p)))

    proof

      let p,q,r be FinSequence, k be Nat such that

       A1: ( len p) < k and

       A2: k <= ( len (p ^ q));

      set n = (k - ( len p));

      (( len p) - ( len p)) = 0 ;

      then

       A3: 0 < n by A1, XREAL_1: 9;

      ( 0 qua Nat + 1) = 1;

      then

       A4: 1 <= n by A3, INT_1: 7;

      then

      reconsider n as Nat by Th2;

      

       A5: ((( len p) + ( len q)) - ( len p)) = ( len q);

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

      then n <= ( len q) by A5, XREAL_1: 9;

      then n in ( Seg ( len q)) by A4;

      then

       A6: n in ( dom q) by FINSEQ_1:def 3;

      ( len (p ^ q)) <= ( len (p ^ (q ^ r))) by Th9;

      then k <= ( len (p ^ (q ^ r))) by A2, XXREAL_0: 2;

      then

       A7: ((p ^ (q ^ r)) . k) = ((q ^ r) . (k - ( len p))) by A1, FINSEQ_1: 24;

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

      ((q ^ r) . n) = (q . n) by A6, FINSEQ_1:def 7;

      hence thesis by A7, FINSEQ_1: 32;

    end;

    definition

      let a be Integer;

      :: original: <*

      redefine

      func <*a*> -> FinSequence of INT ;

      coherence

      proof

        set s = <*a*>;

        a in INT by INT_1:def 2;

        then ( rng s) = {a} & {a} c= INT by FINSEQ_1: 38, ZFMISC_1: 31;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    definition

      let a,b be Integer;

      :: original: <*

      redefine

      func <*a,b*> -> FinSequence of INT ;

      coherence

      proof

        set s = <*a, b*>;

        a in INT & b in INT by INT_1:def 2;

        then ( rng s) = {a, b} & {a, b} c= INT by FINSEQ_2: 127, ZFMISC_1: 32;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    definition

      let a,b,c be Integer;

      :: original: <*

      redefine

      func <*a,b,c*> -> FinSequence of INT ;

      coherence

      proof

        set s = <*a, b, c*>;

        

         A1: c in INT by INT_1:def 2;

        a in INT & b in INT by INT_1:def 2;

        then ( rng s) = {a, b, c} & {a, b, c} c= INT by A1, FINSEQ_2: 128, ZFMISC_1: 133;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    theorem :: POLYFORM:20

    

     Th18: for k be Integer, p be FinSequence of INT holds ( Sum ( <*k*> ^ p)) = (k + ( Sum p))

    proof

      let k be Integer, p be FinSequence of INT ;

      

      thus ( Sum ( <*k*> ^ p)) = (( Sum p) + ( Sum <*k*>)) by RVSUM_1: 75

      .= ( Sum (p ^ <*k*>)) by RVSUM_1: 75

      .= (k + ( Sum p)) by RVSUM_1: 74;

    end;

    theorem :: POLYFORM:21

    

     Th19: for p,q,r be FinSequence of INT holds ( Sum ((p ^ q) ^ r)) = ((( Sum p) + ( Sum q)) + ( Sum r))

    proof

      let p,q,r be FinSequence of INT ;

      

      thus ( Sum ((p ^ q) ^ r)) = (( Sum (p ^ q)) + ( Sum r)) by RVSUM_1: 75

      .= ((( Sum p) + ( Sum q)) + ( Sum r)) by RVSUM_1: 75;

    end;

    theorem :: POLYFORM:22

    for a be Element of Z_2 holds ( Sum <*a*>) = a by FINSOP_1: 11;

    begin

    definition

      let X,Y be set;

      mode incidence-matrix of X,Y is Element of ( Funcs ( [:X, Y:], {( 0. Z_2 ), ( 1. Z_2 )}));

    end

    theorem :: POLYFORM:23

    

     Th21: for X,Y be set holds ( [:X, Y:] --> ( 1. Z_2 )) is incidence-matrix of X, Y

    proof

      let X,Y be set;

      set f = ( [:X, Y:] --> ( 1. Z_2 ));

      ( rng f) c= {( 1. Z_2 )} & {( 1. Z_2 )} c= {( 0. Z_2 ), ( 1. Z_2 )} by FUNCOP_1: 13, ZFMISC_1: 7;

      then ( dom f) = [:X, Y:] & ( rng f) c= {( 0. Z_2 ), ( 1. Z_2 )};

      hence thesis by FUNCT_2:def 2;

    end;

    definition

      struct PolyhedronStr (# the PolytopsF -> FinSequence-yielding FinSequence,

the IncidenceF -> Function-yielding FinSequence #)

       attr strict strict;

    end

    definition

      let p be PolyhedronStr;

      :: POLYFORM:def1

      attr p is polyhedron_1 means ( len the IncidenceF of p) = (( len the PolytopsF of p) - 1);

      :: POLYFORM:def2

      attr p is polyhedron_2 means

      : Def2: for n be Nat st 1 <= n & n < ( len the PolytopsF of p) holds (the IncidenceF of p . n) is incidence-matrix of ( rng (the PolytopsF of p . n)), ( rng (the PolytopsF of p . (n + 1)));

      :: POLYFORM:def3

      attr p is polyhedron_3 means

      : Def3: for n be Nat st 1 <= n & n <= ( len the PolytopsF of p) holds (the PolytopsF of p . n) is non empty & (the PolytopsF of p . n) is one-to-one;

    end

    registration

      cluster polyhedron_1 polyhedron_2 polyhedron_3 for PolyhedronStr;

      existence

      proof

        reconsider I = ( <*> {} ) as Function-yielding FinSequence;

        reconsider F = <* <* {} *>*> as FinSequence-yielding FinSequence;

        take p = PolyhedronStr (# F, I #);

        

         A1: ( len F) = 1 by FINSEQ_1: 39;

        thus p is polyhedron_1 by A1;

        thus p is polyhedron_2 by A1;

        let n be Nat;

        assume 1 <= n & n <= ( len the PolytopsF of p);

        then n = 1 by A1, XXREAL_0: 1;

        hence thesis by FINSEQ_1:def 8;

      end;

    end

    definition

      mode polyhedron is polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr;

    end

    reserve p for polyhedron,

k for Integer,

n for Nat;

    definition

      let p be polyhedron;

      :: POLYFORM:def4

      func dim (p) -> Element of NAT equals ( len the PolytopsF of p);

      coherence ;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def5

      func k -polytopes (p) -> finite set means

      : Def5: (k < ( - 1) implies it = {} ) & (k = ( - 1) implies it = { {} }) & (( - 1) < k & k < ( dim p) implies it = ( rng (the PolytopsF of p . (k + 1)))) & (k = ( dim p) implies it = {p}) & (k > ( dim p) implies it = {} );

      existence

      proof

        set F = the PolytopsF of p;

        per cases by XXREAL_0: 1;

          suppose

           A1: k < ( - 1);

          take {} ;

          thus thesis by A1;

        end;

          suppose

           A2: k = ( - 1);

          take { {} };

          thus thesis by A2;

        end;

          suppose

           A3: ( - 1) < k & k < ( dim p);

          (( - 1) + 1) = 0 ;

          then 0 <= k by A3, INT_1: 7;

          then

          reconsider k as Element of NAT by INT_1: 3;

          set n = (k + 1);

          reconsider Fn = (F . n) as FinSequence;

          take ( rng Fn);

          thus thesis by A3;

        end;

          suppose

           A4: k = ( dim p);

          take {p};

          thus thesis by A4;

        end;

          suppose

           A5: k > ( dim p);

          take {} ;

          thus thesis by A5;

        end;

      end;

      uniqueness

      proof

        set F = the PolytopsF of p;

        let X,Y be finite set such that

         A6: k < ( - 1) implies X = {} and

         A7: k = ( - 1) implies X = { {} } and

         A8: ( - 1) < k & k < ( dim p) implies X = ( rng (F . (k + 1))) and

         A9: k = ( dim p) implies X = {p} and

         A10: k > ( dim p) implies X = {} and

         A11: k < ( - 1) implies Y = {} and

         A12: k = ( - 1) implies Y = { {} } and

         A13: ( - 1) < k & k < ( dim p) implies Y = ( rng (F . (k + 1))) and

         A14: k = ( dim p) implies Y = {p} and

         A15: k > ( dim p) implies Y = {} ;

        per cases by XXREAL_0: 1;

          suppose k < ( - 1);

          hence thesis by A6, A11;

        end;

          suppose k = ( - 1);

          hence thesis by A7, A12;

        end;

          suppose ( - 1) < k & k < ( dim p);

          hence thesis by A8, A13;

        end;

          suppose k = ( dim p);

          hence thesis by A9, A14;

        end;

          suppose k > ( dim p);

          hence thesis by A10, A15;

        end;

      end;

    end

    theorem :: POLYFORM:24

    

     Th22: ( - 1) < k & k < ( dim p) implies (k + 1) is Nat & 1 <= (k + 1) & (k + 1) <= ( dim p)

    proof

      

       A1: (( - 1) + 1) = 0 ;

      assume ( - 1) < k;

      then

       A2: 0 < (k + 1) by A1, XREAL_1: 6;

      then

      reconsider n = (k + 1) as Element of NAT by INT_1: 3;

      

       A3: n is Nat & ( 0 qua Nat + 1) = 1;

      assume k < ( dim p);

      hence thesis by A2, A3, INT_1: 7;

    end;

    theorem :: POLYFORM:25

    

     Th23: (k -polytopes p) is non empty iff ( - 1) <= k & k <= ( dim p)

    proof

      set X = (k -polytopes p);

      thus X is non empty implies ( - 1) <= k & k <= ( dim p) by Def5;

      thus ( - 1) <= k & k <= ( dim p) implies (k -polytopes p) is non empty

      proof

        assume

         A1: ( - 1) <= k;

        assume

         A2: k <= ( dim p);

        per cases by A1, A2, XXREAL_0: 1;

          suppose k = ( - 1);

          hence thesis by Def5;

        end;

          suppose

           A3: ( - 1) < k & k < ( dim p);

          set F = the PolytopsF of p;

          

           A4: (k -polytopes p) = ( rng (F . (k + 1))) by A3, Def5;

          set n = (k + 1);

          

           A5: 1 <= n by A3, Th22;

          

           A6: n <= ( dim p) by A3, Th22;

          reconsider n as Element of NAT by A5, INT_1: 3;

          reconsider n as Nat;

          (F . n) is non empty by A5, A6, Def3;

          hence thesis by A4;

        end;

          suppose k = ( dim p);

          then (k -polytopes p) = {p} by Def5;

          hence thesis;

        end;

      end;

    end;

    theorem :: POLYFORM:26

    k < ( dim p) implies (k - 1) < ( dim p) by XREAL_1: 146, XXREAL_0: 2;

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def6

      func eta (p,k) -> incidence-matrix of ((k - 1) -polytopes p), (k -polytopes p) means

      : Def6: (k < 0 implies it = {} ) & (k = 0 implies it = ( [: { {} }, ( 0 -polytopes p):] --> ( 1. Z_2 ))) & ( 0 < k & k < ( dim p) implies it = (the IncidenceF of p . k)) & (k = ( dim p) implies it = ( [:((( dim p) - 1) -polytopes p), {p}:] --> ( 1. Z_2 ))) & (k > ( dim p) implies it = {} );

      existence

      proof

        per cases by XXREAL_0: 1;

          suppose

           A1: k < 0 ;

          set f = {} ;

          reconsider f as Function;

          (k - 1) < ( 0 qua Nat - 1) by A1, XREAL_1: 9;

          then ((k - 1) -polytopes p) = {} by Def5;

          then [:((k - 1) -polytopes p), (k -polytopes p):] = {} by ZFMISC_1: 90;

          then

          reconsider f as Function of [:((k - 1) -polytopes p), (k -polytopes p):], {( 0. Z_2 ), ( 1. Z_2 )} by RELSET_1: 12;

          reconsider f as Element of ( Funcs ( [:((k - 1) -polytopes p), (k -polytopes p):], {( 0. Z_2 ), ( 1. Z_2 )})) by FUNCT_2: 8;

          take f;

          thus thesis by A1;

        end;

          suppose

           A2: k > ( dim p);

          set f = {} ;

          reconsider f as Function;

          (k -polytopes p) = {} by A2, Th23;

          then [:((k - 1) -polytopes p), (k -polytopes p):] = {} by ZFMISC_1: 90;

          then

          reconsider f as Function of [:((k - 1) -polytopes p), (k -polytopes p):], {( 0. Z_2 ), ( 1. Z_2 )} by RELSET_1: 12;

          reconsider f as Element of ( Funcs ( [:((k - 1) -polytopes p), (k -polytopes p):], {( 0. Z_2 ), ( 1. Z_2 )})) by FUNCT_2: 8;

          take f;

          thus thesis by A2;

        end;

          suppose

           A3: 0 < k & k < ( dim p);

          set F = the PolytopsF of p, I = the IncidenceF of p;

          

           A4: (k -polytopes p) = ( rng (F . (k + 1))) by A3, Def5;

          

           A5: (k - 1) < ( dim p) by A3, XREAL_1: 146, XXREAL_0: 2;

          ( 0 qua Nat + 1) = 1;

          then

           A6: 1 <= k by A3, INT_1: 7;

          then

          reconsider k9 = k as Nat by Th2;

          (1 - 1) = 0 ;

          then ( - 1) < (k - 1) by A6, XREAL_1: 9;

          then ((k - 1) -polytopes p) = ( rng (F . ((k - 1) + 1))) by A5, Def5;

          then

          reconsider Ik = (I . k9) as incidence-matrix of ((k - 1) -polytopes p), (k -polytopes p) by A3, A6, A4, Def2;

          take Ik;

          thus thesis by A3;

        end;

          suppose

           A7: k = 0 ;

          per cases ;

            suppose

             A8: k = ( dim p);

            set f = ( [: { {} }, {p}:] --> ( 1. Z_2 ));

            reconsider f as incidence-matrix of { {} }, {p} by Th21;

            ((k - 1) -polytopes p) = { {} } by A7, Def5;

            then

            reconsider f as incidence-matrix of ((k - 1) -polytopes p), (k -polytopes p) by A8, Def5;

            take f;

            thus thesis by A7, A8, Def5;

          end;

            suppose

             A9: k <> ( dim p);

            set f = ( [: { {} }, ( 0 -polytopes p):] --> ( 1. Z_2 ));

            reconsider f as incidence-matrix of { {} }, ( 0 -polytopes p) by Th21;

            reconsider f as incidence-matrix of ((k - 1) -polytopes p), (k -polytopes p) by A7, Def5;

            take f;

            thus thesis by A7, A9;

          end;

        end;

          suppose

           A10: k = ( dim p);

          per cases ;

            suppose

             A11: k = 0 ;

            set f = ( [: { {} }, {p}:] --> ( 1. Z_2 ));

            reconsider f as incidence-matrix of { {} }, {p} by Th21;

            ((k - 1) -polytopes p) = { {} } by A11, Def5;

            then

            reconsider f as incidence-matrix of ((k - 1) -polytopes p), (k -polytopes p) by A10, Def5;

            take f;

            thus thesis by A10, A11, Def5;

          end;

            suppose

             A12: k <> 0 ;

            set f = ( [:((( dim p) - 1) -polytopes p), {p}:] --> ( 1. Z_2 ));

            reconsider f as incidence-matrix of ((( dim p) - 1) -polytopes p), {p} by Th21;

            reconsider f as incidence-matrix of ((k - 1) -polytopes p), (k -polytopes p) by A10, Def5;

            take f;

            thus thesis by A10, A12;

          end;

        end;

      end;

      uniqueness

      proof

        set I = the IncidenceF of p;

        let s,t be incidence-matrix of ((k - 1) -polytopes p), (k -polytopes p) such that

         A13: k < 0 implies s = {} and

         A14: k = 0 implies s = ( [: { {} }, ( 0 -polytopes p):] --> ( 1. Z_2 )) and

         A15: 0 < k & k < ( dim p) implies s = (I . k) and

         A16: k = ( dim p) implies s = ( [:((( dim p) - 1) -polytopes p), {p}:] --> ( 1. Z_2 )) and

         A17: k > ( dim p) implies s = {} and k < 0 implies t = {} and

         A18: k = 0 implies t = ( [: { {} }, ( 0 -polytopes p):] --> ( 1. Z_2 )) and

         A19: 0 < k & k < ( dim p) implies t = (I . k) and

         A20: k = ( dim p) implies t = ( [:((( dim p) - 1) -polytopes p), {p}:] --> ( 1. Z_2 )) and k > ( dim p) implies t = {} ;

        per cases by XXREAL_0: 1;

          suppose k < 0 ;

          hence thesis by A13;

        end;

          suppose k = 0 ;

          hence thesis by A14, A18;

        end;

          suppose 0 < k & k < ( dim p);

          hence thesis by A15, A19;

        end;

          suppose k = ( dim p);

          hence thesis by A16, A20;

        end;

          suppose k > ( dim p);

          hence thesis by A17;

        end;

      end;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def7

      func k -polytope-seq (p) -> FinSequence means

      : Def7: (k < ( - 1) implies it = ( <*> {} )) & (k = ( - 1) implies it = <* {} *>) & (( - 1) < k & k < ( dim p) implies it = (the PolytopsF of p . (k + 1))) & (k = ( dim p) implies it = <*p*>) & (k > ( dim p) implies it = ( <*> {} ));

      existence

      proof

        per cases by XXREAL_0: 1;

          suppose

           A1: k < ( - 1);

          take ( <*> {} );

          thus thesis by A1;

        end;

          suppose

           A2: k = ( - 1);

          take <* {} *>;

          thus thesis by A2;

        end;

          suppose

           A3: ( - 1) < k & k < ( dim p);

          set F = the PolytopsF of p;

          take (F . (k + 1));

          thus thesis by A3;

        end;

          suppose

           A4: k = ( dim p);

          take <*p*>;

          thus thesis by A4;

        end;

          suppose

           A5: k > ( dim p);

          take ( <*> {} );

          thus thesis by A5;

        end;

      end;

      uniqueness

      proof

        set F = the PolytopsF of p;

        let s,t be FinSequence such that

         A6: k < ( - 1) implies s = ( <*> {} ) and

         A7: k = ( - 1) implies s = <* {} *> and

         A8: ( - 1) < k & k < ( dim p) implies s = (F . (k + 1)) and

         A9: k = ( dim p) implies s = <*p*> and

         A10: k > ( dim p) implies s = ( <*> {} ) and

         A11: k < ( - 1) implies t = ( <*> {} ) and

         A12: k = ( - 1) implies t = <* {} *> and

         A13: ( - 1) < k & k < ( dim p) implies t = (F . (k + 1)) and

         A14: k = ( dim p) implies t = <*p*> and

         A15: k > ( dim p) implies t = ( <*> {} );

        per cases by XXREAL_0: 1;

          suppose k < ( - 1);

          hence thesis by A6, A11;

        end;

          suppose k = ( - 1);

          hence thesis by A7, A12;

        end;

          suppose ( - 1) < k & k < ( dim p);

          hence thesis by A8, A13;

        end;

          suppose k = ( dim p);

          hence thesis by A9, A14;

        end;

          suppose k > ( dim p);

          hence thesis by A10, A15;

        end;

      end;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def8

      func num-polytopes (p,k) -> Element of NAT equals ( card (k -polytopes p));

      coherence ;

    end

    definition

      let p be polyhedron;

      :: POLYFORM:def9

      func num-vertices (p) -> Element of NAT equals ( num-polytopes (p, 0 ));

      correctness ;

      :: POLYFORM:def10

      func num-edges (p) -> Element of NAT equals ( num-polytopes (p,1));

      correctness ;

      :: POLYFORM:def11

      func num-faces (p) -> Element of NAT equals ( num-polytopes (p,2));

      correctness ;

    end

    theorem :: POLYFORM:27

    

     Th25: ( dom (k -polytope-seq p)) = ( Seg ( num-polytopes (p,k)))

    proof

      set F = the PolytopsF of p;

      per cases ;

        suppose k < ( - 1);

        then (k -polytope-seq p) = ( <*> {} ) & (k -polytopes p) = {} by Def5, Def7;

        hence thesis by FINSEQ_1:def 3;

      end;

        suppose

         A1: ( - 1) <= k & k <= ( dim p);

        per cases by A1, XXREAL_0: 1;

          suppose

           A2: k = ( - 1);

          then (k -polytope-seq p) = <* {} *> by Def7;

          then

           A3: ( len (k -polytope-seq p)) = 1 by FINSEQ_1: 39;

          (k -polytopes p) = { {} } by A2, Def5;

          then ( num-polytopes (p,k)) = 1 by CARD_2: 42;

          hence thesis by A3, FINSEQ_1:def 3;

        end;

          suppose

           A4: ( - 1) < k & k < ( dim p);

          set n = (k + 1);

          reconsider n as Nat by A4, Th22;

          reconsider Fn = (F . n) as FinSequence;

          1 <= n & n <= ( dim p) by A4, Th22;

          then

           A5: Fn is one-to-one by Def3;

          (k -polytopes p) = ( rng (F . (k + 1))) by A4, Def5;

          then ( num-polytopes (p,k)) = ( card ( dom Fn)) by A5, CARD_1: 70;

          then

           A6: ( len Fn) = ( num-polytopes (p,k)) by CARD_1: 62;

          (k -polytope-seq p) = (F . (k + 1)) by A4, Def7;

          hence thesis by A6, FINSEQ_1:def 3;

        end;

          suppose

           A7: k = ( dim p);

          then (k -polytope-seq p) = <*p*> by Def7;

          then

           A8: ( len (k -polytope-seq p)) = 1 by FINSEQ_1: 39;

          (k -polytopes p) = {p} by A7, Def5;

          then ( num-polytopes (p,k)) = 1 by CARD_2: 42;

          hence thesis by A8, FINSEQ_1:def 3;

        end;

      end;

        suppose k > ( dim p);

        then (k -polytope-seq p) = ( <*> {} ) & (k -polytopes p) = {} by Def5, Def7;

        hence thesis by FINSEQ_1:def 3;

      end;

    end;

    theorem :: POLYFORM:28

    

     Th26: ( len (k -polytope-seq p)) = ( num-polytopes (p,k))

    proof

      ( dom (k -polytope-seq p)) = ( Seg ( num-polytopes (p,k))) by Th25;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: POLYFORM:29

    

     Th27: ( rng (k -polytope-seq p)) = (k -polytopes p)

    proof

      set F = the PolytopsF of p;

      per cases ;

        suppose

         A1: k < ( - 1);

        then (k -polytopes p) = {} by Def5;

        hence thesis by A1, Def7, RELAT_1: 38;

      end;

        suppose

         A2: ( - 1) <= k & k <= ( dim p);

        per cases by A2, XXREAL_0: 1;

          suppose k = ( - 1);

          then (k -polytopes p) = { {} } & (k -polytope-seq p) = <* {} *> by Def5, Def7;

          hence thesis by FINSEQ_1: 38;

        end;

          suppose

           A3: ( - 1) < k & k < ( dim p);

          then (k -polytopes p) = ( rng (F . (k + 1))) by Def5;

          hence thesis by A3, Def7;

        end;

          suppose k = ( dim p);

          then (k -polytopes p) = {p} & (k -polytope-seq p) = <*p*> by Def5, Def7;

          hence thesis by FINSEQ_1: 38;

        end;

      end;

        suppose

         A4: k > ( dim p);

        then (k -polytopes p) = {} by Def5;

        hence thesis by A4, Def7, RELAT_1: 38;

      end;

    end;

    theorem :: POLYFORM:30

    

     Th28: ( num-polytopes (p,( - 1))) = 1

    proof

      reconsider minusone = ( - 1) as Integer;

      (minusone -polytopes p) = { {} } by Def5;

      hence thesis by CARD_1: 30;

    end;

    theorem :: POLYFORM:31

    

     Th29: ( num-polytopes (p,( dim p))) = 1

    proof

      (( dim p) -polytopes p) = {p} by Def5;

      hence thesis by CARD_1: 30;

    end;

    definition

      let p be polyhedron, k be Integer, n be Nat;

      assume

       A1: 1 <= n & n <= ( num-polytopes (p,k));

      :: POLYFORM:def12

      func n -th-polytope (p,k) -> Element of (k -polytopes p) equals

      : Def12: ((k -polytope-seq p) . n);

      coherence

      proof

        n in ( Seg ( num-polytopes (p,k))) by A1;

        then n in ( dom (k -polytope-seq p)) by Th25;

        then ((k -polytope-seq p) . n) in ( rng (k -polytope-seq p)) by FUNCT_1: 3;

        hence thesis by Th27;

      end;

    end

    theorem :: POLYFORM:32

    

     Th30: ( - 1) <= k & k <= ( dim p) implies for x be Element of (k -polytopes p) holds ex n be Nat st x = (n -th-polytope (p,k)) & 1 <= n & n <= ( num-polytopes (p,k))

    proof

      assume

       A1: ( - 1) <= k & k <= ( dim p);

      let x be Element of (k -polytopes p);

      per cases by A1, XXREAL_0: 1;

        suppose

         A2: k = ( - 1);

        reconsider n = 1 as Nat;

        (k -polytope-seq p) = <* {} *> by A2, Def7;

        then

         A3: ((k -polytope-seq p) . n) = {} by FINSEQ_1:def 8;

        take n;

        (k -polytopes p) = { {} } by A2, Def5;

        then x = {} & n <= ( num-polytopes (p,k)) by CARD_1: 30, TARSKI:def 1;

        hence thesis by A3, Def12;

      end;

        suppose

         A4: k = ( dim p);

        reconsider n = 1 as Nat;

        (k -polytope-seq p) = <*p*> by A4, Def7;

        then

         A5: ((k -polytope-seq p) . n) = p by FINSEQ_1:def 8;

        take n;

        (k -polytopes p) = {p} by A4, Def5;

        then x = p & ( num-polytopes (p,k)) = 1 by CARD_1: 30, TARSKI:def 1;

        hence thesis by A5, Def12;

      end;

        suppose

         A6: ( - 1) < k & k < ( dim p);

        set F = the PolytopsF of p;

        

         A7: (k -polytopes p) = ( rng (F . (k + 1))) by A6, Def5;

        

         A8: (( - 1) + 1) < (k + 1) by A6, XREAL_1: 6;

        then

         A9: ( 0 qua Nat + 1) <= (k + 1) by INT_1: 7;

        reconsider k9 = (k + 1) as Element of NAT by A8, INT_1: 3;

        (k + 1) <= ( dim p) by A6, INT_1: 7;

        then (F . k9) is non empty by A9, Def3;

        then

        consider m be object such that

         A10: m in ( dom (F . k9)) and

         A11: ((F . k9) . m) = x by A7, FUNCT_1:def 3;

        reconsider Fk9 = (F . k9) as FinSequence;

        reconsider m as Element of NAT by A10;

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

        then

         A12: 1 <= m & m <= ( len Fk9) by A10, FINSEQ_1: 1;

        take m;

        

         A13: (k -polytope-seq p) = (F . (k + 1)) by A6, Def7;

        then ( num-polytopes (p,k)) = ( len (F . (k + 1))) by Th26;

        hence thesis by A13, A11, A12, Def12;

      end;

    end;

    theorem :: POLYFORM:33

    

     Th31: (k -polytope-seq p) is one-to-one

    proof

      set s = (k -polytope-seq p);

      per cases by XXREAL_0: 1;

        suppose k < ( - 1);

        hence thesis by Def7;

      end;

        suppose k = ( - 1);

        hence thesis by Def7;

      end;

        suppose

         A1: ( - 1) < k & k < ( dim p);

        then

         A2: (( - 1) + 1) < (k + 1) by XREAL_1: 6;

        then

        reconsider m = (k + 1) as Element of NAT by INT_1: 3;

        set F = the PolytopsF of p;

        

         A3: ( 0 qua Nat + 1) <= m by A2, INT_1: 7;

        s = (F . (k + 1)) & m <= ( dim p) by A1, Def7, INT_1: 7;

        hence thesis by A3, Def3;

      end;

        suppose k = ( dim p);

        then s = <*p*> by Def7;

        hence thesis;

      end;

        suppose k > ( dim p);

        hence thesis by Def7;

      end;

    end;

    theorem :: POLYFORM:34

    

     Th32: for m,n be Nat st 1 <= n & n <= ( num-polytopes (p,k)) & 1 <= m & m <= ( num-polytopes (p,k)) & (n -th-polytope (p,k)) = (m -th-polytope (p,k)) holds m = n

    proof

      let m,n be Nat such that

       A1: 1 <= n & n <= ( num-polytopes (p,k)) and

       A2: 1 <= m & m <= ( num-polytopes (p,k)) and

       A3: (n -th-polytope (p,k)) = (m -th-polytope (p,k));

      set s = (k -polytope-seq p);

      

       A4: s is one-to-one by Th31;

      m in ( Seg ( num-polytopes (p,k))) by A2;

      then

       A5: m in ( dom s) by Th25;

      n in ( Seg ( num-polytopes (p,k))) by A1;

      then

       A6: n in ( dom s) by Th25;

      (n -th-polytope (p,k)) = (s . n) & (m -th-polytope (p,k)) = (s . m) by A1, A2, Def12;

      hence thesis by A3, A6, A5, A4, FUNCT_1:def 4;

    end;

    definition

      let p be polyhedron, k be Integer, x be Element of ((k - 1) -polytopes p), y be Element of (k -polytopes p);

      assume that

       A1: 0 <= k and

       A2: k <= ( dim p);

      :: POLYFORM:def13

      func incidence-value (x,y) -> Element of Z_2 equals

      : Def13: (( eta (p,k)) . (x,y));

      coherence

      proof

        set n = ( eta (p,k));

        

         A3: ((k - 1) -polytopes p) <> {}

        proof

          set m = (k - 1);

          ( 0 qua Nat - 1) = ( - 1);

          then

           A4: ( - 1) <= m by A1, XREAL_1: 9;

          m <= (( dim p) - 0 qua Nat) by A2, XREAL_1: 13;

          hence thesis by A4, Th23;

        end;

        ( dom n) = [:((k - 1) -polytopes p), (k -polytopes p):] & (k -polytopes p) <> {} by A1, A2, Th23, FUNCT_2: 92;

        then [x, y] in ( dom n) by A3, ZFMISC_1: 87;

        then (n . [x, y]) in ( rng n) by FUNCT_1: 3;

        hence thesis by BSPACE: 3, BSPACE: 5, BSPACE: 6;

      end;

    end

    begin

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def14

      func k -chain-space (p) -> finite-dimensional VectSp of Z_2 equals ( bspace (k -polytopes p));

      coherence ;

    end

    theorem :: POLYFORM:35

    for x be Element of (k -polytopes p) holds (( 0. (k -chain-space p)) @ x) = ( 0. Z_2 ) by BSPACE: 14;

    theorem :: POLYFORM:36

    

     Th34: ( num-polytopes (p,k)) = ( dim (k -chain-space p))

    proof

      set n = ( dim (k -chain-space p));

      ( singletons (k -polytopes p)) is Basis of (k -chain-space p) by BSPACE: 40;

      then n = ( card ( singletons (k -polytopes p))) by VECTSP_9:def 1;

      hence thesis by BSPACE: 41;

    end;

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def15

      func k -chains (p) -> non empty finite set equals ( bool (k -polytopes p));

      coherence ;

    end

    definition

      let p be polyhedron, k be Integer, x be Element of ((k - 1) -polytopes p), v be Element of (k -chain-space p);

      :: POLYFORM:def16

      func incidence-sequence (x,v) -> FinSequence of Z_2 means

      : Def16: (((k - 1) -polytopes p) is empty implies it = ( <*> {} )) & (((k - 1) -polytopes p) is non empty implies ( len it ) = ( num-polytopes (p,k)) & for n be Nat st 1 <= n & n <= ( num-polytopes (p,k)) holds (it . n) = ((v @ (n -th-polytope (p,k))) * ( incidence-value (x,(n -th-polytope (p,k))))));

      existence

      proof

        per cases ;

          suppose

           A1: ((k - 1) -polytopes p) is empty;

          set s = ( <*> {} );

          ( rng s) c= the carrier of Z_2 ;

          then

          reconsider s as FinSequence of Z_2 by FINSEQ_1:def 4;

          take s;

          thus thesis by A1;

        end;

          suppose

           A2: ((k - 1) -polytopes p) is non empty;

          deffunc F( Nat) = ((v @ ($1 -th-polytope (p,k))) * ( incidence-value (x,($1 -th-polytope (p,k)))));

          consider s be FinSequence of Z_2 such that

           A3: ( len s) = ( num-polytopes (p,k)) and

           A4: for n be Nat st n in ( dom s) holds (s . n) = F(n) from FINSEQ_2:sch 1;

          take s;

          

           A5: ( dom s) = ( Seg ( num-polytopes (p,k))) by A3, FINSEQ_1:def 3;

          for n be Nat st 1 <= n & n <= ( num-polytopes (p,k)) holds (s . n) = ((v @ (n -th-polytope (p,k))) * ( incidence-value (x,(n -th-polytope (p,k)))))

          proof

            let n be Nat;

            assume 1 <= n & n <= ( num-polytopes (p,k));

            then n in ( Seg ( num-polytopes (p,k)));

            hence thesis by A4, A5;

          end;

          hence thesis by A2, A3;

        end;

      end;

      uniqueness

      proof

        let s,t be FinSequence of Z_2 such that

         A6: ((k - 1) -polytopes p) is empty implies s = ( <*> {} ) and

         A7: ((k - 1) -polytopes p) is non empty implies ( len s) = ( num-polytopes (p,k)) & for n be Nat st 1 <= n & n <= ( num-polytopes (p,k)) holds (s . n) = ((v @ (n -th-polytope (p,k))) * ( incidence-value (x,(n -th-polytope (p,k))))) and

         A8: ((k - 1) -polytopes p) is empty implies t = ( <*> {} ) and

         A9: ((k - 1) -polytopes p) is non empty implies ( len t) = ( num-polytopes (p,k)) & for n be Nat st 1 <= n & n <= ( num-polytopes (p,k)) holds (t . n) = ((v @ (n -th-polytope (p,k))) * ( incidence-value (x,(n -th-polytope (p,k)))));

        per cases ;

          suppose ((k - 1) -polytopes p) is empty;

          hence thesis by A6, A8;

        end;

          suppose

           A10: ((k - 1) -polytopes p) is non empty;

          for n be Nat st 1 <= n & n <= ( len s) holds (s . n) = (t . n)

          proof

            let n be Nat such that

             A11: 1 <= n & n <= ( len s);

            reconsider n as Nat;

            (s . n) = ((v @ (n -th-polytope (p,k))) * ( incidence-value (x,(n -th-polytope (p,k))))) by A7, A10, A11;

            hence thesis by A7, A9, A10, A11;

          end;

          hence thesis by A7, A9, A10;

        end;

      end;

    end

    theorem :: POLYFORM:37

    

     Th35: for c,d be Element of (k -chain-space p), x be Element of (k -polytopes p) holds ((c + d) @ x) = ((c @ x) + (d @ x))

    proof

      let c,d be Element of (k -chain-space p), x be Element of (k -polytopes p);

      (c + d) = (c \+\ d) by BSPACE:def 5;

      hence thesis by BSPACE: 15;

    end;

    theorem :: POLYFORM:38

    

     Th36: for c,d be Element of (k -chain-space p), x be Element of ((k - 1) -polytopes p) holds ( incidence-sequence (x,(c + d))) = (( incidence-sequence (x,c)) + ( incidence-sequence (x,d)))

    proof

      let c,d be Element of (k -chain-space p), x be Element of ((k - 1) -polytopes p);

      set n = ( num-polytopes (p,k));

      set l = ( incidence-sequence (x,(c + d)));

      set isc = ( incidence-sequence (x,c));

      set isd = ( incidence-sequence (x,d));

      set r = (isc + isd);

      per cases ;

        suppose

         A1: ((k - 1) -polytopes p) is empty;

        then isd is Tuple of 0 , the carrier of Z_2 by Def16;

        then

        reconsider isd as Element of ( 0 -tuples_on the carrier of Z_2 ) by FINSEQ_2: 131;

        isc = ( <*> the carrier of Z_2 ) by A1, Def16;

        then

        reconsider isc as Element of ( 0 -tuples_on the carrier of Z_2 ) by FINSEQ_2: 131;

        (isc + isd) is Element of ( 0 -tuples_on the carrier of Z_2 );

        hence thesis by A1, Def16;

      end;

        suppose

         A2: ((k - 1) -polytopes p) is non empty;

        

         A3: ( len l) = n & ( len r) = n

        proof

          ( len isd) = n by A2, Def16;

          then

          reconsider isd as Element of (n -tuples_on the carrier of Z_2 ) by FINSEQ_2: 92;

          ( len isc) = n by A2, Def16;

          then

          reconsider isc as Element of (n -tuples_on the carrier of Z_2 ) by FINSEQ_2: 92;

          reconsider s = (isc + isd) as Element of (n -tuples_on the carrier of Z_2 );

          ( len s) = n by CARD_1:def 7;

          hence thesis by A2, Def16;

        end;

        for n be Nat st 1 <= n & n <= ( len l) holds (l . n) = (r . n)

        proof

          

           A4: ( dom r) = ( Seg n) & ( len l) = n by A3, FINSEQ_1:def 3;

          let m be Nat such that

           A5: 1 <= m & m <= ( len l);

          set a = (m -th-polytope (p,k));

          set iva = ( incidence-value (x,a));

          

           A6: ( len l) = n by A2, Def16;

          then

           A7: (l . m) = (((c + d) @ a) * iva) by A2, A5, Def16;

          

           A8: m in ( dom r) by A4, A5;

          (isc . m) = ((c @ a) * iva) & (isd . m) = ((d @ a) * iva) by A2, A5, A6, Def16;

          

          then (r . m) = (((c @ a) * iva) + ((d @ a) * iva)) by A8, FVSUM_1: 17

          .= (((c @ a) + (d @ a)) * iva) by VECTSP_1:def 3

          .= (l . m) by A7, Th35;

          hence thesis;

        end;

        hence thesis by A3;

      end;

    end;

    theorem :: POLYFORM:39

    

     Th37: for c,d be Element of (k -chain-space p), x be Element of ((k - 1) -polytopes p) holds ( Sum (( incidence-sequence (x,c)) + ( incidence-sequence (x,d)))) = (( Sum ( incidence-sequence (x,c))) + ( Sum ( incidence-sequence (x,d))))

    proof

      let c,d be Element of (k -chain-space p), x be Element of ((k - 1) -polytopes p);

      set isc = ( incidence-sequence (x,c));

      set isd = ( incidence-sequence (x,d));

      per cases ;

        suppose

         A1: ((k - 1) -polytopes p) is empty;

        then isd = ( <*> the carrier of Z_2 ) by Def16;

        then

        reconsider isd as Element of ( 0 -tuples_on the carrier of Z_2 ) by FINSEQ_2: 131;

        isc = ( <*> the carrier of Z_2 ) by A1, Def16;

        then

        reconsider isc as Element of ( 0 -tuples_on the carrier of Z_2 ) by FINSEQ_2: 131;

        reconsider s = (isc + isd) as Element of ( 0 -tuples_on the carrier of Z_2 );

        ( Sum s) = ( 0. Z_2 ) by FVSUM_1: 74;

        hence thesis by RLVECT_1:def 4;

      end;

        suppose

         A2: ((k - 1) -polytopes p) is non empty;

        reconsider n = ( num-polytopes (p,k)) as Element of NAT ;

        ( len isd) = n by A2, Def16;

        then

        reconsider isd9 = isd as Element of (n -tuples_on the carrier of Z_2 ) by FINSEQ_2: 92;

        ( len isc) = n by A2, Def16;

        then

        reconsider isc9 = isc as Element of (n -tuples_on the carrier of Z_2 ) by FINSEQ_2: 92;

        ( Sum (isc + isd)) = ( Sum (isc9 + isd9))

        .= (( Sum isc) + ( Sum isd)) by FVSUM_1: 76;

        hence thesis;

      end;

    end;

    theorem :: POLYFORM:40

    

     Th38: for c,d be Element of (k -chain-space p), x be Element of ((k - 1) -polytopes p) holds ( Sum ( incidence-sequence (x,(c + d)))) = (( Sum ( incidence-sequence (x,c))) + ( Sum ( incidence-sequence (x,d))))

    proof

      let c,d be Element of (k -chain-space p), x be Element of ((k - 1) -polytopes p);

      ( Sum ( incidence-sequence (x,(c + d)))) = ( Sum (( incidence-sequence (x,c)) + ( incidence-sequence (x,d)))) by Th36

      .= (( Sum ( incidence-sequence (x,c))) + ( Sum ( incidence-sequence (x,d)))) by Th37;

      hence thesis;

    end;

    theorem :: POLYFORM:41

    

     Th39: for c be Element of (k -chain-space p), a be Element of Z_2 , x be Element of (k -polytopes p) holds ((a * c) @ x) = (a * (c @ x))

    proof

      let c be Element of (k -chain-space p), a be Element of Z_2 , x be Element of (k -polytopes p);

      per cases by BSPACE: 8;

        suppose a = ( 0. Z_2 );

        then (a * (c @ x)) = ( 0. Z_2 ) & (a * c) = ( 0. (k -chain-space p)) by VECTSP_1: 14;

        hence thesis by BSPACE: 14;

      end;

        suppose a = ( 1. Z_2 );

        hence thesis by VECTSP_1:def 17;

      end;

    end;

    theorem :: POLYFORM:42

    

     Th40: for c be Element of (k -chain-space p), a be Element of Z_2 , x be Element of ((k - 1) -polytopes p) holds ( incidence-sequence (x,(a * c))) = (a * ( incidence-sequence (x,c)))

    proof

      let c be Element of (k -chain-space p), a be Element of Z_2 , x be Element of ((k - 1) -polytopes p);

      set l = ( incidence-sequence (x,(a * c)));

      set isc = ( incidence-sequence (x,c));

      set r = (a * isc);

      per cases ;

        suppose

         A1: ((k - 1) -polytopes p) is empty;

        then isc = ( <*> the carrier of Z_2 ) by Def16;

        then

        reconsider isc as Element of ( 0 -tuples_on the carrier of Z_2 ) by FINSEQ_2: 131;

        (a * isc) is Element of ( 0 -tuples_on the carrier of Z_2 );

        then

        reconsider r as Element of ( 0 -tuples_on the carrier of Z_2 );

        r = ( <*> the carrier of Z_2 );

        hence thesis by A1, Def16;

      end;

        suppose

         A2: ((k - 1) -polytopes p) is non empty;

        set n = ( num-polytopes (p,k));

        

         A3: ( len l) = n & ( len r) = n

        proof

          ( len isc) = n by A2, Def16;

          then

          reconsider isc as Element of (n -tuples_on the carrier of Z_2 ) by FINSEQ_2: 92;

          set r = (a * isc);

          reconsider r as Element of (n -tuples_on the carrier of Z_2 );

          ( len r) = n by CARD_1:def 7;

          hence thesis by A2, Def16;

        end;

        for m be Nat st 1 <= m & m <= ( len l) holds (l . m) = (r . m)

        proof

          

           A4: ( dom r) = ( Seg n) by A3, FINSEQ_1:def 3;

          let m be Nat such that

           A5: 1 <= m & m <= ( len l);

          set s = (m -th-polytope (p,k));

          set ivs = ( incidence-value (x,s));

          

           A6: ( len l) = n by A2, Def16;

          then

           A7: (l . m) = (((a * c) @ s) * ivs) by A2, A5, Def16;

          ( len l) = n & m in NAT by A2, Def16, ORDINAL1:def 12;

          then

           A8: m in ( Seg n) by A5;

          (isc . m) = ((c @ s) * ivs) by A2, A5, A6, Def16;

          

          then (r . m) = (a * ((c @ s) * ivs)) by A4, A8, FVSUM_1: 50

          .= ((a * (c @ s)) * ivs) by GROUP_1:def 3

          .= (l . m) by A7, Th39;

          hence thesis;

        end;

        hence thesis by A3;

      end;

    end;

    theorem :: POLYFORM:43

    

     Th41: for c,d be Element of (k -chain-space p) holds c = d iff for x be Element of (k -polytopes p) holds (c @ x) = (d @ x)

    proof

      let c,d be Element of (k -chain-space p);

      thus c = d implies for x be Element of (k -polytopes p) holds (c @ x) = (d @ x);

      thus (for x be Element of (k -polytopes p) holds (c @ x) = (d @ x)) implies c = d

      proof

        assume

         A1: for x be Element of (k -polytopes p) holds (c @ x) = (d @ x);

        thus c c= d

        proof

          let x be object such that

           A2: x in c;

          reconsider x as Element of (k -polytopes p) by A2;

          reconsider c as Subset of (k -polytopes p);

          (c @ x) = ( 1. Z_2 ) by A2, BSPACE:def 3;

          then (d @ x) = ( 1. Z_2 ) by A1;

          hence thesis by BSPACE: 9;

        end;

        thus d c= c

        proof

          let x be object such that

           A3: x in d;

          reconsider x as Element of (k -polytopes p) by A3;

          reconsider d as Subset of (k -polytopes p);

          (d @ x) = ( 1. Z_2 ) by A3, BSPACE:def 3;

          then (c @ x) = ( 1. Z_2 ) by A1;

          hence thesis by BSPACE: 9;

        end;

      end;

    end;

    theorem :: POLYFORM:44

    

     Th42: for c,d be Element of (k -chain-space p) holds c = d iff for x be Element of (k -polytopes p) holds x in c iff x in d

    proof

      let c,d be Element of (k -chain-space p);

      thus c = d implies for x be Element of (k -polytopes p) holds x in c iff x in d;

      thus (for x be Element of (k -polytopes p) holds x in c iff x in d) implies c = d

      proof

        assume

         A1: for x be Element of (k -polytopes p) holds x in c iff x in d;

        assume c <> d;

        then

        consider x be Element of (k -polytopes p) such that

         A2: (c @ x) <> (d @ x) by Th41;

         not (x in c iff x in d) by A2, BSPACE: 13;

        hence thesis by A1;

      end;

    end;

    scheme :: POLYFORM:sch1

    ChainEx { p() -> polyhedron , k() -> Integer , P[ Element of (k() -polytopes p())] } :

ex c be Subset of (k() -polytopes p()) st for x be Element of (k() -polytopes p()) holds x in c iff P[x] & x in (k() -polytopes p());

      set c = { x where x be Element of (k() -polytopes p()) : P[x] & x in (k() -polytopes p()) };

      c c= (k() -polytopes p())

      proof

        let x be object;

        assume x in c;

        then ex y be Element of (k() -polytopes p()) st x = y & P[y] & y in (k() -polytopes p());

        hence thesis;

      end;

      then

      reconsider c as Subset of (k() -polytopes p());

      take c;

      for x be Element of (k() -polytopes p()) holds x in c iff P[x] & x in (k() -polytopes p())

      proof

        let x be Element of (k() -polytopes p());

        thus x in c implies P[x] & x in (k() -polytopes p())

        proof

          assume x in c;

          then ex y be Element of (k() -polytopes p()) st y = x & P[y] & y in (k() -polytopes p());

          hence thesis;

        end;

        thus thesis;

      end;

      hence thesis;

    end;

    definition

      let p be polyhedron, k be Integer, v be Element of (k -chain-space p);

      :: POLYFORM:def17

      func Boundary (v) -> Element of ((k - 1) -chain-space p) means

      : Def17: (((k - 1) -polytopes p) is empty implies it = ( 0. ((k - 1) -chain-space p))) & (((k - 1) -polytopes p) is non empty implies for x be Element of ((k - 1) -polytopes p) holds x in it iff ( Sum ( incidence-sequence (x,v))) = ( 1. Z_2 ));

      existence

      proof

        defpred Q[ Element of ((k - 1) -polytopes p)] means ( Sum ( incidence-sequence ($1,v))) = ( 1. Z_2 );

        consider c be Subset of ((k - 1) -polytopes p) such that

         A1: for x be Element of ((k - 1) -polytopes p) holds x in c iff Q[x] & x in ((k - 1) -polytopes p) from ChainEx;

        reconsider c as Element of ((k - 1) -chain-space p);

        take c;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let c,d be Element of ((k - 1) -chain-space p) such that

         A2: ((k - 1) -polytopes p) is empty implies c = ( 0. ((k - 1) -chain-space p)) and

         A3: ((k - 1) -polytopes p) is non empty implies for x be Element of ((k - 1) -polytopes p) holds x in c iff ( Sum ( incidence-sequence (x,v))) = ( 1. Z_2 ) and ((k - 1) -polytopes p) is empty implies d = ( 0. ((k - 1) -chain-space p)) and

         A4: ((k - 1) -polytopes p) is non empty implies for x be Element of ((k - 1) -polytopes p) holds x in d iff ( Sum ( incidence-sequence (x,v))) = ( 1. Z_2 );

        per cases ;

          suppose ((k - 1) -polytopes p) is empty;

          hence thesis by A2;

        end;

          suppose

           A5: ((k - 1) -polytopes p) is non empty;

          for x be Element of ((k - 1) -polytopes p) holds x in c iff x in d

          proof

            let x be Element of ((k - 1) -polytopes p);

            thus x in c implies x in d

            proof

              assume x in c;

              then ( Sum ( incidence-sequence (x,v))) = ( 1. Z_2 ) by A3;

              hence thesis by A4, A5;

            end;

            thus x in d implies x in c

            proof

              assume x in d;

              then ( Sum ( incidence-sequence (x,v))) = ( 1. Z_2 ) by A4;

              hence thesis by A3, A5;

            end;

          end;

          hence thesis by Th42;

        end;

      end;

    end

    theorem :: POLYFORM:45

    

     Th43: for c be Element of (k -chain-space p), x be Element of ((k - 1) -polytopes p) holds (( Boundary c) @ x) = ( Sum ( incidence-sequence (x,c)))

    proof

      let c be Element of (k -chain-space p), x be Element of ((k - 1) -polytopes p);

      set b = ( Boundary c);

      per cases ;

        suppose

         A1: ((k - 1) -polytopes p) is empty;

        set iscx = ( incidence-sequence (x,c));

        iscx = ( <*> the carrier of Z_2 ) by A1, Def16;

        then

         A2: ( Sum iscx) = ( 0. Z_2 ) by RLVECT_1: 43;

        ( Boundary c) = ( 0. ((k - 1) -chain-space p)) by A1;

        hence thesis by A2, BSPACE: 14;

      end;

        suppose

         A3: ((k - 1) -polytopes p) is non empty;

        then

         A4: x in b iff ( Sum ( incidence-sequence (x,c))) = ( 1. Z_2 ) by Def17;

        per cases ;

          suppose x in b;

          hence thesis by A4, BSPACE:def 3;

        end;

          suppose

           A5: not x in b;

          then ( Sum ( incidence-sequence (x,c))) <> ( 1. Z_2 ) by A3, Def17;

          then ( Sum ( incidence-sequence (x,c))) = ( 0. Z_2 ) by BSPACE: 8;

          hence thesis by A5, BSPACE:def 3;

        end;

      end;

    end;

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def18

      func k -boundary (p) -> Function of (k -chain-space p), ((k - 1) -chain-space p) means

      : Def18: for c be Element of (k -chain-space p) holds (it . c) = ( Boundary c);

      existence

      proof

        defpred Q[ object, object] means ex c be Element of (k -chain-space p) st $1 = c & $2 = ( Boundary c);

        

         A1: for x be object st x in (k -chains p) holds ex y be object st y in ((k - 1) -chains p) & Q[x, y]

        proof

          let x be object;

          assume x in (k -chains p);

          then

          reconsider x as Element of (k -chain-space p);

          set b = ( Boundary x);

          take b;

          thus thesis;

        end;

        consider f be Function of (k -chains p), ((k - 1) -chains p) such that

         A2: for x be object st x in (k -chains p) holds Q[x, (f . x)] from FUNCT_2:sch 1( A1);

        reconsider f as Function of (k -chain-space p), ((k - 1) -chain-space p);

        take f;

        for c be Element of (k -chain-space p) holds (f . c) = ( Boundary c)

        proof

          let c be Element of (k -chain-space p);

           Q[c, (f . c)] by A2;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of (k -chain-space p), ((k - 1) -chain-space p) such that

         A3: for c be Element of (k -chain-space p) holds (f . c) = ( Boundary c) and

         A4: for c be Element of (k -chain-space p) holds (g . c) = ( Boundary c);

        

         A5: for x be object st x in ( dom f) holds (f . x) = (g . x)

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider x as Element of (k -chain-space p);

          (f . x) = ( Boundary x) by A3;

          hence thesis by A4;

        end;

        ( dom f) = ( [#] (k -chain-space p)) by FUNCT_2:def 1;

        then ( dom f) = ( dom g) by FUNCT_2:def 1;

        hence thesis by A5, FUNCT_1: 2;

      end;

    end

    theorem :: POLYFORM:46

    

     Th44: for c,d be Element of (k -chain-space p) holds ( Boundary (c + d)) = (( Boundary c) + ( Boundary d))

    proof

      let c,d be Element of (k -chain-space p);

      set bc = ( Boundary c);

      set bd = ( Boundary d);

      set s = (c + d);

      set l = ( Boundary s);

      set r = (bc + bd);

      for x be Element of ((k - 1) -polytopes p) holds (l @ x) = (r @ x)

      proof

        let x be Element of ((k - 1) -polytopes p);

        set a = (bc @ x);

        set b = (bd @ x);

        

         A1: a = ( Sum ( incidence-sequence (x,c))) & b = ( Sum ( incidence-sequence (x,d))) by Th43;

        (l @ x) = ( Sum ( incidence-sequence (x,s))) & (r @ x) = (a + b) by Th35, Th43;

        hence thesis by A1, Th38;

      end;

      hence thesis by Th41;

    end;

    theorem :: POLYFORM:47

    

     Th45: for a be Element of Z_2 , c be Element of (k -chain-space p) holds ( Boundary (a * c)) = (a * ( Boundary c))

    proof

      let a be Element of Z_2 , c be Element of (k -chain-space p);

      set lsm = (a * c);

      set l = ( Boundary lsm);

      set rb = ( Boundary c);

      set r = (a * rb);

      for x be Element of ((k - 1) -polytopes p) holds (l @ x) = (r @ x)

      proof

        let x be Element of ((k - 1) -polytopes p);

        set b = (rb @ x);

        

         A1: (l @ x) = ( Sum ( incidence-sequence (x,lsm))) & (rb @ x) = ( Sum ( incidence-sequence (x,c))) by Th43;

        (r @ x) = (a * b) & ( incidence-sequence (x,lsm)) = (a * ( incidence-sequence (x,c))) by Th39, Th40;

        hence thesis by A1, FVSUM_1: 73;

      end;

      hence thesis by Th41;

    end;

    theorem :: POLYFORM:48

    

     Th46: (k -boundary p) is linear-transformation of (k -chain-space p), ((k - 1) -chain-space p)

    proof

      set V = (k -chain-space p);

      set b = (k -boundary p);

      

       A1: for a be Element of Z_2 , x be Element of V holds (b . (a * x)) = (a * (b . x))

      proof

        let a be Element of Z_2 , x be Element of V;

        (b . (a * x)) = ( Boundary (a * x)) by Def18

        .= (a * ( Boundary x)) by Th45

        .= (a * (b . x)) by Def18;

        hence thesis;

      end;

      for x,y be Element of V holds (b . (x + y)) = ((b . x) + (b . y))

      proof

        let x,y be Element of V;

        (b . (x + y)) = ( Boundary (x + y)) by Def18

        .= (( Boundary x) + ( Boundary y)) by Th44

        .= ((b . x) + ( Boundary y)) by Def18

        .= ((b . x) + (b . y)) by Def18;

        hence thesis;

      end;

      then b is additive homogeneous by A1, MOD_2:def 2, VECTSP_1:def 20;

      hence thesis;

    end;

    registration

      let p be polyhedron, k be Integer;

      cluster (k -boundary p) -> homogeneous additive;

      coherence by Th46;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def19

      func k -circuit-space (p) -> Subspace of (k -chain-space p) equals ( ker (k -boundary p));

      coherence ;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def20

      func k -circuits (p) -> non empty Subset of (k -chains p) equals ( [#] (k -circuit-space p));

      coherence by VECTSP_4:def 2;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def21

      func k -bounding-chain-space (p) -> Subspace of (k -chain-space p) equals ( im ((k + 1) -boundary p));

      coherence ;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def22

      func k -bounding-chains (p) -> non empty Subset of (k -chains p) equals ( [#] (k -bounding-chain-space p));

      coherence by VECTSP_4:def 2;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def23

      func k -bounding-circuit-space (p) -> Subspace of (k -chain-space p) equals ((k -bounding-chain-space p) /\ (k -circuit-space p));

      coherence ;

    end

    definition

      let p be polyhedron, k be Integer;

      :: POLYFORM:def24

      func k -bounding-circuits (p) -> non empty Subset of (k -chains p) equals ( [#] (k -bounding-circuit-space p));

      coherence by VECTSP_4:def 2;

    end

    theorem :: POLYFORM:49

    ( dim (k -chain-space p)) = (( rank (k -boundary p)) + ( nullity (k -boundary p))) by RANKNULL: 44;

    begin

    definition

      let p be polyhedron;

      :: POLYFORM:def25

      attr p is simply-connected means for k be Integer holds (k -circuits p) = (k -bounding-chains p);

    end

    theorem :: POLYFORM:50

    

     Th48: p is simply-connected iff for n be Integer holds (n -circuit-space p) = (n -bounding-chain-space p)

    proof

      defpred Q[ polyhedron] means for n be Integer holds (n -circuit-space $1) = (n -bounding-chain-space $1);

      thus p is simply-connected implies Q[p]

      proof

        assume

         A1: p is simply-connected;

        let n be Integer;

        (n -circuits p) = (n -bounding-chains p) by A1;

        hence thesis by VECTSP_4: 29;

      end;

      thus Q[p] implies p is simply-connected;

    end;

    definition

      let p be polyhedron;

      :: POLYFORM:def26

      func alternating-f-vector (p) -> FinSequence of INT means

      : Def26: ( len it ) = (( dim p) + 2) & for k be Nat st 1 <= k & k <= (( dim p) + 2) holds (it . k) = ((( - 1) |^ k) * ( num-polytopes (p,(k - 2))));

      existence

      proof

        deffunc F( Nat) = ( In (((( - 1) |^ $1) * ( num-polytopes (p,($1 - 2)))), INT ));

        consider s be FinSequence of INT such that

         A1: ( len s) = (( dim p) + 2) and

         A2: for j be Nat st j in ( dom s) holds (s . j) = F(j) from FINSEQ_2:sch 1;

        take s;

        for j be Nat st 1 <= j & j <= (( dim p) + 2) holds (s . j) = ((( - 1) |^ j) * ( num-polytopes (p,(j - 2))))

        proof

          let j be Nat;

          assume 1 <= j & j <= (( dim p) + 2);

          then j in ( dom s) by A1, FINSEQ_3: 25;

          then (s . j) = F(j) by A2;

          hence thesis;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let s,t be FinSequence of INT such that

         A3: ( len s) = (( dim p) + 2) and

         A4: for k be Nat st 1 <= k & k <= (( dim p) + 2) holds (s . k) = ((( - 1) |^ k) * ( num-polytopes (p,(k - 2)))) and

         A5: ( len t) = (( dim p) + 2) and

         A6: for k be Nat st 1 <= k & k <= (( dim p) + 2) holds (t . k) = ((( - 1) |^ k) * ( num-polytopes (p,(k - 2))));

        for k be Nat st 1 <= k & k <= ( len s) holds (s . k) = (t . k)

        proof

          let k be Nat such that

           A7: 1 <= k & k <= ( len s);

          reconsider k as Nat;

          (s . k) = ((( - 1) |^ k) * ( num-polytopes (p,(k - 2)))) by A3, A4, A7;

          hence thesis by A3, A6, A7;

        end;

        hence thesis by A3, A5;

      end;

    end

    definition

      let p be polyhedron;

      :: POLYFORM:def27

      func alternating-proper-f-vector (p) -> FinSequence of INT means

      : Def27: ( len it ) = ( dim p) & for k be Nat st 1 <= k & k <= ( dim p) holds (it . k) = ((( - 1) |^ (k + 1)) * ( num-polytopes (p,(k - 1))));

      existence

      proof

        deffunc F( Nat) = ( In (((( - 1) |^ ($1 + 1)) * ( num-polytopes (p,($1 - 1)))), INT ));

        consider s be FinSequence of INT such that

         A1: ( len s) = ( dim p) and

         A2: for j be Nat st j in ( dom s) holds (s . j) = F(j) from FINSEQ_2:sch 1;

        take s;

        for j be Nat st 1 <= j & j <= ( dim p) holds (s . j) = ((( - 1) |^ (j + 1)) * ( num-polytopes (p,(j - 1))))

        proof

          let j be Nat;

          assume 1 <= j & j <= ( dim p);

          then j in ( dom s) by A1, FINSEQ_3: 25;

          then (s . j) = F(j) by A2;

          hence thesis;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let s,t be FinSequence of INT such that

         A3: ( len s) = ( dim p) and

         A4: for k be Nat st 1 <= k & k <= ( dim p) holds (s . k) = ((( - 1) |^ (k + 1)) * ( num-polytopes (p,(k - 1)))) and

         A5: ( len t) = ( dim p) and

         A6: for k be Nat st 1 <= k & k <= ( dim p) holds (t . k) = ((( - 1) |^ (k + 1)) * ( num-polytopes (p,(k - 1))));

        for k be Nat st 1 <= k & k <= ( len s) holds (s . k) = (t . k)

        proof

          let k be Nat such that

           A7: 1 <= k & k <= ( len s);

          reconsider k as Nat;

          (s . k) = ((( - 1) |^ (k + 1)) * ( num-polytopes (p,(k - 1)))) by A3, A4, A7;

          hence thesis by A3, A6, A7;

        end;

        hence thesis by A3, A5;

      end;

    end

    definition

      let p be polyhedron;

      :: POLYFORM:def28

      func alternating-semi-proper-f-vector (p) -> FinSequence of INT means

      : Def28: ( len it ) = (( dim p) + 1) & for k be Nat st 1 <= k & k <= (( dim p) + 1) holds (it . k) = ((( - 1) |^ (k + 1)) * ( num-polytopes (p,(k - 1))));

      existence

      proof

        deffunc F( Nat) = ( In (((( - 1) |^ ($1 + 1)) * ( num-polytopes (p,($1 - 1)))), INT ));

        consider s be FinSequence of INT such that

         A1: ( len s) = (( dim p) + 1) and

         A2: for j be Nat st j in ( dom s) holds (s . j) = F(j) from FINSEQ_2:sch 1;

        take s;

        for j be Nat st 1 <= j & j <= (( dim p) + 1) holds (s . j) = ((( - 1) |^ (j + 1)) * ( num-polytopes (p,(j - 1))))

        proof

          let j be Nat;

          assume 1 <= j & j <= (( dim p) + 1);

          then j in ( dom s) by A1, FINSEQ_3: 25;

          then (s . j) = F(j) by A2;

          hence thesis;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let s,t be FinSequence of INT such that

         A3: ( len s) = (( dim p) + 1) and

         A4: for k be Nat st 1 <= k & k <= (( dim p) + 1) holds (s . k) = ((( - 1) |^ (k + 1)) * ( num-polytopes (p,(k - 1)))) and

         A5: ( len t) = (( dim p) + 1) and

         A6: for k be Nat st 1 <= k & k <= (( dim p) + 1) holds (t . k) = ((( - 1) |^ (k + 1)) * ( num-polytopes (p,(k - 1))));

        for k be Nat st 1 <= k & k <= ( len s) holds (s . k) = (t . k)

        proof

          let k be Nat such that

           A7: 1 <= k & k <= ( len s);

          reconsider k as Nat;

          (s . k) = ((( - 1) |^ (k + 1)) * ( num-polytopes (p,(k - 1)))) by A3, A4, A7;

          hence thesis by A3, A6, A7;

        end;

        hence thesis by A3, A5;

      end;

    end

    theorem :: POLYFORM:51

    

     Th49: 1 <= n & n <= ( len ( alternating-proper-f-vector p)) implies (( alternating-proper-f-vector p) . n) = (((( - 1) |^ (n + 1)) * ( dim ((n - 2) -bounding-chain-space p))) + ((( - 1) |^ (n + 1)) * ( dim ((n - 1) -circuit-space p))))

    proof

      set apcs = ( alternating-proper-f-vector p);

      assume

       A1: 1 <= n;

      set a = (( - 1) |^ (n + 1));

      assume n <= ( len apcs);

      then n <= ( dim p) by Def27;

      

      then (apcs . n) = (a * ( num-polytopes (p,(n - 1)))) by A1, Def27

      .= (a * ( dim ((n - 1) -chain-space p))) by Th34

      .= (a * (( rank ((n - 1) -boundary p)) + ( nullity ((n - 1) -boundary p)))) by RANKNULL: 44

      .= ((a * ( dim ((n - 2) -bounding-chain-space p))) + (a * ( dim ((n - 1) -circuit-space p))));

      hence thesis;

    end;

    definition

      let p be polyhedron;

      :: POLYFORM:def29

      attr p is eulerian means ( Sum ( alternating-proper-f-vector p)) = (1 + (( - 1) |^ (( dim p) + 1)));

    end

    theorem :: POLYFORM:52

    

     Th50: ( alternating-semi-proper-f-vector p) = (( alternating-proper-f-vector p) ^ <*(( - 1) |^ ( dim p))*>)

    proof

      set d = ( dim p);

      set aspcs = ( alternating-semi-proper-f-vector p);

      set apcs = ( alternating-proper-f-vector p);

      set r = (apcs ^ <*(( - 1) |^ ( dim p))*>);

      

       A1: ( len aspcs) = (d + 1) by Def28;

      

       A2: for n be Nat st 1 <= n & n <= ( len aspcs) holds (aspcs . n) = (r . n)

      proof

        let n be Nat such that

         A3: 1 <= n and

         A4: n <= ( len aspcs);

        per cases by A1, A4, NAT_1: 8;

          suppose

           A5: n <= d;

          ( len apcs) = d & ( dom apcs) = ( Seg ( len apcs)) by Def27, FINSEQ_1:def 3;

          then n in ( dom apcs) by A3, A5;

          

          then (r . n) = (apcs . n) by FINSEQ_1:def 7

          .= ((( - 1) |^ (n + 1)) * ( num-polytopes (p,(n - 1)))) by A3, A5, Def27;

          hence thesis by A1, A3, A4, Def28;

        end;

          suppose

           A6: n = (d + 1);

          then n = (( len apcs) + 1) by Def27;

          

          then

           A7: (r . n) = (( - 1) |^ d) by FINSEQ_1: 42

          .= (( - 1) |^ (d + 2)) by Th12;

          (aspcs . n) = ((( - 1) |^ (n + 1)) * ( num-polytopes (p,(n - 1)))) by A3, A6, Def28

          .= ((( - 1) |^ (n + 1)) * 1) by A6, Th29

          .= (( - 1) |^ (n + 1));

          hence thesis by A6, A7;

        end;

      end;

      ( len r) = (( len apcs) + ( len <*(( - 1) |^ ( dim p))*>)) by FINSEQ_1: 22

      .= (d + ( len <*(( - 1) |^ ( dim p))*>)) by Def27

      .= (d + 1) by FINSEQ_1: 40;

      then ( len aspcs) = ( len r) by Def28;

      hence thesis by A2;

    end;

    definition

      let p be polyhedron;

      :: original: eulerian

      redefine

      :: POLYFORM:def30

      attr p is eulerian means ( Sum ( alternating-semi-proper-f-vector p)) = 1;

      compatibility

      proof

        set aspcs = ( alternating-semi-proper-f-vector p);

        set apcs = ( alternating-proper-f-vector p);

        aspcs = (apcs ^ <*(( - 1) |^ ( dim p))*>) by Th50;

        then

         A1: ( Sum aspcs) = (( Sum apcs) + (( - 1) |^ ( dim p))) by RVSUM_1: 74;

        

         A2: ( Sum aspcs) = 1 implies p is eulerian

        proof

          assume ( Sum aspcs) = 1;

          

          then ( Sum apcs) = (1 + (( - 1) * (( - 1) |^ ( dim p)))) by A1

          .= (1 + (( - 1) |^ (( dim p) + 1))) by NEWTON: 6;

          hence thesis;

        end;

        p is eulerian implies ( Sum aspcs) = 1

        proof

          assume p is eulerian;

          

          then ( Sum aspcs) = ((1 + (( - 1) |^ (( dim p) + 1))) + (( - 1) |^ ( dim p))) by A1

          .= ((1 + (( - 1) * (( - 1) |^ ( dim p)))) + (( - 1) |^ ( dim p))) by NEWTON: 6

          .= 1;

          hence thesis;

        end;

        hence thesis by A2;

      end;

    end

    theorem :: POLYFORM:53

    

     Th51: ( alternating-f-vector p) = ( <*( - 1)*> ^ ( alternating-semi-proper-f-vector p))

    proof

      set acs = ( alternating-f-vector p);

      set aspcs = ( alternating-semi-proper-f-vector p);

      set d = ( dim p);

      set r = ( <*( - 1)*> ^ aspcs);

      

       A1: ( len r) = (( len <*( - 1)*>) + ( len aspcs)) by FINSEQ_1: 22

      .= (( len <*( - 1)*>) + (d + 1)) by Def28

      .= (1 + (d + 1)) by FINSEQ_1: 40

      .= (d + 2);

      

       A2: for n be Nat st 1 <= n & n <= ( len acs) holds (acs . n) = (r . n)

      proof

        let n be Nat such that

         A3: 1 <= n and

         A4: n <= ( len acs);

        

         A5: n <= (d + 2) by A4, Def26;

        per cases by A3, XXREAL_0: 1;

          suppose

           A6: n = 1;

          

          then (acs . n) = ((( - 1) |^ 1) * ( num-polytopes (p,(1 - 2)))) by A5, Def26

          .= (( - 1) * ( num-polytopes (p,( - 1))))

          .= (( - 1) * 1) by Th28

          .= ( - 1);

          hence thesis by A6, FINSEQ_1: 41;

        end;

          suppose

           A7: n > 1;

          then

           A8: (1 - 1) < (n - 1) by XREAL_1: 9;

          then

          reconsider m = (n - 1) as Element of NAT by INT_1: 3;

          (n - 1) <= ((d + 2) - 1) by A5, XREAL_1: 9;

          then

           A9: m <= (d + 1);

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

          then

           A10: (r . n) = (aspcs . (n - 1)) by A1, A5, A7, FINSEQ_1: 24;

           0 < ( 0 qua Nat + m) by A8;

          then 1 <= m by NAT_1: 19;

          

          then (aspcs . m) = ((( - 1) |^ (m + 1)) * ( num-polytopes (p,(m - 1)))) by A9, Def28

          .= ((( - 1) |^ n) * ( num-polytopes (p,(n - 2))));

          hence thesis by A3, A5, A10, Def26;

        end;

      end;

      ( len acs) = ( len r) by A1, Def26;

      hence thesis by A2;

    end;

    definition

      let p be polyhedron;

      :: original: eulerian

      redefine

      :: POLYFORM:def31

      attr p is eulerian means ( Sum ( alternating-f-vector p)) = 0 ;

      compatibility

      proof

        set aspcs = ( alternating-semi-proper-f-vector p);

        set acs = ( alternating-f-vector p);

        acs = ( <*( - 1)*> ^ aspcs) by Th51;

        then

         A1: ( Sum acs) = (( - 1) + ( Sum aspcs)) by Th18;

        thus thesis by A1;

      end;

    end

    begin

    theorem :: POLYFORM:54

    

     Th52: ( 0 -polytopes p) is non empty

    proof

      set d = ( dim p);

      per cases ;

        suppose d = 0 ;

        then ( 0 -polytopes p) = {p} by Def5;

        hence thesis;

      end;

        suppose d > 0 ;

        hence thesis by Th23;

      end;

    end;

    theorem :: POLYFORM:55

    

     Th53: ( card ( [#] (( - 1) -chain-space p))) = 2

    proof

      (( - 1) -polytopes p) = { {} } by Def5;

      then ( card (( - 1) -polytopes p)) = 1 by CARD_1: 30;

      

      then ( card ( [#] (( - 1) -chain-space p))) = ( exp (2,1)) by BSPACE: 42

      .= 2 by CARD_2: 27;

      hence thesis;

    end;

    theorem :: POLYFORM:56

    

     Th54: ( [#] (( - 1) -chain-space p)) = { {} , { {} }}

    proof

      (( - 1) -polytopes p) = { {} } by Def5;

      hence thesis by ZFMISC_1: 24;

    end;

    theorem :: POLYFORM:57

    

     Th55: for x be Element of (k -polytopes p), e be Element of ((k - 1) -polytopes p) st k = 0 & e = {} holds ( incidence-value (e,x)) = ( 1. Z_2 )

    proof

      let x be Element of (k -polytopes p), e be Element of ((k - 1) -polytopes p) such that

       A1: k = 0 and

       A2: e = {} ;

      

       A3: ( eta (p,k)) = ( [: { {} }, ( 0 -polytopes p):] --> ( 1. Z_2 )) by A1, Def6;

      

       A4: k <= ( dim p) by A1;

      then {} in { {} } & ( 0 -polytopes p) is non empty by Th23, TARSKI:def 1;

      then

       A5: [ {} , x] in [: { {} }, ( 0 -polytopes p):] by A1, ZFMISC_1: 87;

      ( incidence-value (e,x)) = (( eta (p,k)) . (e,x)) by A1, A4, Def13

      .= ( 1. Z_2 ) by A2, A3, A5, FUNCOP_1: 7;

      hence thesis;

    end;

    theorem :: POLYFORM:58

    

     Th56: for k be Integer, x be Element of (k -polytopes p), v be Element of (k -chain-space p), e be Element of ((k - 1) -polytopes p), n be Nat st k = 0 & v = {x} & e = {} & x = (n -th-polytope (p,k)) & 1 <= n & n <= ( num-polytopes (p,k)) holds (( incidence-sequence (e,v)) . n) = ( 1. Z_2 )

    proof

      let k be Integer, x be Element of (k -polytopes p), v be Element of (k -chain-space p), e be Element of ((k - 1) -polytopes p), n be Nat such that

       A1: k = 0 and

       A2: v = {x} and

       A3: e = {} and

       A4: x = (n -th-polytope (p,k)) & 1 <= n & n <= ( num-polytopes (p,k));

      set iseq = ( incidence-sequence (e,v));

      

       A5: x in v by A2, TARSKI:def 1;

      ((k - 1) -polytopes p) is non empty by A1, Def5;

      

      then (iseq . n) = ((v @ x) * ( incidence-value (e,x))) by A4, Def16

      .= (( 1. Z_2 ) * ( incidence-value (e,x))) by A5, BSPACE:def 3

      .= (( 1. Z_2 ) * ( 1. Z_2 )) by A1, A3, Th55

      .= ( 1. Z_2 );

      hence thesis;

    end;

    theorem :: POLYFORM:59

    

     Th57: for k be Integer, x be Element of (k -polytopes p), e be Element of ((k - 1) -polytopes p), v be Element of (k -chain-space p), m,n be Nat st k = 0 & v = {x} & x = (n -th-polytope (p,k)) & 1 <= m & m <= ( num-polytopes (p,k)) & 1 <= n & n <= ( num-polytopes (p,k)) & m <> n holds (( incidence-sequence (e,v)) . m) = ( 0. Z_2 )

    proof

      let k be Integer, x be Element of (k -polytopes p), e be Element of ((k - 1) -polytopes p), v be Element of (k -chain-space p), m,n be Nat such that

       A1: k = 0 and

       A2: v = {x} and

       A3: x = (n -th-polytope (p,k)) and

       A4: 1 <= m & m <= ( num-polytopes (p,k)) and

       A5: 1 <= n & n <= ( num-polytopes (p,k)) & m <> n;

      

       A6: (m -th-polytope (p,k)) <> x by A3, A4, A5, Th32;

      now

        assume (v @ (m -th-polytope (p,k))) = ( 1. Z_2 );

        then (m -th-polytope (p,k)) in {x} by A2, BSPACE: 9;

        hence contradiction by A6, TARSKI:def 1;

      end;

      then

       A7: (v @ (m -th-polytope (p,k))) = ( 0. Z_2 ) by BSPACE: 11;

      set iseq = ( incidence-sequence (e,v));

      ((k - 1) -polytopes p) is non empty by A1, Def5;

      

      then (iseq . m) = (( 0. Z_2 ) * ( incidence-value (e,(m -th-polytope (p,k))))) by A4, A7, Def16

      .= ( 0. Z_2 );

      hence thesis;

    end;

    theorem :: POLYFORM:60

    

     Th58: for k be Integer, x be Element of (k -polytopes p), v be Element of (k -chain-space p), e be Element of ((k - 1) -polytopes p) st k = 0 & v = {x} & e = {} holds ( Sum ( incidence-sequence (e,v))) = ( 1. Z_2 )

    proof

      let k be Integer, x be Element of (k -polytopes p), v be Element of (k -chain-space p), e be Element of ((k - 1) -polytopes p) such that

       A1: k = 0 and

       A2: v = {x} and

       A3: e = {} ;

      set iseq = ( incidence-sequence (e,v));

      k <= ( dim p) by A1;

      then

      consider n be Nat such that

       A4: x = (n -th-polytope (p,k)) and

       A5: 1 <= n & n <= ( num-polytopes (p,k)) by A1, Th30;

      ((k - 1) -polytopes p) is non empty by A1, Def5;

      then

       A6: ( len iseq) = ( num-polytopes (p,k)) by Def16;

      

       A7: for m be Nat st m in ( dom iseq) & m <> n holds (iseq . m) = ( 0. Z_2 )

      proof

        let m be Nat such that

         A8: m in ( dom iseq) and

         A9: m <> n;

        m in ( Seg ( len iseq)) by A8, FINSEQ_1:def 3;

        then 1 <= m & m <= ( len iseq) by FINSEQ_1: 1;

        hence thesis by A1, A2, A4, A5, A6, A9, Th57;

      end;

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

      then

       A10: n in ( dom iseq) by A5, A6;

      (iseq . n) = ( 1. Z_2 ) by A1, A2, A3, A4, A5, Th56;

      hence thesis by A10, A7, MATRIX_3: 12;

    end;

    theorem :: POLYFORM:61

    

     Th59: for x be Element of ( 0 -polytopes p) holds (( 0 -boundary p) . {x}) = { {} }

    proof

      reconsider minusone = ( 0 qua Nat - 1) as Integer;

      let x be Element of ( 0 -polytopes p);

      set T = ( 0 -boundary p);

      ( 0 -polytopes p) is non empty by Th52;

      then

      reconsider v = {x} as Subset of ( 0 -polytopes p) by ZFMISC_1: 31;

      (( 0 qua Nat - 1) -polytopes p) = { {} } by Def5;

      then

      reconsider null = {} as Element of (( 0 qua Nat - 1) -polytopes p) by TARSKI:def 1;

      reconsider v as Element of ( 0 -chain-space p);

      reconsider bv = ( Boundary v) as Element of (minusone -chain-space p);

      

       A1: bv c= {null}

      proof

        

         A2: ( [#] (minusone -chain-space p)) = { {} , { {} }} by Th54;

        let y be object such that

         A3: y in bv;

        per cases by A2, TARSKI:def 2;

          suppose bv = {} ;

          hence thesis by A3;

        end;

          suppose bv = { {} };

          hence thesis by A3;

        end;

      end;

      (minusone -polytopes p) is non empty by Def5;

      then null in bv iff ( Sum ( incidence-sequence (null,v))) = ( 1. Z_2 ) by Def17;

      then

       A4: {null} c= bv by Th58, ZFMISC_1: 31;

      (T . v) = ( Boundary v) by Def18;

      hence thesis by A4, A1;

    end;

    theorem :: POLYFORM:62

    

     Th60: k = ( - 1) implies ( dim (k -bounding-chain-space p)) = 1

    proof

      set T = ( 0 -boundary p);

      set V = (k -bounding-chain-space p);

      assume

       A1: k = ( - 1);

      ( card ( [#] V)) = 2

      proof

        ( [#] V) c= ( [#] (k -chain-space p)) by VECTSP_4:def 2;

        then ( card ( [#] V)) c= ( card ( [#] (k -chain-space p))) by CARD_1: 11;

        then

         A2: ( card ( [#] V)) c= 2 by A1, Th53;

        ( 0 -polytopes p) <> {} by Th52;

        then

        consider x be object such that

         A3: x in ( 0 -polytopes p) by XBOOLE_0:def 1;

        reconsider x as Element of ( 0 -polytopes p) by A3;

        set v = {x};

        

         A4: (T . v) = { {} } by Th59;

        reconsider v as Subset of ( 0 -polytopes p) by A3, ZFMISC_1: 31;

        reconsider v as Element of ( 0 -chain-space p);

        

         A5: ( dom T) = ( [#] ( 0 -chain-space p)) by RANKNULL: 7;

        then v in ( dom T);

        then

         A6: { {} } in ( rng T) by A4, FUNCT_1: 3;

        (T . ( 0. ( 0 -chain-space p))) = ( 0. (k -chain-space p)) by A1, RANKNULL: 9

        .= {} ;

        then {} in ( rng T) by A5, FUNCT_1: 3;

        then

         A7: { {} , { {} }} c= ( rng T) by A6, ZFMISC_1: 32;

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

        then

         A8: 2 c= ( card ( rng T)) by A7, CARD_1: 11;

        ( card ( rng T)) = ( card (T .: ( [#] ( 0 -chain-space p)))) by RELSET_1: 22

        .= ( card ( [#] V)) by A1, RANKNULL:def 2;

        hence thesis by A8, A2;

      end;

      hence thesis by RANKNULL: 6;

    end;

    theorem :: POLYFORM:63

    

     Th61: ( card ( [#] (( dim p) -chain-space p))) = 2

    proof

      (( dim p) -polytopes p) = {p} by Def5;

      then ( card (( dim p) -polytopes p)) = 1 by CARD_1: 30;

      

      then ( card ( [#] (( dim p) -chain-space p))) = ( exp (2,1)) by BSPACE: 42

      .= 2 by CARD_2: 27;

      hence thesis;

    end;

    theorem :: POLYFORM:64

    

     Th62: {p} is Element of (( dim p) -chain-space p)

    proof

      (( dim p) -polytopes p) = {p} by Def5;

      hence thesis;

    end;

    theorem :: POLYFORM:65

    

     Th63: {p} in ( [#] (( dim p) -chain-space p))

    proof

       {p} is Element of (( dim p) -chain-space p) by Th62;

      hence thesis;

    end;

    theorem :: POLYFORM:66

    

     Th64: ((( dim p) - 1) -polytopes p) is non empty

    proof

      set n = (( dim p) - 1);

      ( 0 qua Nat - 1) = ( - 1);

      then

       A1: ( - 1) <= n by XREAL_1: 9;

      n <= ( dim p) by XREAL_1: 146;

      hence thesis by A1, Th23;

    end;

    registration

      let p be polyhedron;

      cluster ((( dim p) - 1) -polytopes p) -> non empty;

      coherence by Th64;

    end

    theorem :: POLYFORM:67

    

     Th65: ( [#] (( dim p) -chain-space p)) = {( 0. (( dim p) -chain-space p)), {p}}

    proof

      set V = (( dim p) -chain-space p);

      set C = ( [#] V);

      

       A1: ( card C) = 2 by Th61;

      reconsider C as finite set;

      

       A2: {p} in C by Th63;

      ex a,b be object st a <> b & C = {a, b} by A1, CARD_2: 60;

      hence thesis by A2, Th1;

    end;

    theorem :: POLYFORM:68

    

     Th66: for x be Element of (( dim p) -chain-space p) holds x = ( 0. (( dim p) -chain-space p)) or x = {p}

    proof

      set V = (( dim p) -chain-space p);

      let x be Element of V;

      x in ( [#] V);

      then x in {( 0. V), {p}} by Th65;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: POLYFORM:69

    

     Th67: for x,y be Element of (( dim p) -chain-space p) st x <> y holds x = ( 0. (( dim p) -chain-space p)) or y = ( 0. (( dim p) -chain-space p))

    proof

      set V = (( dim p) -chain-space p);

      let x,y be Element of V such that

       A1: x <> y;

      assume x <> ( 0. V);

      then

       A2: x = {p} by Th66;

      assume y <> ( 0. V);

      hence contradiction by A1, A2, Th66;

    end;

    theorem :: POLYFORM:70

    (( dim p) -polytope-seq p) = <*p*> by Def7;

    theorem :: POLYFORM:71

    

     Th69: (1 -th-polytope (p,( dim p))) = p

    proof

      reconsider egy = 1 as Nat;

      set s = (( dim p) -polytope-seq p);

      

       A1: s = <*p*> by Def7;

      egy <= ( num-polytopes (p,( dim p))) by Th29;

      

      then (egy -th-polytope (p,( dim p))) = (s . egy) by Def12

      .= p by A1, FINSEQ_1: 40;

      hence thesis;

    end;

    theorem :: POLYFORM:72

    

     Th70: for c be Element of (( dim p) -chain-space p), x be Element of (( dim p) -polytopes p) st c = {p} holds (c @ x) = ( 1. Z_2 )

    proof

      

       A1: (( dim p) -polytopes p) = {p} by Def5;

      let c be Element of (( dim p) -chain-space p), x be Element of (( dim p) -polytopes p);

      assume c = {p};

      hence thesis by A1, BSPACE:def 3;

    end;

    theorem :: POLYFORM:73

    

     Th71: for x be Element of ((( dim p) - 1) -polytopes p), c be Element of (( dim p) -polytopes p) st c = p holds ( incidence-value (x,c)) = ( 1. Z_2 )

    proof

      set f = ( [:((( dim p) - 1) -polytopes p), {p}:] --> ( 1. Z_2 ));

      let x be Element of ((( dim p) - 1) -polytopes p), c be Element of (( dim p) -polytopes p);

      assume c = p;

      then ( dom f) = [:((( dim p) - 1) -polytopes p), {p}:] & c in {p} by TARSKI:def 1;

      then [x, c] in ( dom f) by ZFMISC_1: 87;

      then (f . (x,c)) in ( rng f) by FUNCT_1: 3;

      then (f . (x,c)) in {( 1. Z_2 )} by FUNCOP_1: 8;

      then

       A1: (f . (x,c)) = ( 1. Z_2 ) by TARSKI:def 1;

      ( eta (p,( dim p))) = f by Def6;

      hence thesis by A1, Def13;

    end;

    theorem :: POLYFORM:74

    

     Th72: for x be Element of ((( dim p) - 1) -polytopes p), c be Element of (( dim p) -chain-space p) st c = {p} holds ( incidence-sequence (x,c)) = <*( 1. Z_2 )*>

    proof

      let x be Element of ((( dim p) - 1) -polytopes p), c be Element of (( dim p) -chain-space p) such that

       A1: c = {p};

      set iseq = ( incidence-sequence (x,c));

      

       A2: (iseq . 1) = ( 1. Z_2 )

      proof

        reconsider egy = 1 as Nat;

        set z = (egy -th-polytope (p,( dim p)));

        egy <= ( num-polytopes (p,( dim p))) by Th29;

        then

         A3: (iseq . egy) = ((c @ z) * ( incidence-value (x,z))) by Def16;

        (c @ z) = ( 1. Z_2 ) & ( incidence-value (x,z)) = ( 1. Z_2 ) by A1, Th69, Th70, Th71;

        hence thesis by A3;

      end;

      ( num-polytopes (p,( dim p))) = 1 by Th29;

      then ( len iseq) = 1 by Def16;

      hence thesis by A2, FINSEQ_1: 40;

    end;

    theorem :: POLYFORM:75

    

     Th73: for x be Element of ((( dim p) - 1) -polytopes p), c be Element of (( dim p) -chain-space p) st c = {p} holds ( Sum ( incidence-sequence (x,c))) = ( 1. Z_2 )

    proof

      let x be Element of ((( dim p) - 1) -polytopes p), c be Element of (( dim p) -chain-space p);

      assume c = {p};

      then ( incidence-sequence (x,c)) = <*( 1. Z_2 )*> by Th72;

      hence thesis by FINSOP_1: 11;

    end;

    theorem :: POLYFORM:76

    

     Th74: ((( dim p) -boundary p) . {p}) = ((( dim p) - 1) -polytopes p)

    proof

      reconsider c = {p} as Element of (( dim p) -chain-space p) by Th62;

      set T = (( dim p) -boundary p);

      set X = ((( dim p) - 1) -polytopes p);

      reconsider d = X as Element of ((( dim p) - 1) -chain-space p) by ZFMISC_1:def 1;

      reconsider Tc = (T . c) as Element of ((( dim p) - 1) -chain-space p);

      for x be Element of X holds x in Tc iff x in d

      proof

        let x be Element of X;

        thus x in Tc implies x in d;

        thus x in d implies x in Tc

        proof

          assume x in d;

          ( Sum ( incidence-sequence (x,c))) = ( 1. Z_2 ) by Th73;

          then x in ( Boundary c) by Def17;

          hence thesis by Def18;

        end;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: POLYFORM:77

    

     Th75: (( dim p) -boundary p) is one-to-one

    proof

      set T = (( dim p) -boundary p);

      set U = ((( dim p) - 1) -chain-space p);

      set V = (( dim p) -chain-space p);

      set B = {p};

      assume not T is one-to-one;

      then

      consider x1,x2 be object such that

       A1: x1 in ( dom T) and

       A2: x2 in ( dom T) and

       A3: (T . x1) = (T . x2) and

       A4: x1 <> x2 by FUNCT_1:def 4;

      reconsider x2 as Element of V by A2;

      reconsider x1 as Element of V by A1;

      per cases by A4, Th67;

        suppose x1 = ( 0. V);

        then x2 = B & (T . x1) = ( 0. U) by A4, Th66, RANKNULL: 9;

        hence thesis by A3, Th74;

      end;

        suppose x2 = ( 0. V);

        then x1 = B & (T . x2) = ( 0. U) by A4, Th66, RANKNULL: 9;

        hence thesis by A3, Th74;

      end;

    end;

    theorem :: POLYFORM:78

    

     Th76: ( dim ((( dim p) - 1) -bounding-chain-space p)) = 1

    proof

      set d = ( dim p);

      set T = (d -boundary p);

      set U = (d -chain-space p);

      set V = ((d - 1) -bounding-chain-space p);

      

       A1: ( card ( [#] V)) = ( card (T .: ( [#] U))) by RANKNULL:def 2

      .= ( card ( rng T)) by RELSET_1: 22;

      

       A2: ( card ( dom T)) = ( card ( [#] U)) by RANKNULL: 7

      .= 2 by Th61;

      T is one-to-one by Th75;

      then ( card ( [#] V)) = 2 by A1, A2, CARD_1: 70;

      hence thesis by RANKNULL: 6;

    end;

    theorem :: POLYFORM:79

    

     Th77: p is simply-connected implies ( dim ((( dim p) - 1) -circuit-space p)) = 1

    proof

      set d = ( dim p);

      set U = ((d - 1) -bounding-chain-space p);

      set V = ((d - 1) -circuit-space p);

      assume p is simply-connected;

      then U = V by Th48;

      hence thesis by Th76;

    end;

    theorem :: POLYFORM:80

    

     Th78: 1 < n & n < (( dim p) + 2) implies (( alternating-f-vector p) . n) = (( alternating-proper-f-vector p) . (n - 1))

    proof

      assume

       A1: 1 < n;

      (1 - 1) = 0 ;

      then

      reconsider m = (n - 1) as Element of NAT by A1, INT_1: 3, XREAL_1: 13;

      reconsider m as Nat;

      set apcs = ( alternating-proper-f-vector p);

      set acs = ( alternating-f-vector p);

      

       A2: (2 - 1) = 1;

      (1 + 1) = 2;

      then 2 <= n by A1, INT_1: 7;

      then

       A3: 1 <= m by A2, XREAL_1: 13;

      assume

       A4: n < (( dim p) + 2);

      then n < ((( dim p) + 1) + 1);

      then n <= (( dim p) + 1) by NAT_1: 13;

      then (n - 1) <= ((( dim p) + 1) - 1) by XREAL_1: 9;

      then

       A5: (apcs . m) = ((( - 1) |^ (m + 1)) * ( num-polytopes (p,(m - 1)))) by A3, Def27;

      (acs . n) = ((( - 1) |^ n) * ( num-polytopes (p,(n - 2)))) by A1, A4, Def26;

      hence thesis by A5;

    end;

    theorem :: POLYFORM:81

    

     Th79: ( alternating-f-vector p) = (( <*( - 1)*> ^ ( alternating-proper-f-vector p)) ^ <*(( - 1) |^ ( dim p))*>)

    proof

      set acs = ( alternating-f-vector p);

      set apcs = ( alternating-proper-f-vector p);

      set r = (( <*( - 1)*> ^ apcs) ^ <*(( - 1) |^ ( dim p))*>);

      set n = ( dim p);

      

       A1: ( len <*(( - 1) |^ ( dim p))*>) = 1 by FINSEQ_1: 39;

      

       A2: ( len apcs) = n by Def27;

      

       A3: ( len acs) = (n + 2) by Def26;

      

       A4: for k be Nat st 1 <= k & k <= ( len acs) holds (acs . k) = (r . k)

      proof

        let k be Nat such that

         A5: 1 <= k & k <= ( len acs);

        per cases by A3, A5, XXREAL_0: 1;

          suppose

           A6: k = 1;

          reconsider o = 1 as Nat;

          1 <= (n + 2) & (o - 2) = ( - 1) by Th10;

          then

           A7: (acs . o) = ((( - 1) |^ o) * ( num-polytopes (p,( - 1)))) by Def26;

          (( - 1) |^ 1) = ( - 1) & ( num-polytopes (p,( - 1))) = 1 by Th28;

          hence thesis by A6, A7, Th15;

        end;

          suppose

           A8: k = (n + 2);

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

          then k = ((( len <*( - 1)*>) + ( len apcs)) + 1) by A2, A8;

          

          then

           A9: (r . k) = (( - 1) |^ ( dim p)) by Th16

          .= (( - 1) |^ k) by A8, Th12;

          1 <= k by A8, Th10;

          then

           A10: (acs . k) = ((( - 1) |^ k) * ( num-polytopes (p,(k - 2)))) by A8, Def26;

          ( num-polytopes (p,(k - 2))) = 1 by A8, Th29;

          hence thesis by A10, A9;

        end;

          suppose

           A11: 1 < k & k < (n + 2);

          set m = (k - 1);

          

           A12: ((k + 1) - 1) = k & ((n + 2) - 1) = (n + 1);

          

           A13: (k + 1) <= (n + 2) by A11, INT_1: 7;

          ( len ( <*( - 1)*> ^ apcs)) = (( len <*( - 1)*>) + ( len apcs)) by FINSEQ_1: 22

          .= (n + 1) by A2, FINSEQ_1: 39;

          then ( len <*( - 1)*>) = 1 & k <= ( len ( <*( - 1)*> ^ apcs)) by A13, A12, FINSEQ_1: 39, XREAL_1: 9;

          then (r . k) = (apcs . m) by A11, Th17;

          hence thesis by A11, Th78;

        end;

      end;

      ( len r) = ((( len <*( - 1)*>) + ( len apcs)) + ( len <*(( - 1) |^ ( dim p))*>)) & ( len <*( - 1)*>) = 1 by Th14, FINSEQ_1: 39;

      hence thesis by A3, A2, A1, A4;

    end;

    begin

    theorem :: POLYFORM:82

    

     Th80: ( dim p) is odd implies ( Sum ( alternating-f-vector p)) = (( Sum ( alternating-proper-f-vector p)) - 2)

    proof

      reconsider minusone = ( - 1) as Integer;

      set acs = ( alternating-f-vector p);

      set apcs = ( alternating-proper-f-vector p);

      reconsider lastterm = (( - 1) |^ ( dim p)) as Integer;

      assume ( dim p) is odd;

      then

       A1: (( - 1) |^ ( dim p)) = ( - 1) by Th8;

      acs = (( <*( - 1)*> ^ apcs) ^ <*(( - 1) |^ ( dim p))*>) by Th79;

      

      then ( Sum acs) = ((( Sum <*minusone*>) + ( Sum apcs)) + ( Sum <*lastterm*>)) by Th19

      .= ((( Sum <*minusone*>) + ( Sum apcs)) + ( - 1)) by A1, RVSUM_1: 73

      .= ((( - 1) + ( Sum apcs)) + ( - 1)) by RVSUM_1: 73

      .= (( Sum apcs) - 2);

      hence thesis;

    end;

    theorem :: POLYFORM:83

    

     Th81: ( dim p) is even implies ( Sum ( alternating-f-vector p)) = ( Sum ( alternating-proper-f-vector p))

    proof

      reconsider minusone = ( - 1) as Integer;

      set acs = ( alternating-f-vector p);

      set apcs = ( alternating-proper-f-vector p);

      reconsider lastterm = (( - 1) |^ ( dim p)) as Integer;

      assume ( dim p) is even;

      then

       A1: (( - 1) |^ ( dim p)) = 1 by Th7;

      acs = (( <*( - 1)*> ^ apcs) ^ <*(( - 1) |^ ( dim p))*>) by Th79;

      

      then ( Sum acs) = ((( Sum <*minusone*>) + ( Sum apcs)) + ( Sum <*lastterm*>)) by Th19

      .= ((( Sum <*minusone*>) + ( Sum apcs)) + 1) by A1, RVSUM_1: 73

      .= ((( - 1) + ( Sum apcs)) + 1) by RVSUM_1: 73

      .= ( Sum apcs);

      hence thesis;

    end;

    theorem :: POLYFORM:84

    

     Th82: ( dim p) = 1 implies ( Sum ( alternating-proper-f-vector p)) = ( num-polytopes (p, 0 ))

    proof

      reconsider egy = 1 as Nat;

      set apcs = ( alternating-proper-f-vector p);

      assume ( dim p) = 1;

      then

       A1: ( len apcs) = 1 & (apcs . egy) = ((( - 1) |^ (egy + 1)) * ( num-polytopes (p,(egy - 1)))) by Def27;

      (( - 1) |^ (egy + 1)) = 1 by Th4, Th7;

      then apcs = <*( num-polytopes (p, 0 ))*> by A1, FINSEQ_1: 40;

      hence thesis by RVSUM_1: 73;

    end;

    theorem :: POLYFORM:85

    

     Th83: ( dim p) = 2 implies ( Sum ( alternating-proper-f-vector p)) = (( num-polytopes (p, 0 )) - ( num-polytopes (p,1)))

    proof

      reconsider t = 2 as Nat;

      reconsider o = 1 as Nat;

      set apcs = ( alternating-proper-f-vector p);

      reconsider apcso = (apcs . o) as Integer;

      reconsider apcst = (apcs . t) as Integer;

      assume

       A1: ( dim p) = 2;

      then

       A2: (apcs . o) = ((( - 1) |^ (o + 1)) * ( num-polytopes (p,(o - 1)))) & (apcs . t) = ((( - 1) |^ (t + 1)) * ( num-polytopes (p,(t - 1)))) by Def27;

      

       A3: (( - 1) |^ (o + 1)) = 1 & (( - 1) |^ (t + 1)) = ( - 1) by Th4, Th7, Th8;

      ( len apcs) = 2 by A1, Def27;

      then apcs = <*apcso, apcst*> by FINSEQ_1: 44;

      

      then ( Sum apcs) = (apcso + apcst) by RVSUM_1: 77

      .= (( num-polytopes (p, 0 )) - ( num-polytopes (p,1))) by A2, A3;

      hence thesis;

    end;

    theorem :: POLYFORM:86

    

     Th84: ( dim p) = 3 implies ( Sum ( alternating-proper-f-vector p)) = ((( num-polytopes (p, 0 )) - ( num-polytopes (p,1))) + ( num-polytopes (p,2)))

    proof

      reconsider mo = ( - 1) as Integer;

      reconsider th = 3 as Nat;

      reconsider tw = 2 as Nat;

      reconsider o = 1 as Nat;

      assume

       A1: ( dim p) = 3;

      set apcs = ( alternating-proper-f-vector p);

      (( - 1) |^ (tw + 1)) = ( - 1) by Th5, Th8;

      then

       A2: (apcs . tw) = (mo * ( num-polytopes (p,(tw - 1)))) by A1, Def27;

      (( - 1) |^ (th + 1)) = 1 by Th6, Th7;

      then

       A3: (apcs . th) = (o * ( num-polytopes (p,(th - 1)))) by A1, Def27;

      reconsider apcsth = (apcs . th) as Integer;

      reconsider apcstw = (apcs . tw) as Integer;

      reconsider apcson = (apcs . o) as Integer;

      (( - 1) |^ (o + 1)) = 1 by Th4, Th7;

      then

       A4: (apcs . o) = (o * ( num-polytopes (p,(o - 1)))) by A1, Def27;

      ( len apcs) = 3 by A1, Def27;

      then apcs = <*apcson, apcstw, apcsth*> by FINSEQ_1: 45;

      

      then ( Sum apcs) = ((apcson + apcstw) + apcsth) by RVSUM_1: 78

      .= ((( num-polytopes (p, 0 )) - ( num-polytopes (p,1))) + ( num-polytopes (p,2))) by A4, A2, A3;

      hence thesis;

    end;

    theorem :: POLYFORM:87

    

     Th85: ( dim p) = 0 implies p is eulerian

    proof

      set d = ( dim p);

      set apcs = ( alternating-proper-f-vector p);

      assume

       A1: d = 0 ;

      then (( - 1) |^ (d + 1)) = ( - 1);

      then

       A2: (1 + (( - 1) |^ (d + 1))) = 0 ;

      ( len apcs) = 0 by A1, Def27;

      then apcs = ( <*> INT );

      hence thesis by A2, GR_CY_1: 3;

    end;

    theorem :: POLYFORM:88

    

     Th86: p is simply-connected implies p is eulerian

    proof

      assume

       A1: p is simply-connected;

      set apcs = ( alternating-proper-f-vector p);

      per cases ;

        suppose ( dim p) = 0 ;

        hence thesis by Th85;

      end;

        suppose

         A2: ( dim p) > 0 ;

        deffunc B( Nat) = ((( - 1) |^ ($1 + 1)) * ( dim (($1 - 1) -circuit-space p)));

        deffunc A( Nat) = ((( - 1) |^ ($1 + 1)) * ( dim (($1 - 2) -bounding-chain-space p)));

        consider a be FinSequence such that

         A3: ( len a) = ( len apcs) and

         A4: for n be Nat st n in ( dom a) holds (a . n) = A(n) from FINSEQ_1:sch 2;

        

         A5: ( rng a) c= INT

        proof

          let y be object;

          assume y in ( rng a);

          then

          consider x be object such that

           A6: x in ( dom a) and

           A7: y = (a . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A6;

          (a . x) = ((( - 1) |^ (x + 1)) * ( dim ((x - 2) -bounding-chain-space p))) by A4, A6;

          hence thesis by A7, INT_1:def 2;

        end;

        consider b be FinSequence such that

         A8: ( len b) = ( len apcs) and

         A9: for n be Nat st n in ( dom b) holds (b . n) = B(n) from FINSEQ_1:sch 2;

        ( rng b) c= INT

        proof

          let y be object;

          assume y in ( rng b);

          then

          consider x be object such that

           A10: x in ( dom b) and

           A11: y = (b . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A10;

          (b . x) = ((( - 1) |^ (x + 1)) * ( dim ((x - 1) -circuit-space p))) by A9, A10;

          hence thesis by A11, INT_1:def 2;

        end;

        then

        reconsider a, b as FinSequence of INT by A5, FINSEQ_1:def 4;

        

         A12: ( len apcs) > 0 by A2, Def27;

        

         A13: (a . 1) = 1

        proof

          reconsider egy = 1 as Element of NAT ;

          1 <= ( 0 qua Nat + 1);

          then egy <= ( len apcs) by A12, NAT_1: 13;

          then egy in ( dom a) by A3, FINSEQ_3: 25;

          

          then (a . egy) = ((( - 1) |^ (1 + 1)) * ( dim ((egy - 2) -bounding-chain-space p))) by A4

          .= (1 * ( dim ((egy - 2) -bounding-chain-space p))) by Th4, Th7

          .= 1 by Th60;

          hence thesis;

        end;

        

         A14: for n be Nat st 1 <= n & n < ( len apcs) holds (b . n) = ( - (a . (n + 1)))

        proof

          let n be Nat such that

           A15: 1 <= n and

           A16: n < ( len apcs);

          

           A17: n in ( dom b) by A8, A15, A16, FINSEQ_3: 25;

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

          

           A18: (b . n) = ((( - 1) |^ (n + 1)) * ( dim ((n - 1) -circuit-space p))) by A9, A17;

          

           A19: 1 <= (n + 1) by NAT_1: 11;

          (n + 1) <= ( len apcs) by A16, INT_1: 7;

          then (n + 1) in ( dom a) by A3, A19, FINSEQ_3: 25;

          

          then (a . (n + 1)) = A(+) by A4

          .= (((( - 1) |^ (n + 1)) * (( - 1) |^ 1)) * ( dim ((n - 1) -bounding-chain-space p))) by NEWTON: 8

          .= (((( - 1) |^ (n + 1)) * ( - 1)) * ( dim ((n - 1) -bounding-chain-space p)))

          .= ( - ((( - 1) |^ (n + 1)) * ( dim ((n - 1) -bounding-chain-space p))))

          .= ( - (b . n)) by A1, A18, Th48;

          hence thesis;

        end;

        

         A20: (b . ( len apcs)) = (( - 1) |^ (( dim p) + 1))

        proof

          reconsider n = ( len apcs) as Element of NAT ;

          

           A21: n = ( dim p) by Def27;

          ( 0 qua Nat + 1) = 1;

          then 1 <= ( len apcs) by A12, NAT_1: 13;

          then n in ( dom b) by A8, FINSEQ_3: 25;

          

          then (b . n) = B(n) by A9

          .= ((( - 1) |^ (n + 1)) * 1) by A1, A21, Th77

          .= (( - 1) |^ (n + 1));

          hence thesis by Def27;

        end;

        for n be Nat st 1 <= n & n <= ( len apcs) holds (apcs . n) = ((a . n) + (b . n))

        proof

          let n be Nat such that

           A22: 1 <= n & n <= ( len apcs);

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

          n9 in ( dom a) by A3, A22, FINSEQ_3: 25;

          then

           A23: (a . n9) = ((( - 1) |^ (n9 + 1)) * ( dim ((n9 - 2) -bounding-chain-space p))) by A4;

          (apcs . n) = (((( - 1) |^ (n + 1)) * ( dim ((n - 2) -bounding-chain-space p))) + ((( - 1) |^ (n + 1)) * ( dim ((n - 1) -circuit-space p)))) & n9 in ( dom b) by A8, A22, Th49, FINSEQ_3: 25;

          hence thesis by A9, A23;

        end;

        then ( Sum apcs) = ((a . 1) + (b . ( len apcs))) by A12, A3, A8, A14, Th13;

        hence thesis by A13, A20;

      end;

    end;

    theorem :: POLYFORM:89

    p is simply-connected & ( dim p) = 1 implies ( num-vertices p) = 2

    proof

      set acs = ( alternating-f-vector p);

      set apcs = ( alternating-proper-f-vector p);

      assume p is simply-connected;

      then

       A1: p is eulerian by Th86;

      assume

       A2: ( dim p) = 1;

       0 = ( Sum acs) by A1

      .= (( Sum apcs) - 2) by A2, Th3, Th80

      .= (( num-polytopes (p, 0 )) - 2) by A2, Th82;

      hence thesis;

    end;

    theorem :: POLYFORM:90

    p is simply-connected & ( dim p) = 2 implies ( num-vertices p) = ( num-edges p)

    proof

      set s = (( num-polytopes (p, 0 )) - ( num-polytopes (p,1)));

      set c = ( alternating-f-vector p);

      assume p is simply-connected;

      then

       A1: p is eulerian by Th86;

      assume

       A2: ( dim p) = 2;

      then

       A3: s = ( Sum ( alternating-proper-f-vector p)) by Th83;

       0 = ( Sum c) by A1

      .= s by A2, A3, Th4, Th81;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: POLYFORM:91

    p is simply-connected & ( dim p) = 3 implies ((( num-vertices p) - ( num-edges p)) + ( num-faces p)) = 2

    proof

      set s = ((( num-polytopes (p, 0 )) - ( num-polytopes (p,1))) + ( num-polytopes (p,2)));

      set c = ( alternating-f-vector p);

      assume p is simply-connected;

      then

       A1: p is eulerian by Th86;

      assume

       A2: ( dim p) = 3;

      then

       A3: s = ( Sum ( alternating-proper-f-vector p)) by Th84;

       0 = ( Sum c) by A1

      .= (s - 2) by A2, A3, Th5, Th80;

      hence thesis;

    end;